Solving ../../benchmarks/true/sort_append.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_yi, _zi, _aj]) /\ insert([_yi, _zi, _bj])) -> eq_eltlist([_aj, _bj])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj])}
(sort([_ej, _fj]) /\ sort([_ej, _gj])) -> eq_eltlist([_fj, _gj])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)])}
(append([_ij, _jj, _kj]) /\ append([_ij, _jj, _lj])) -> eq_eltlist([_kj, _lj])
)
}

properties:
{(append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj])}


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

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  ;  () -> sort([nil, nil]) -> 0  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 0  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 0  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 0  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 0  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0  ;  (leq([b, a])) -> BOT -> 0
}


Solving took 30.456470 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5612, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5620, q_gen_5621, q_gen_5622, q_gen_5623, q_gen_5636, q_gen_5637, q_gen_5638, q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5653, q_gen_5654, q_gen_5655, q_gen_5656, q_gen_5657, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5675, q_gen_5676, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5685, q_gen_5686, q_gen_5687, q_gen_5688, q_gen_5689, q_gen_5700, q_gen_5701, q_gen_5702, q_gen_5703, q_gen_5704, q_gen_5705, q_gen_5706, q_gen_5707, q_gen_5708, q_gen_5715, q_gen_5716, q_gen_5717},
Q_f={},
Delta=
{
<nil>() -> q_gen_5640
<b>() -> q_gen_5641
<a>() -> q_gen_5656
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5688
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<b, nil>() -> q_gen_5615
<b, b>() -> q_gen_5616
<nil, a>() -> q_gen_5621
<a, nil>() -> q_gen_5622
<a, a>() -> q_gen_5623
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5638
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5639
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5642
<cons, cons>(q_gen_5623, q_gen_5622, q_gen_5621, q_gen_5613) -> q_gen_5654
<cons, b>(q_gen_5656, q_gen_5640) -> q_gen_5655
<b, cons>(q_gen_5656, q_gen_5640) -> q_gen_5657
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5659
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5660
<cons, cons>(q_gen_5616, q_gen_5642, q_gen_5639, q_gen_5638) -> q_gen_5686
<cons, b>(q_gen_5641, q_gen_5688) -> q_gen_5687
<b, cons>(q_gen_5641, q_gen_5688) -> q_gen_5689
<nil, cons>(q_gen_5656, q_gen_5640) -> q_gen_5702
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5704
<cons, cons>(q_gen_5623, q_gen_5660, q_gen_5659, q_gen_5638) -> q_gen_5706
<cons, a>(q_gen_5656, q_gen_5688) -> q_gen_5707
<a, cons>(q_gen_5656, q_gen_5688) -> q_gen_5708
<cons, a>(q_gen_5656, q_gen_5640) -> q_gen_5716
<a, cons>(q_gen_5656, q_gen_5640) -> q_gen_5717
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5612
<nil, cons, cons>(q_gen_5623, q_gen_5622, q_gen_5621, q_gen_5613) -> q_gen_5620
<cons, nil, cons>(q_gen_5623, q_gen_5622, q_gen_5621, q_gen_5613) -> q_gen_5636
<nil, cons, cons>(q_gen_5616, q_gen_5642, q_gen_5639, q_gen_5638) -> q_gen_5637
<cons, nil, cons>(q_gen_5616, q_gen_5657, q_gen_5655, q_gen_5654) -> q_gen_5653
<nil, cons, cons>(q_gen_5623, q_gen_5660, q_gen_5659, q_gen_5638) -> q_gen_5658
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5675
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5677) -> q_gen_5676
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5677
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
<nil, cons, cons>(q_gen_5616, q_gen_5689, q_gen_5687, q_gen_5686) -> q_gen_5685
<nil, nil, cons>(q_gen_5656, q_gen_5640) -> q_gen_5700
<cons, nil, cons>(q_gen_5616, q_gen_5657, q_gen_5614, q_gen_5702) -> q_gen_5701
<cons, nil, cons>(q_gen_5623, q_gen_5660, q_gen_5621, q_gen_5704) -> q_gen_5703
<nil, cons, cons>(q_gen_5623, q_gen_5708, q_gen_5707, q_gen_5706) -> q_gen_5705
<cons, nil, cons>(q_gen_5623, q_gen_5717, q_gen_5716, q_gen_5654) -> q_gen_5715
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5599, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5609, q_gen_5610, q_gen_5611, q_gen_5618, q_gen_5619, q_gen_5624, q_gen_5625, q_gen_5626, q_gen_5627, q_gen_5631, q_gen_5632, q_gen_5633, q_gen_5634, q_gen_5635, q_gen_5643, q_gen_5644, q_gen_5645, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5652, q_gen_5661, q_gen_5662, q_gen_5663, q_gen_5664, q_gen_5670, q_gen_5671, q_gen_5672, q_gen_5673, q_gen_5674, q_gen_5690, q_gen_5691, q_gen_5692, q_gen_5693, q_gen_5694, q_gen_5695, q_gen_5709, q_gen_5710, q_gen_5718, q_gen_5723, q_gen_5724, q_gen_5725, q_gen_5726, q_gen_5727},
Q_f={},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5635
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5674
<cons>(q_gen_5597, q_gen_5635) -> q_gen_5710
<cons>(q_gen_5597, q_gen_5674) -> q_gen_5727
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, a>() -> q_gen_5603
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5610
<a, a>() -> q_gen_5611
<nil, b>() -> q_gen_5625
<b, b>() -> q_gen_5626
<cons, cons>(q_gen_5626, q_gen_5602, q_gen_5625, q_gen_5600) -> q_gen_5632
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5633
<a, cons>(q_gen_5597, q_gen_5635) -> q_gen_5634
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5644
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5645
<cons, cons>(q_gen_5611, q_gen_5610, q_gen_5601, q_gen_5600) -> q_gen_5650
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5651
<a, cons>(q_gen_5619, q_gen_5635) -> q_gen_5652
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5662
<b, cons>(q_gen_5597, q_gen_5635) -> q_gen_5663
<cons, cons>(q_gen_5611, q_gen_5645, q_gen_5601, q_gen_5644) -> q_gen_5672
<a, cons>(q_gen_5619, q_gen_5674) -> q_gen_5673
<cons, cons>(q_gen_5692, q_gen_5645, q_gen_5625, q_gen_5644) -> q_gen_5691
<a, b>() -> q_gen_5692
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5693
<b, cons>(q_gen_5597, q_gen_5674) -> q_gen_5694
<cons, cons>(q_gen_5626, q_gen_5694, q_gen_5693, q_gen_5691) -> q_gen_5724
<cons, b>(q_gen_5597, q_gen_5674) -> q_gen_5725
<b, cons>(q_gen_5597, q_gen_5727) -> q_gen_5726
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5599
<b, cons, cons>(q_gen_5611, q_gen_5610, q_gen_5601, q_gen_5600) -> q_gen_5609
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5618
<b, cons, cons>(q_gen_5626, q_gen_5602, q_gen_5625, q_gen_5600) -> q_gen_5624
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
<b, cons, cons>(q_gen_5611, q_gen_5634, q_gen_5633, q_gen_5632) -> q_gen_5631
<a, cons, cons>(q_gen_5611, q_gen_5645, q_gen_5601, q_gen_5644) -> q_gen_5643
<b, cons, cons>(q_gen_5611, q_gen_5652, q_gen_5651, q_gen_5650) -> q_gen_5649
<b, cons, cons>(q_gen_5626, q_gen_5663, q_gen_5662, q_gen_5632) -> q_gen_5661
<b, nil, cons>(q_gen_5597, q_gen_5635) -> q_gen_5664
<b, cons, cons>(q_gen_5611, q_gen_5645, q_gen_5601, q_gen_5644) -> q_gen_5670
<b, cons, cons>(q_gen_5611, q_gen_5673, q_gen_5651, q_gen_5672) -> q_gen_5671
<b, cons, cons>(q_gen_5626, q_gen_5694, q_gen_5693, q_gen_5691) -> q_gen_5690
<b, nil, cons>(q_gen_5597, q_gen_5674) -> q_gen_5695
<b, nil, cons>(q_gen_5597, q_gen_5710) -> q_gen_5709
<a, nil, cons>(q_gen_5619, q_gen_5674) -> q_gen_5718
<b, cons, cons>(q_gen_5626, q_gen_5726, q_gen_5725, q_gen_5724) -> q_gen_5723
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5604, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5629, q_gen_5630, q_gen_5646, q_gen_5647, q_gen_5648, q_gen_5665, q_gen_5666, q_gen_5667, q_gen_5668, q_gen_5669, q_gen_5696, q_gen_5697, q_gen_5698, q_gen_5699, q_gen_5711, q_gen_5712, q_gen_5713, q_gen_5714, q_gen_5719, q_gen_5720, q_gen_5721, q_gen_5722},
Q_f={},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<a>() -> q_gen_5698
<cons>(q_gen_5668, q_gen_5667) -> q_gen_5713
<nil, nil>() -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5604
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5629, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, nil>() -> q_gen_5629
<a, b>() -> q_gen_5630
<cons, cons>(q_gen_5648, q_gen_5629, q_gen_5647, q_gen_5592) -> q_gen_5646
<nil, a>() -> q_gen_5647
<a, a>() -> q_gen_5648
<cons, cons>(q_gen_5607, q_gen_5669, q_gen_5605, q_gen_5666) -> q_gen_5665
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5666
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5669
<cons, cons>(q_gen_5607, q_gen_5699, q_gen_5605, q_gen_5697) -> q_gen_5696
<nil, cons>(q_gen_5698, q_gen_5667) -> q_gen_5697
<b, cons>(q_gen_5698, q_gen_5667) -> q_gen_5699
<cons, cons>(q_gen_5607, q_gen_5714, q_gen_5605, q_gen_5712) -> q_gen_5711
<nil, cons>(q_gen_5668, q_gen_5713) -> q_gen_5712
<b, cons>(q_gen_5668, q_gen_5713) -> q_gen_5714
<cons, cons>(q_gen_5648, q_gen_5720, q_gen_5647, q_gen_5697) -> q_gen_5719
<a, cons>(q_gen_5698, q_gen_5667) -> q_gen_5720
<cons, cons>(q_gen_5648, q_gen_5722, q_gen_5647, q_gen_5666) -> q_gen_5721
<a, cons>(q_gen_5668, q_gen_5667) -> q_gen_5722
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004539 s (model generation: 0.003884,  model checking: 0.000655):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  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
}}}

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.003522 s (model generation: 0.003502,  model checking: 0.000020):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  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_5592},
Q_f={q_gen_5592},
Delta=
{
<nil, nil>() -> q_gen_5592
}

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([b, b]), {

})

-------------------------------------------
Step 2, which took 0.003518 s (model generation: 0.003492,  model checking: 0.000026):

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

}

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

}

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

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

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 3, which took 0.003567 s (model generation: 0.003465,  model checking: 0.000102):

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

}

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

}

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

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

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.004304 s (model generation: 0.003972,  model checking: 0.000332):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

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

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 5, which took 0.005137 s (model generation: 0.004353,  model checking: 0.000784):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

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

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 6, which took 0.005406 s (model generation: 0.005175,  model checking: 0.000231):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

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

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 1  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 7, which took 0.007928 s (model generation: 0.005861,  model checking: 0.002067):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 1  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 1  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]), {
_xi -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.010952 s (model generation: 0.010570,  model checking: 0.000382):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 2  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.007687 s (model generation: 0.007678,  model checking: 0.000009):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<b, nil>() -> q_gen_5615
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 3  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 2  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.008567 s (model generation: 0.008161,  model checking: 0.000406):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<b, nil>() -> q_gen_5615
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 3  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.008575 s (model generation: 0.006926,  model checking: 0.001649):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<b, nil>() -> q_gen_5615
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 4  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.016770 s (model generation: 0.013201,  model checking: 0.003569):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<b, nil>() -> q_gen_5615
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 4  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.025466 s (model generation: 0.011451,  model checking: 0.014015):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 4  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 14, which took 0.012943 s (model generation: 0.008837,  model checking: 0.004106):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 4  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 4  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.024695 s (model generation: 0.013649,  model checking: 0.011046):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, b>() -> q_gen_5607
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 4  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]), {
_xi -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.006056 s (model generation: 0.005869,  model checking: 0.000187):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, b>() -> q_gen_5607
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 4  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]), {
_mj -> cons(b, nil)  ;  _nj -> nil  ;  _oj -> cons(a, nil)  ;  l -> nil
})

-------------------------------------------
Step 17, which took 0.010689 s (model generation: 0.009049,  model checking: 0.001640):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5621, q_gen_5636},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<nil, a>() -> q_gen_5621
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5621, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5621, q_gen_5613) -> q_gen_5636
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<a>() -> q_gen_5597
<b>() -> q_gen_5597
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, b>() -> q_gen_5607
<b, b>() -> q_gen_5607
}

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

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

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  ;  () -> sort([nil, nil]) -> 4  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 7  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.024802 s (model generation: 0.016336,  model checking: 0.008466):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616},
Q_f={q_gen_5598},
Delta=
{
<nil, nil>() -> q_gen_5613
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  () -> sort([nil, nil]) -> 5  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 7  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 19, which took 0.040564 s (model generation: 0.017349,  model checking: 0.023215):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5629},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<a, b>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5607, q_gen_5629, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, nil>() -> q_gen_5629
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  () -> sort([nil, nil]) -> 6  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 7  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 20, which took 0.010891 s (model generation: 0.006334,  model checking: 0.004557):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5629},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, b>() -> q_gen_5605
<b, nil>() -> q_gen_5606
<a, b>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5607, q_gen_5629, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, nil>() -> q_gen_5629
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 7  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 7  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 21, which took 0.021197 s (model generation: 0.006710,  model checking: 0.014487):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 7  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 7  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 10  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8
}
Sat witness: Yes: ((insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]), {
_xi -> cons(a, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 22, which took 0.018185 s (model generation: 0.006958,  model checking: 0.011227):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 10  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 8  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 10  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 8
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.010878 s (model generation: 0.007507,  model checking: 0.003371):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 8  ;  () -> sort([nil, nil]) -> 8  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 10  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 9  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 10  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 9
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 24, which took 0.126186 s (model generation: 0.007936,  model checking: 0.118250):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 9  ;  () -> sort([nil, nil]) -> 9  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 10  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 10  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 10  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 10
}
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 25, which took 0.014447 s (model generation: 0.009819,  model checking: 0.004628):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630},
Q_f={q_gen_5592},
Delta=
{
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 10  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 10  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 10  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(b, cons(b, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 26, which took 0.045473 s (model generation: 0.009510,  model checking: 0.035963):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 10  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 10  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 13  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11
}
Sat witness: Yes: ((insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]), {
_xi -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 1.110322 s (model generation: 0.011338,  model checking: 1.098984):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 13  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 11  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 13  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.026027 s (model generation: 0.012475,  model checking: 0.013552):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 11  ;  () -> leq([a, y]) -> 11  ;  () -> leq([b, b]) -> 11  ;  () -> sort([nil, nil]) -> 11  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 13  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 12  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 13  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 12
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 29, which took 0.028740 s (model generation: 0.012800,  model checking: 0.015940):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 12  ;  () -> leq([a, y]) -> 12  ;  () -> leq([b, b]) -> 12  ;  () -> sort([nil, nil]) -> 12  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 13  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 13  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 13  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 13
}
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 30, which took 0.023797 s (model generation: 0.014200,  model checking: 0.009597):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> sort([nil, nil]) -> 13  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 13  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 13  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 13  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 14
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(b, cons(a, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 31, which took 2.137622 s (model generation: 0.016837,  model checking: 2.120785):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> sort([nil, nil]) -> 13  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 16  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 14  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 14  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 14
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 32, which took 2.037212 s (model generation: 0.016349,  model checking: 2.020863):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> insert([x, nil, cons(x, nil)]) -> 14  ;  () -> leq([a, y]) -> 14  ;  () -> leq([b, b]) -> 14  ;  () -> sort([nil, nil]) -> 14  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 16  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 17  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 15  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 15
}
Sat witness: Yes: ((append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]), {
_mj -> cons(a, nil)  ;  _nj -> nil  ;  _oj -> cons(a, cons(b, nil))  ;  l -> nil
})

-------------------------------------------
Step 33, which took 2.009038 s (model generation: 0.017738,  model checking: 1.991300):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5660, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5703},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5660
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
<cons, nil, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5703
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> insert([x, nil, cons(x, nil)]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> sort([nil, nil]) -> 15  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 16  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 17  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 16  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16  ;  (leq([b, a])) -> BOT -> 16
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 34, which took 0.037883 s (model generation: 0.019502,  model checking: 0.018381):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5660, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5703},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<cons, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5660
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5598) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
<cons, nil, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5703
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> insert([x, nil, cons(x, nil)]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> sort([nil, nil]) -> 16  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 16  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 17  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 16  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 17  ;  (leq([b, a])) -> BOT -> 17
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(b, cons(b, cons(b, nil)))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 35, which took 2.023772 s (model generation: 0.019857,  model checking: 2.003915):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5660, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<cons, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5660
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5677) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5660, q_gen_5614, q_gen_5613) -> q_gen_5677
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5677
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<cons>(q_gen_5668, q_gen_5667) -> q_gen_5667
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> insert([x, nil, cons(x, nil)]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> sort([nil, nil]) -> 16  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 19  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 17  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 17  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 19  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 17  ;  (leq([b, a])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]), {
_hj -> cons(a, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 36, which took 2.053771 s (model generation: 0.021693,  model checking: 2.032078):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5702},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5702
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5677) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5702) -> q_gen_5677
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5677
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<cons>(q_gen_5668, q_gen_5667) -> q_gen_5667
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> insert([x, nil, cons(x, nil)]) -> 17  ;  () -> leq([a, y]) -> 17  ;  () -> leq([b, b]) -> 17  ;  () -> sort([nil, nil]) -> 17  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 19  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 18  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 18  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 22  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 18
}
Sat witness: Yes: ((insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]), {
_cj -> nil  ;  _dj -> cons(a, cons(a, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 37, which took 2.037249 s (model generation: 0.024055,  model checking: 2.013194):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5702},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5702
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5677) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5702) -> q_gen_5677
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5677
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627},
Q_f={q_gen_5595},
Delta=
{
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5596
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5596
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<cons>(q_gen_5668, q_gen_5667) -> q_gen_5667
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> insert([x, nil, cons(x, nil)]) -> 18  ;  () -> leq([a, y]) -> 18  ;  () -> leq([b, b]) -> 18  ;  () -> sort([nil, nil]) -> 18  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 19  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 21  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 19  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 22  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 19  ;  (leq([b, a])) -> BOT -> 19
}
Sat witness: Yes: ((append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]), {
_mj -> cons(a, cons(b, nil))  ;  _nj -> nil  ;  _oj -> cons(a, nil)  ;  l -> nil
})

-------------------------------------------
Step 38, which took 0.603176 s (model generation: 0.027221,  model checking: 0.575955):

Model:
|_
{
append -> 
{{{
Q={q_gen_5598, q_gen_5613, q_gen_5614, q_gen_5615, q_gen_5616, q_gen_5640, q_gen_5641, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5702},
Q_f={q_gen_5598},
Delta=
{
<cons>(q_gen_5641, q_gen_5640) -> q_gen_5640
<nil>() -> q_gen_5640
<a>() -> q_gen_5641
<b>() -> q_gen_5641
<cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5613
<nil, nil>() -> q_gen_5613
<cons, a>(q_gen_5641, q_gen_5640) -> q_gen_5614
<cons, b>(q_gen_5641, q_gen_5640) -> q_gen_5614
<nil, a>() -> q_gen_5614
<nil, b>() -> q_gen_5614
<a, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<a, nil>() -> q_gen_5615
<b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5615
<b, nil>() -> q_gen_5615
<a, a>() -> q_gen_5616
<b, b>() -> q_gen_5616
<nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5702
<cons, cons, cons>(q_gen_5684, q_gen_5683, q_gen_5682, q_gen_5681, q_gen_5680, q_gen_5679, q_gen_5678, q_gen_5677) -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, cons, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5613) -> q_gen_5598
<nil, nil, nil>() -> q_gen_5598
<cons, nil, cons>(q_gen_5616, q_gen_5615, q_gen_5614, q_gen_5702) -> q_gen_5677
<nil, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5677
<nil, nil, b>() -> q_gen_5678
<nil, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5679
<nil, b, b>() -> q_gen_5680
<b, nil, cons>(q_gen_5641, q_gen_5640) -> q_gen_5681
<b, nil, b>() -> q_gen_5682
<b, b, cons>(q_gen_5641, q_gen_5640) -> q_gen_5683
<b, b, b>() -> q_gen_5684
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  insert -> 
{{{
Q={q_gen_5595, q_gen_5596, q_gen_5597, q_gen_5600, q_gen_5601, q_gen_5602, q_gen_5603, q_gen_5619, q_gen_5627, q_gen_5635},
Q_f={q_gen_5595},
Delta=
{
<nil>() -> q_gen_5596
<b>() -> q_gen_5597
<a>() -> q_gen_5619
<cons>(q_gen_5597, q_gen_5596) -> q_gen_5635
<cons>(q_gen_5597, q_gen_5635) -> q_gen_5635
<cons>(q_gen_5619, q_gen_5596) -> q_gen_5635
<cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5600
<nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5600
<nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5600
<cons, a>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, a>(q_gen_5619, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5597, q_gen_5596) -> q_gen_5601
<cons, b>(q_gen_5619, q_gen_5596) -> q_gen_5601
<nil, a>() -> q_gen_5601
<nil, b>() -> q_gen_5601
<a, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5597, q_gen_5635) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5596) -> q_gen_5602
<a, cons>(q_gen_5619, q_gen_5635) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5596) -> q_gen_5602
<b, cons>(q_gen_5597, q_gen_5635) -> q_gen_5602
<a, a>() -> q_gen_5603
<a, b>() -> q_gen_5603
<b, a>() -> q_gen_5603
<b, b>() -> q_gen_5603
<a, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<a, nil, cons>(q_gen_5619, q_gen_5596) -> q_gen_5595
<b, cons, cons>(q_gen_5603, q_gen_5602, q_gen_5601, q_gen_5600) -> q_gen_5595
<b, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5595
<a, nil, cons>(q_gen_5597, q_gen_5596) -> q_gen_5627
<a, nil, cons>(q_gen_5619, q_gen_5635) -> q_gen_5627
<b, nil, cons>(q_gen_5597, q_gen_5635) -> q_gen_5627
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5592, q_gen_5605, q_gen_5606, q_gen_5607, q_gen_5628, q_gen_5630, q_gen_5667, q_gen_5668},
Q_f={q_gen_5592},
Delta=
{
<cons>(q_gen_5668, q_gen_5667) -> q_gen_5667
<nil>() -> q_gen_5667
<a>() -> q_gen_5668
<b>() -> q_gen_5668
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5592
<nil, nil>() -> q_gen_5592
<nil, a>() -> q_gen_5605
<nil, b>() -> q_gen_5605
<a, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<a, nil>() -> q_gen_5606
<b, cons>(q_gen_5668, q_gen_5667) -> q_gen_5606
<b, nil>() -> q_gen_5606
<a, a>() -> q_gen_5607
<b, b>() -> q_gen_5607
<cons, cons>(q_gen_5607, q_gen_5606, q_gen_5605, q_gen_5628) -> q_gen_5628
<cons, cons>(q_gen_5630, q_gen_5606, q_gen_5605, q_gen_5592) -> q_gen_5628
<nil, cons>(q_gen_5668, q_gen_5667) -> q_gen_5628
<a, b>() -> q_gen_5630
}

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

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

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  ;  () -> sort([nil, nil]) -> 19  ;  (append([t1, l2, _hj])) -> append([cons(h1, t1), l2, cons(h1, _hj)]) -> 19  ;  (append([cons(a, nil), _nj, _oj]) /\ sort([l, _nj]) /\ sort([cons(a, l), _mj])) -> eq_eltlist([_mj, _oj]) -> 21  ;  (insert([x, z, _xi]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xi)]) -> 19  ;  (insert([y, _cj, _dj]) /\ sort([z, _cj])) -> sort([cons(y, z), _dj]) -> 22  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 22  ;  (leq([b, a])) -> BOT -> 20
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, cons(a, nil))
})

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