Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: left


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)])}
(append([_es, _fs, _gs]) /\ append([_es, _fs, _hs])) -> eq_eltlist([_gs, _hs])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js])}
(reverse([_ks, _ls]) /\ reverse([_ks, _ms])) -> eq_eltlist([_ls, _ms])
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_os, _ps, _qs]) /\ insert([_os, _ps, _rs])) -> eq_eltlist([_qs, _rs])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts])}
(sort([_us, _vs]) /\ sort([_us, _ws])) -> eq_eltlist([_vs, _ws])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
}

properties:
{(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys])}


over-approximation: {append, insert, reverse, sort}
under-approximation: {leq, sort}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 0
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 0
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 0
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 0
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 0
}


Solving took 0.769404 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<a, b>() -> q_gen_4905
<b, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<cons>(q_gen_4950, q_gen_4949) -> q_gen_4949
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<cons, nil>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008661 s (model generation: 0.007950,  model checking: 0.000711):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.009253 s (model generation: 0.009182,  model checking: 0.000071):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884},
Q_f={q_gen_4884},
Delta=
{
<nil>() -> q_gen_4884
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.008076 s (model generation: 0.008011,  model checking: 0.000065):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.008407 s (model generation: 0.008343,  model checking: 0.000064):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 4, which took 0.008200 s (model generation: 0.008036,  model checking: 0.000164):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 5, which took 0.008092 s (model generation: 0.008049,  model checking: 0.000043):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 6, which took 0.007990 s (model generation: 0.007864,  model checking: 0.000126):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 7, which took 0.010735 s (model generation: 0.008643,  model checking: 0.002092):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.016499 s (model generation: 0.016061,  model checking: 0.000438):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894},
Q_f={q_gen_4894},
Delta=
{
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 2
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.012811 s (model generation: 0.012657,  model checking: 0.000154):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894},
Q_f={q_gen_4894},
Delta=
{
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887},
Q_f={q_gen_4887},
Delta=
{
<nil, nil>() -> q_gen_4887
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 1
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 2
}
Sat witness: Found: ((insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]), {
_ss -> nil  ;  _ts -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 10, which took 0.011119 s (model generation: 0.010806,  model checking: 0.000313):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894},
Q_f={q_gen_4894},
Delta=
{
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 1
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 2
}
Sat witness: Found: ((insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]), {
_ns -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 11, which took 0.011324 s (model generation: 0.011134,  model checking: 0.000190):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894},
Q_f={q_gen_4894},
Delta=
{
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, a>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 1
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 2
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.011517 s (model generation: 0.011412,  model checking: 0.000105):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<nil, nil>() -> q_gen_4904
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, a>() -> q_gen_4889
<b, b>() -> q_gen_4889
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 2
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 3
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 13, which took 0.015291 s (model generation: 0.015031,  model checking: 0.000260):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<nil, nil>() -> q_gen_4904
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 3
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 4
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 14, which took 0.012209 s (model generation: 0.011383,  model checking: 0.000826):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<nil, nil>() -> q_gen_4904
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 15, which took 0.009950 s (model generation: 0.009691,  model checking: 0.000259):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<nil, nil>() -> q_gen_4904
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 4
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 16, which took 0.011909 s (model generation: 0.011169,  model checking: 0.000740):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<nil, nil>() -> q_gen_4904
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 17, which took 0.012618 s (model generation: 0.011947,  model checking: 0.000671):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 5
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.012425 s (model generation: 0.012084,  model checking: 0.000341):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 4
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 5
}
Sat witness: Found: ((insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]), {
_ss -> nil  ;  _ts -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 19, which took 0.012439 s (model generation: 0.011976,  model checking: 0.000463):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 4
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 7
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 5
}
Sat witness: Found: ((insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]), {
_ns -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 20, which took 0.013967 s (model generation: 0.012950,  model checking: 0.001017):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905},
Q_f={q_gen_4894},
Delta=
{
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 4
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 7
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 7
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 5
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.013358 s (model generation: 0.013220,  model checking: 0.000138):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888},
Q_f={q_gen_4888},
Delta=
{
<nil, nil>() -> q_gen_4888
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 7
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 7
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 7
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 5
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> nil  ;  _js -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.016393 s (model generation: 0.015032,  model checking: 0.001361):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> reverse([nil, nil]) -> 5
() -> sort([nil, nil]) -> 5
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 5
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 7
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 7
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 7
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 6
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 6
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.016131 s (model generation: 0.015712,  model checking: 0.000419):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> reverse([nil, nil]) -> 6
() -> sort([nil, nil]) -> 6
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 6
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 7
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 7
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 7
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 7
}
Sat witness: Found: ((insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]), {
_ss -> nil  ;  _ts -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 24, which took 0.017979 s (model generation: 0.016853,  model checking: 0.001126):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 7
() -> reverse([nil, nil]) -> 7
() -> sort([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 7
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 7
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 10
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 8
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 8
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 8
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.016054 s (model generation: 0.015838,  model checking: 0.000216):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 7
() -> reverse([nil, nil]) -> 7
() -> sort([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 7
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 10
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 10
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 8
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 8
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 8
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> nil  ;  _js -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.018290 s (model generation: 0.016710,  model checking: 0.001580):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> insert([x, nil, cons(x, nil)]) -> 8
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 8
() -> reverse([nil, nil]) -> 8
() -> sort([nil, nil]) -> 8
() -> sorted([cons(x, nil)]) -> 8
() -> sorted([nil]) -> 8
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 10
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 10
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 9
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 9
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 9
}
Sat witness: Found: ((insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]), {
_ss -> nil  ;  _ts -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 27, which took 0.020257 s (model generation: 0.018245,  model checking: 0.002012):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> insert([x, nil, cons(x, nil)]) -> 9
() -> leq([a, y]) -> 9
() -> leq([b, b]) -> 9
() -> reverse([nil, nil]) -> 9
() -> sort([nil, nil]) -> 9
() -> sorted([cons(x, nil)]) -> 9
() -> sorted([nil]) -> 9
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 10
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 13
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 10
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 10
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 10
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.020214 s (model generation: 0.019014,  model checking: 0.001200):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, b, a>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930},
Q_f={q_gen_4888},
Delta=
{
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> insert([x, nil, cons(x, nil)]) -> 10
() -> leq([a, y]) -> 10
() -> leq([b, b]) -> 10
() -> reverse([nil, nil]) -> 10
() -> sort([nil, nil]) -> 10
() -> sorted([cons(x, nil)]) -> 10
() -> sorted([nil]) -> 10
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 13
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 13
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 11
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 11
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 11
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> nil  ;  _js -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.023671 s (model generation: 0.020524,  model checking: 0.003147):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, b, a>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> insert([x, nil, cons(x, nil)]) -> 11
() -> leq([a, y]) -> 11
() -> leq([b, b]) -> 11
() -> reverse([nil, nil]) -> 11
() -> sort([nil, nil]) -> 11
() -> sorted([cons(x, nil)]) -> 11
() -> sorted([nil]) -> 11
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 13
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 16
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 12
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 14
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 12
(leq([b, a])) -> BOT -> 12
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 12
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.023082 s (model generation: 0.021433,  model checking: 0.001649):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> insert([x, nil, cons(x, nil)]) -> 12
() -> leq([a, y]) -> 12
() -> leq([b, b]) -> 12
() -> reverse([nil, nil]) -> 12
() -> sort([nil, nil]) -> 12
() -> sorted([cons(x, nil)]) -> 12
() -> sorted([nil]) -> 12
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 16
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 16
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 13
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 14
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13
(leq([b, a])) -> BOT -> 13
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 13
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> cons(b, nil)  ;  _js -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.026243 s (model generation: 0.023443,  model checking: 0.002800):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> insert([x, nil, cons(x, nil)]) -> 13
() -> leq([a, y]) -> 13
() -> leq([b, b]) -> 13
() -> reverse([nil, nil]) -> 13
() -> sort([nil, nil]) -> 13
() -> sorted([cons(x, nil)]) -> 13
() -> sorted([nil]) -> 13
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 16
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 19
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 14
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 15
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14
(leq([b, a])) -> BOT -> 14
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 14
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 32, which took 0.025955 s (model generation: 0.023508,  model checking: 0.002447):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> insert([x, nil, cons(x, nil)]) -> 14
() -> leq([a, y]) -> 14
() -> leq([b, b]) -> 14
() -> reverse([nil, nil]) -> 14
() -> sort([nil, nil]) -> 14
() -> sorted([cons(x, nil)]) -> 14
() -> sorted([nil]) -> 14
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 19
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 19
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 15
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 16
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15
(leq([b, a])) -> BOT -> 15
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 15
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> nil  ;  _js -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 33, which took 0.033625 s (model generation: 0.030483,  model checking: 0.003142):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> insert([x, nil, cons(x, nil)]) -> 15
() -> leq([a, y]) -> 15
() -> leq([b, b]) -> 15
() -> reverse([nil, nil]) -> 15
() -> sort([nil, nil]) -> 15
() -> sorted([cons(x, nil)]) -> 15
() -> sorted([nil]) -> 15
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 19
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 22
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 16
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 17
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16
(leq([b, a])) -> BOT -> 16
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 16
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.031766 s (model generation: 0.029407,  model checking: 0.002359):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> insert([x, nil, cons(x, nil)]) -> 16
() -> leq([a, y]) -> 16
() -> leq([b, b]) -> 16
() -> reverse([nil, nil]) -> 16
() -> sort([nil, nil]) -> 16
() -> sorted([cons(x, nil)]) -> 16
() -> sorted([nil]) -> 16
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 22
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 22
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 17
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 18
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 17
(leq([b, a])) -> BOT -> 17
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 17
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> cons(a, nil)  ;  _js -> cons(a, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.037947 s (model generation: 0.032311,  model checking: 0.005636):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> insert([x, nil, cons(x, nil)]) -> 17
() -> leq([a, y]) -> 17
() -> leq([b, b]) -> 17
() -> reverse([nil, nil]) -> 17
() -> sort([nil, nil]) -> 17
() -> sorted([cons(x, nil)]) -> 17
() -> sorted([nil]) -> 17
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 22
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 25
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 18
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 19
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18
(leq([b, a])) -> BOT -> 18
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 18
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 36, which took 0.037382 s (model generation: 0.035162,  model checking: 0.002220):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> insert([x, nil, cons(x, nil)]) -> 18
() -> leq([a, y]) -> 18
() -> leq([b, b]) -> 18
() -> reverse([nil, nil]) -> 18
() -> sort([nil, nil]) -> 18
() -> sorted([cons(x, nil)]) -> 18
() -> sorted([nil]) -> 18
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 25
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 25
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 19
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 20
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 19
(leq([b, a])) -> BOT -> 19
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 19
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> nil  ;  _js -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.046119 s (model generation: 0.040897,  model checking: 0.005222):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<b, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<cons>(q_gen_4950, q_gen_4949) -> q_gen_4949
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> insert([x, nil, cons(x, nil)]) -> 19
() -> leq([a, y]) -> 19
() -> leq([b, b]) -> 19
() -> reverse([nil, nil]) -> 19
() -> sort([nil, nil]) -> 19
() -> sorted([cons(x, nil)]) -> 19
() -> sorted([nil]) -> 19
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 25
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 28
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 20
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 21
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20
(leq([b, a])) -> BOT -> 20
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 20
}
Sat witness: Found: ((append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]), {
_ds -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 38, which took 0.050305 s (model generation: 0.047578,  model checking: 0.002727):

Model:
|_
{
append -> 
{{{
Q={q_gen_4894, q_gen_4904, q_gen_4905, q_gen_4926, q_gen_4927, q_gen_4928},
Q_f={q_gen_4894},
Delta=
{
<cons>(q_gen_4927, q_gen_4926) -> q_gen_4926
<nil>() -> q_gen_4926
<a>() -> q_gen_4927
<b>() -> q_gen_4927
<cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4904
<nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4904
<nil, nil>() -> q_gen_4904
<a, a>() -> q_gen_4905
<a, b>() -> q_gen_4905
<b, a>() -> q_gen_4905
<b, b>() -> q_gen_4905
<cons, cons, cons>(q_gen_4928, q_gen_4894) -> q_gen_4894
<cons, nil, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, cons, cons>(q_gen_4905, q_gen_4904) -> q_gen_4894
<nil, nil, cons>(q_gen_4927, q_gen_4926) -> q_gen_4894
<nil, nil, nil>() -> q_gen_4894
<a, a, a>() -> q_gen_4928
<a, b, a>() -> q_gen_4928
<b, a, b>() -> q_gen_4928
<b, b, b>() -> q_gen_4928
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  insert -> 
{{{
Q={q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4896, q_gen_4897},
Q_f={q_gen_4891},
Delta=
{
<nil>() -> q_gen_4892
<a>() -> q_gen_4893
<b>() -> q_gen_4893
<cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4896
<nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4896
<a, a>() -> q_gen_4897
<a, b>() -> q_gen_4897
<b, a>() -> q_gen_4897
<b, b>() -> q_gen_4897
<a, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<a, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
<b, cons, cons>(q_gen_4897, q_gen_4896) -> q_gen_4891
<b, nil, cons>(q_gen_4893, q_gen_4892) -> q_gen_4891
}

Datatype: <elt, eltlist, eltlist>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_4889, q_gen_4900},
Q_f={q_gen_4889},
Delta=
{
<a, a>() -> q_gen_4889
<a, b>() -> q_gen_4889
<b, b>() -> q_gen_4889
<b, a>() -> q_gen_4900
}

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_4888, q_gen_4930, q_gen_4949, q_gen_4950},
Q_f={q_gen_4888},
Delta=
{
<cons>(q_gen_4950, q_gen_4949) -> q_gen_4949
<nil>() -> q_gen_4949
<a>() -> q_gen_4950
<b>() -> q_gen_4950
<cons, cons>(q_gen_4930, q_gen_4888) -> q_gen_4888
<nil, cons>(q_gen_4950, q_gen_4949) -> q_gen_4888
<nil, nil>() -> q_gen_4888
<a, a>() -> q_gen_4930
<a, b>() -> q_gen_4930
<b, a>() -> q_gen_4930
<b, b>() -> q_gen_4930
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_4887, q_gen_4899},
Q_f={q_gen_4887},
Delta=
{
<cons, cons>(q_gen_4899, q_gen_4887) -> q_gen_4887
<nil, nil>() -> q_gen_4887
<a, a>() -> q_gen_4899
<a, b>() -> q_gen_4899
<b, a>() -> q_gen_4899
<b, b>() -> q_gen_4899
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}
  ;  sorted -> 
{{{
Q={q_gen_4884, q_gen_4886},
Q_f={q_gen_4884},
Delta=
{
<cons>(q_gen_4886, q_gen_4884) -> q_gen_4884
<nil>() -> q_gen_4884
<a>() -> q_gen_4886
<b>() -> q_gen_4886
}

Datatype: <eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> insert([x, nil, cons(x, nil)]) -> 20
() -> leq([a, y]) -> 20
() -> leq([b, b]) -> 20
() -> reverse([nil, nil]) -> 20
() -> sort([nil, nil]) -> 20
() -> sorted([cons(x, nil)]) -> 20
() -> sorted([nil]) -> 20
(append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]) -> 28
(append([t1, l2, _ds])) -> append([cons(h1, t1), l2, cons(h1, _ds)]) -> 28
(insert([x, z, _ns]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _ns)]) -> 21
(insert([y, _ss, _ts]) /\ sort([z, _ss])) -> sort([cons(y, z), _ts]) -> 22
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 21
(leq([b, a])) -> BOT -> 21
(reverse([_xs, _ys]) /\ reverse([l, _xs]) /\ sorted([l])) -> sorted([_ys]) -> 21
}
Sat witness: Found: ((append([_is, cons(h1, nil), _js]) /\ reverse([t1, _is])) -> reverse([cons(h1, t1), _js]), {
_is -> cons(b, nil)  ;  _js -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

Total time: 0.769404
Reason for stopping: Proved