Solving ../../benchmarks/true/timbuk_insertionSort.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_qk, _rk, _sk]) /\ insert([_qk, _rk, _tk])) -> eq_eltlist([_sk, _tk])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk])}
(sort([_wk, _xk]) /\ sort([_wk, _yk])) -> eq_eltlist([_xk, _yk])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
}

properties:
{(sort([l, _zk])) -> sorted([_zk])}


over-approximation: {insert, sort}
under-approximation: {leq, sorted}

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 0  ;  () -> sorted([nil]) -> 0  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 0  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 0  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0  ;  (leq([b, a])) -> BOT -> 0  ;  (sort([l, _zk])) -> sorted([_zk]) -> 0
}


Solving took 0.357919 seconds.
Proved
Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<a, b>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<cons>(q_gen_6219, q_gen_6218) -> q_gen_6218
<nil>() -> q_gen_6218
<a>() -> q_gen_6219
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<cons, a>(q_gen_6219, q_gen_6218) -> q_gen_6188
<cons, b>(q_gen_6219, q_gen_6218) -> q_gen_6188
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011948 s (model generation: 0.011655,  model checking: 0.000293):

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 0  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.004574 s (model generation: 0.004438,  model checking: 0.000136):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 0  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.008424 s (model generation: 0.006950,  model checking: 0.001474):

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

}

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

}

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

}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.004114 s (model generation: 0.004090,  model checking: 0.000024):

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

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176},
Q_f={q_gen_6176},
Delta=
{
<nil, nil>() -> q_gen_6176
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.003667 s (model generation: 0.003641,  model checking: 0.000026):

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

}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176},
Q_f={q_gen_6176},
Delta=
{
<nil, nil>() -> q_gen_6176
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.010945 s (model generation: 0.010587,  model checking: 0.000358):

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

}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176},
Q_f={q_gen_6176},
Delta=
{
<nil, nil>() -> q_gen_6176
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1  ;  (sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 6, which took 0.016800 s (model generation: 0.011678,  model checking: 0.005122):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176},
Q_f={q_gen_6176},
Delta=
{
<nil, nil>() -> q_gen_6176
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 7, which took 0.013704 s (model generation: 0.012446,  model checking: 0.001258):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176},
Q_f={q_gen_6176},
Delta=
{
<nil, nil>() -> q_gen_6176
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.016010 s (model generation: 0.012280,  model checking: 0.003730):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2  ;  (sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Yes: ((insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]), {
_pk -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.013862 s (model generation: 0.013661,  model checking: 0.000201):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 3  ;  () -> sorted([nil]) -> 3  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 3
}
Sat witness: Yes: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.013175 s (model generation: 0.012894,  model checking: 0.000281):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Yes: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 11, which took 0.014678 s (model generation: 0.012300,  model checking: 0.002378):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 12, which took 0.015046 s (model generation: 0.013497,  model checking: 0.001549):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 13, which took 0.020011 s (model generation: 0.012041,  model checking: 0.007970):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 14, which took 0.014506 s (model generation: 0.009676,  model checking: 0.004830):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, b>() -> q_gen_6188
<b, nil>() -> q_gen_6189
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.026640 s (model generation: 0.011693,  model checking: 0.014947):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, nil>() -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  () -> sorted([cons(x, nil)]) -> 6  ;  () -> sorted([nil]) -> 4  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5  ;  (sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Yes: ((insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]), {
_pk -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.009498 s (model generation: 0.005438,  model checking: 0.004060):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, nil>() -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  () -> sort([nil, nil]) -> 5  ;  () -> sorted([cons(x, nil)]) -> 7  ;  () -> sorted([nil]) -> 5  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 6  ;  (sort([l, _zk])) -> sorted([_zk]) -> 6
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.009866 s (model generation: 0.006295,  model checking: 0.003571):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190},
Q_f={q_gen_6176},
Delta=
{
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, nil>() -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  () -> sort([nil, nil]) -> 6  ;  () -> sorted([cons(x, nil)]) -> 7  ;  () -> sorted([nil]) -> 6  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7  ;  (sort([l, _zk])) -> sorted([_zk]) -> 7
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(b, cons(b, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.026094 s (model generation: 0.009308,  model checking: 0.016786):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<nil>() -> q_gen_6218
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  () -> sorted([cons(x, nil)]) -> 8  ;  () -> sorted([nil]) -> 7  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 8  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 8  ;  (sort([l, _zk])) -> sorted([_zk]) -> 8
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 19, which took 0.018307 s (model generation: 0.007285,  model checking: 0.011022):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<a, b>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<nil>() -> q_gen_6218
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 8  ;  () -> sort([nil, nil]) -> 8  ;  () -> sorted([cons(x, nil)]) -> 9  ;  () -> sorted([nil]) -> 8  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 9  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 9  ;  (sort([l, _zk])) -> sorted([_zk]) -> 9
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(a, cons(a, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 20, which took 0.018660 s (model generation: 0.008362,  model checking: 0.010298):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<a, b>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<nil>() -> q_gen_6218
<a>() -> q_gen_6219
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 9  ;  () -> sort([nil, nil]) -> 9  ;  () -> sorted([cons(x, nil)]) -> 10  ;  () -> sorted([nil]) -> 9  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 10  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 10  ;  (sort([l, _zk])) -> sorted([_zk]) -> 10
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(b, cons(b, cons(b, nil)))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 21, which took 0.019530 s (model generation: 0.009247,  model checking: 0.010283):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<a, b>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<cons>(q_gen_6219, q_gen_6218) -> q_gen_6218
<nil>() -> q_gen_6218
<a>() -> q_gen_6219
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 11  ;  () -> leq([a, y]) -> 11  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  () -> sorted([cons(x, nil)]) -> 11  ;  () -> sorted([nil]) -> 10  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 11  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15  ;  (leq([b, a])) -> BOT -> 11  ;  (sort([l, _zk])) -> sorted([_zk]) -> 11
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> cons(a, nil)  ;  _vk -> cons(b, cons(b, nil))  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 22, which took 0.020696 s (model generation: 0.010622,  model checking: 0.010074):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186},
Q_f={q_gen_6179},
Delta=
{
<cons>(q_gen_6181, q_gen_6180) -> q_gen_6180
<nil>() -> q_gen_6180
<a>() -> q_gen_6181
<b>() -> q_gen_6181
<cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6183
<nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6183
<cons, a>(q_gen_6181, q_gen_6180) -> q_gen_6184
<cons, b>(q_gen_6181, q_gen_6180) -> q_gen_6184
<nil, a>() -> q_gen_6184
<nil, b>() -> q_gen_6184
<a, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<b, cons>(q_gen_6181, q_gen_6180) -> q_gen_6185
<a, a>() -> q_gen_6186
<a, b>() -> q_gen_6186
<b, a>() -> q_gen_6186
<b, b>() -> q_gen_6186
<a, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<a, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
<b, cons, cons>(q_gen_6186, q_gen_6185, q_gen_6184, q_gen_6183) -> q_gen_6179
<b, nil, cons>(q_gen_6181, q_gen_6180) -> q_gen_6179
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_6176, q_gen_6188, q_gen_6189, q_gen_6190, q_gen_6218, q_gen_6219},
Q_f={q_gen_6176},
Delta=
{
<cons>(q_gen_6219, q_gen_6218) -> q_gen_6218
<nil>() -> q_gen_6218
<a>() -> q_gen_6219
<b>() -> q_gen_6219
<cons, cons>(q_gen_6190, q_gen_6189, q_gen_6188, q_gen_6176) -> q_gen_6176
<nil, cons>(q_gen_6219, q_gen_6218) -> q_gen_6176
<nil, nil>() -> q_gen_6176
<cons, b>(q_gen_6219, q_gen_6218) -> q_gen_6188
<nil, a>() -> q_gen_6188
<nil, b>() -> q_gen_6188
<a, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<a, nil>() -> q_gen_6189
<b, cons>(q_gen_6219, q_gen_6218) -> q_gen_6189
<b, nil>() -> q_gen_6189
<a, a>() -> q_gen_6190
<a, b>() -> q_gen_6190
<b, a>() -> q_gen_6190
<b, b>() -> q_gen_6190
}

Datatype: <eltlist, eltlist>
Convolution form: complete
}}}
  ;  sorted -> 
{{{
Q={q_gen_6173, q_gen_6175},
Q_f={q_gen_6173},
Delta=
{
<cons>(q_gen_6175, q_gen_6173) -> q_gen_6173
<nil>() -> q_gen_6173
<a>() -> q_gen_6175
<b>() -> q_gen_6175
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 12  ;  () -> leq([a, y]) -> 12  ;  () -> leq([b, b]) -> 11  ;  () -> sort([nil, nil]) -> 11  ;  () -> sorted([cons(x, nil)]) -> 12  ;  () -> sorted([nil]) -> 11  ;  (insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 12  ;  (insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 22  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 12  ;  (sort([l, _zk])) -> sorted([_zk]) -> 12
}
Sat witness: Yes: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> cons(b, nil)  ;  _vk -> cons(a, cons(b, nil))  ;  y -> b  ;  z -> cons(b, nil)
})

Total time: 0.357919
Reason for stopping: Proved