Solving ../../benchmarks/true/insert_length_eq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_xl, _yl, _am]) /\ insert([_xl, _yl, _zl])) -> eq_eltlist([_zl, _am])
)
(length, F:
{() -> length([nil, z])
(length([ll, _bm])) -> length([cons(x, ll), s(_bm)])}
(length([_cm, _dm]) /\ length([_cm, _em])) -> eq_nat([_dm, _em])
)
}

properties:
{(insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm])}


over-approximation: {insert, length}
under-approximation: {leq}

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 0  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 0  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 0  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0  ;  (leq([b, a])) -> BOT -> 0
}


Solving took 30.000430 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1033, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037, q_gen_1041, q_gen_1042, q_gen_1043, q_gen_1045, q_gen_1046, q_gen_1047, q_gen_1048, q_gen_1049, q_gen_1052, q_gen_1053, q_gen_1054, q_gen_1055, q_gen_1056, q_gen_1057, q_gen_1058, q_gen_1059, q_gen_1063, q_gen_1065, q_gen_1066, q_gen_1067, q_gen_1068, q_gen_1069, q_gen_1070, q_gen_1071, q_gen_1072},
Q_f={},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<a>() -> q_gen_1046
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1056
<cons>(q_gen_1032, q_gen_1056) -> q_gen_1069
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, a>() -> q_gen_1037
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1042
<a, a>() -> q_gen_1043
<nil, b>() -> q_gen_1048
<b, b>() -> q_gen_1049
<cons, cons>(q_gen_1049, q_gen_1036, q_gen_1048, q_gen_1034) -> q_gen_1053
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1054
<a, cons>(q_gen_1032, q_gen_1056) -> q_gen_1055
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1058
<b, cons>(q_gen_1032, q_gen_1056) -> q_gen_1059
<cons, cons>(q_gen_1049, q_gen_1059, q_gen_1058, q_gen_1053) -> q_gen_1066
<cons, a>(q_gen_1032, q_gen_1056) -> q_gen_1067
<a, cons>(q_gen_1032, q_gen_1069) -> q_gen_1068
<cons, b>(q_gen_1032, q_gen_1056) -> q_gen_1071
<b, cons>(q_gen_1032, q_gen_1069) -> q_gen_1072
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1033
<b, cons, cons>(q_gen_1043, q_gen_1042, q_gen_1035, q_gen_1034) -> q_gen_1041
<a, nil, cons>(q_gen_1046, q_gen_1031) -> q_gen_1045
<b, cons, cons>(q_gen_1049, q_gen_1036, q_gen_1048, q_gen_1034) -> q_gen_1047
<b, cons, cons>(q_gen_1043, q_gen_1055, q_gen_1054, q_gen_1053) -> q_gen_1052
<b, cons, cons>(q_gen_1049, q_gen_1059, q_gen_1058, q_gen_1053) -> q_gen_1057
<b, nil, cons>(q_gen_1032, q_gen_1056) -> q_gen_1063
<b, cons, cons>(q_gen_1043, q_gen_1068, q_gen_1067, q_gen_1066) -> q_gen_1065
<b, cons, cons>(q_gen_1049, q_gen_1072, q_gen_1071, q_gen_1066) -> q_gen_1070
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1038, q_gen_1039, q_gen_1050, q_gen_1051, q_gen_1060, q_gen_1061, q_gen_1062, q_gen_1064, q_gen_1073, q_gen_1074},
Q_f={},
Delta=
{
<z>() -> q_gen_1062
<nil, z>() -> q_gen_1029
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1038
<b, z>() -> q_gen_1039
<cons, s>(q_gen_1051, q_gen_1029) -> q_gen_1050
<a, z>() -> q_gen_1051
<cons, s>(q_gen_1061, q_gen_1050) -> q_gen_1060
<b, s>(q_gen_1062) -> q_gen_1061
<cons, s>(q_gen_1061, q_gen_1038) -> q_gen_1064
<cons, s>(q_gen_1074, q_gen_1038) -> q_gen_1073
<a, s>(q_gen_1062) -> q_gen_1074
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1028, q_gen_1040, q_gen_1044},
Q_f={},
Delta=
{
<b, b>() -> q_gen_1027
<a, b>() -> q_gen_1028
<b, a>() -> q_gen_1040
<a, a>() -> q_gen_1044
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004086 s (model generation: 0.003465,  model checking: 0.000621):

Model:
|_
{
insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 1, which took 0.003477 s (model generation: 0.003452,  model checking: 0.000025):

Model:
|_
{
insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 2, which took 0.003415 s (model generation: 0.003373,  model checking: 0.000042):

Model:
|_
{
insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.003569 s (model generation: 0.003421,  model checking: 0.000148):

Model:
|_
{
insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029},
Q_f={q_gen_1029},
Delta=
{
<nil, z>() -> q_gen_1029
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.004210 s (model generation: 0.003463,  model checking: 0.000747):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029},
Q_f={q_gen_1029},
Delta=
{
<nil, z>() -> q_gen_1029
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 5, which took 0.003776 s (model generation: 0.003658,  model checking: 0.000118):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029},
Q_f={q_gen_1029},
Delta=
{
<nil, z>() -> q_gen_1029
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 1  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((length([ll, _bm])) -> length([cons(x, ll), s(_bm)]), {
_bm -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 6, which took 0.004925 s (model generation: 0.003704,  model checking: 0.001221):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 1  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]), {
_wl -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 7, which took 0.004549 s (model generation: 0.004427,  model checking: 0.000122):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, a>() -> q_gen_1027
<b, b>() -> q_gen_1027
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 2  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 8, which took 0.004843 s (model generation: 0.004675,  model checking: 0.000168):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 3  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 9, which took 0.004695 s (model generation: 0.004075,  model checking: 0.000620):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 4  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.008147 s (model generation: 0.004162,  model checking: 0.003985):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 4  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 11, which took 0.004797 s (model generation: 0.004689,  model checking: 0.000108):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 4  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 4  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((length([ll, _bm])) -> length([cons(x, ll), s(_bm)]), {
_bm -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 12, which took 0.010510 s (model generation: 0.004691,  model checking: 0.005819):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 4  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 7  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]), {
_wl -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.008226 s (model generation: 0.005522,  model checking: 0.002704):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 5  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 5  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 7  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 6
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.006187 s (model generation: 0.005831,  model checking: 0.000356):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039},
Q_f={q_gen_1029},
Delta=
{
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 6  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 6  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 7  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7
}
Sat witness: Yes: ((length([ll, _bm])) -> length([cons(x, ll), s(_bm)]), {
_bm -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 15, which took 0.006076 s (model generation: 0.005915,  model checking: 0.000161):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037},
Q_f={q_gen_1030},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039, q_gen_1062},
Q_f={q_gen_1029},
Delta=
{
<z>() -> q_gen_1062
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, s>(q_gen_1062) -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 6  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 9  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 7  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7
}
Sat witness: Yes: ((insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]), {
_fm -> z  ;  _gm -> cons(b, cons(b, nil))  ;  _hm -> s(s(z))  ;  l -> nil  ;  x -> b
})

-------------------------------------------
Step 16, which took 0.174794 s (model generation: 0.006942,  model checking: 0.167852):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037, q_gen_1056, q_gen_1063},
Q_f={q_gen_1030},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1056
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1056) -> q_gen_1063
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039, q_gen_1062},
Q_f={q_gen_1029},
Delta=
{
<z>() -> q_gen_1062
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, s>(q_gen_1062) -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 9  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 10  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8
}
Sat witness: Yes: ((insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]), {
_wl -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  y -> a  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.025017 s (model generation: 0.008018,  model checking: 0.016999):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037, q_gen_1056, q_gen_1063},
Q_f={q_gen_1030},
Delta=
{
<cons>(q_gen_1032, q_gen_1056) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1056
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, a>(q_gen_1032, q_gen_1056) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1056) -> q_gen_1063
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039, q_gen_1062},
Q_f={q_gen_1029},
Delta=
{
<z>() -> q_gen_1062
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, s>(q_gen_1062) -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 8  ;  () -> length([nil, z]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 8  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 10  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 10  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 9
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 18, which took 0.009372 s (model generation: 0.008015,  model checking: 0.001357):

Model:
|_
{
insert -> 
{{{
Q={q_gen_1030, q_gen_1031, q_gen_1032, q_gen_1034, q_gen_1035, q_gen_1036, q_gen_1037, q_gen_1056, q_gen_1063},
Q_f={q_gen_1030},
Delta=
{
<cons>(q_gen_1032, q_gen_1056) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1056
<cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1034
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1034
<cons, a>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, a>(q_gen_1032, q_gen_1056) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1031) -> q_gen_1035
<cons, b>(q_gen_1032, q_gen_1056) -> q_gen_1035
<nil, a>() -> q_gen_1035
<nil, b>() -> q_gen_1035
<a, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<a, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1031) -> q_gen_1036
<b, cons>(q_gen_1032, q_gen_1056) -> q_gen_1036
<a, a>() -> q_gen_1037
<b, a>() -> q_gen_1037
<b, b>() -> q_gen_1037
<a, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<a, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, cons, cons>(q_gen_1037, q_gen_1036, q_gen_1035, q_gen_1034) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1030
<b, nil, cons>(q_gen_1032, q_gen_1056) -> q_gen_1063
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_1029, q_gen_1039, q_gen_1062},
Q_f={q_gen_1029},
Delta=
{
<z>() -> q_gen_1062
<cons, s>(q_gen_1039, q_gen_1029) -> q_gen_1029
<nil, z>() -> q_gen_1029
<a, z>() -> q_gen_1039
<b, s>(q_gen_1062) -> q_gen_1039
<b, z>() -> q_gen_1039
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_1027, q_gen_1040},
Q_f={q_gen_1027},
Delta=
{
<a, a>() -> q_gen_1027
<a, b>() -> q_gen_1027
<b, b>() -> q_gen_1027
<b, a>() -> q_gen_1040
}

Datatype: <elt, elt>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 9  ;  () -> length([nil, z]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 9  ;  (insert([x, l, _gm]) /\ length([_gm, _hm]) /\ length([l, _fm])) -> eq_nat([s(_fm), _hm]) -> 10  ;  (insert([x, z, _wl]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _wl)]) -> 10  ;  (length([ll, _bm])) -> length([cons(x, ll), s(_bm)]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 10
}
Sat witness: Yes: ((length([ll, _bm])) -> length([cons(x, ll), s(_bm)]), {
_bm -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

Total time: 30.000430
Reason for stopping: DontKnow. Stopped because: timeout