Solving ../../benchmarks/true/sort_length_eq.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_bl, _cl, _dl]) /\ insert([_bl, _cl, _el])) -> eq_eltlist([_dl, _el])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl])}
(sort([_hl, _il]) /\ sort([_hl, _jl])) -> eq_eltlist([_il, _jl])
)
(length, F:
{() -> length([nil, z])
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)])}
(length([_ll, _ml]) /\ length([_ll, _nl])) -> eq_nat([_ml, _nl])
)
}

properties:
{(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql])}


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

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 0  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 0  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 0  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 0  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 0  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0  ;  (leq([b, a])) -> BOT -> 0
}


Solving took 30.034987 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5820, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824, q_gen_5832, q_gen_5833, q_gen_5834, q_gen_5836, q_gen_5837, q_gen_5838, q_gen_5839, q_gen_5840, q_gen_5843, q_gen_5847, q_gen_5848, q_gen_5849, q_gen_5850, q_gen_5851, q_gen_5852, q_gen_5853, q_gen_5854, q_gen_5858, q_gen_5866, q_gen_5867, q_gen_5868, q_gen_5869, q_gen_5870, q_gen_5871, q_gen_5872, q_gen_5873, q_gen_5876, q_gen_5888, q_gen_5891, q_gen_5892, q_gen_5893, q_gen_5894, q_gen_5895, q_gen_5896, q_gen_5897, q_gen_5898, q_gen_5899, q_gen_5900},
Q_f={},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<a>() -> q_gen_5837
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5851
<cons>(q_gen_5837, q_gen_5818) -> q_gen_5873
<cons>(q_gen_5819, q_gen_5851) -> q_gen_5895
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, a>() -> q_gen_5824
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5833
<a, a>() -> q_gen_5834
<nil, b>() -> q_gen_5839
<b, b>() -> q_gen_5840
<cons, cons>(q_gen_5840, q_gen_5823, q_gen_5839, q_gen_5821) -> q_gen_5848
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5849
<a, cons>(q_gen_5819, q_gen_5851) -> q_gen_5850
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5853
<b, cons>(q_gen_5819, q_gen_5851) -> q_gen_5854
<cons, cons>(q_gen_5870, q_gen_5869, q_gen_5839, q_gen_5868) -> q_gen_5867
<nil, cons>(q_gen_5837, q_gen_5818) -> q_gen_5868
<a, cons>(q_gen_5837, q_gen_5818) -> q_gen_5869
<a, b>() -> q_gen_5870
<cons, b>(q_gen_5837, q_gen_5818) -> q_gen_5871
<b, cons>(q_gen_5819, q_gen_5873) -> q_gen_5872
<cons, cons>(q_gen_5834, q_gen_5850, q_gen_5849, q_gen_5848) -> q_gen_5892
<cons, a>(q_gen_5837, q_gen_5851) -> q_gen_5893
<a, cons>(q_gen_5837, q_gen_5895) -> q_gen_5894
<cons, cons>(q_gen_5840, q_gen_5854, q_gen_5853, q_gen_5848) -> q_gen_5897
<cons, b>(q_gen_5819, q_gen_5851) -> q_gen_5898
<b, cons>(q_gen_5819, q_gen_5895) -> q_gen_5899
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5820
<b, cons, cons>(q_gen_5834, q_gen_5833, q_gen_5822, q_gen_5821) -> q_gen_5832
<a, nil, cons>(q_gen_5837, q_gen_5818) -> q_gen_5836
<b, cons, cons>(q_gen_5840, q_gen_5823, q_gen_5839, q_gen_5821) -> q_gen_5838
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5843
<b, cons, cons>(q_gen_5834, q_gen_5850, q_gen_5849, q_gen_5848) -> q_gen_5847
<b, cons, cons>(q_gen_5840, q_gen_5854, q_gen_5853, q_gen_5848) -> q_gen_5852
<a, nil, cons>(q_gen_5837, q_gen_5851) -> q_gen_5858
<b, cons, cons>(q_gen_5840, q_gen_5872, q_gen_5871, q_gen_5867) -> q_gen_5866
<b, nil, cons>(q_gen_5837, q_gen_5873) -> q_gen_5876
<a, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5888
<b, cons, cons>(q_gen_5834, q_gen_5894, q_gen_5893, q_gen_5892) -> q_gen_5891
<b, cons, cons>(q_gen_5840, q_gen_5899, q_gen_5898, q_gen_5897) -> q_gen_5896
<a, cons, cons>(q_gen_5870, q_gen_5833, q_gen_5839, q_gen_5821) -> q_gen_5900
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_5816, q_gen_5825, q_gen_5826, q_gen_5841, q_gen_5842, q_gen_5855, q_gen_5856, q_gen_5857, q_gen_5874, q_gen_5875, q_gen_5882, q_gen_5885, q_gen_5886, q_gen_5887},
Q_f={},
Delta=
{
<z>() -> q_gen_5857
<s>(q_gen_5857) -> q_gen_5887
<nil, z>() -> q_gen_5816
<cons, s>(q_gen_5826, q_gen_5816) -> q_gen_5825
<b, z>() -> q_gen_5826
<cons, s>(q_gen_5842, q_gen_5816) -> q_gen_5841
<a, z>() -> q_gen_5842
<cons, s>(q_gen_5856, q_gen_5841) -> q_gen_5855
<b, s>(q_gen_5857) -> q_gen_5856
<cons, s>(q_gen_5875, q_gen_5825) -> q_gen_5874
<a, s>(q_gen_5857) -> q_gen_5875
<cons, s>(q_gen_5856, q_gen_5825) -> q_gen_5882
<cons, s>(q_gen_5886, q_gen_5882) -> q_gen_5885
<b, s>(q_gen_5887) -> q_gen_5886
}

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5827, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5844, q_gen_5845, q_gen_5846, q_gen_5859, q_gen_5860, q_gen_5861, q_gen_5862, q_gen_5863, q_gen_5864, q_gen_5865, q_gen_5877, q_gen_5878, q_gen_5879, q_gen_5880, q_gen_5881, q_gen_5883, q_gen_5884, q_gen_5889, q_gen_5890, q_gen_5901, q_gen_5902, q_gen_5903},
Q_f={},
Delta=
{
<nil>() -> q_gen_5861
<b>() -> q_gen_5862
<a>() -> q_gen_5879
<nil, nil>() -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5827
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5846, q_gen_5845, q_gen_5828, q_gen_5813) -> q_gen_5844
<a, nil>() -> q_gen_5845
<a, b>() -> q_gen_5846
<cons, cons>(q_gen_5865, q_gen_5864, q_gen_5863, q_gen_5860) -> q_gen_5859
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
<nil, a>() -> q_gen_5863
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5864
<a, a>() -> q_gen_5865
<cons, cons>(q_gen_5881, q_gen_5880, q_gen_5863, q_gen_5878) -> q_gen_5877
<nil, cons>(q_gen_5879, q_gen_5861) -> q_gen_5878
<b, cons>(q_gen_5879, q_gen_5861) -> q_gen_5880
<b, a>() -> q_gen_5881
<cons, cons>(q_gen_5830, q_gen_5884, q_gen_5828, q_gen_5860) -> q_gen_5883
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5884
<cons, cons>(q_gen_5846, q_gen_5864, q_gen_5828, q_gen_5860) -> q_gen_5889
<cons, cons>(q_gen_5881, q_gen_5884, q_gen_5863, q_gen_5860) -> q_gen_5890
<cons, cons>(q_gen_5881, q_gen_5829, q_gen_5863, q_gen_5813) -> q_gen_5901
<cons, cons>(q_gen_5846, q_gen_5864, q_gen_5903, q_gen_5827) -> q_gen_5902
<cons, b>(q_gen_5862, q_gen_5861) -> q_gen_5903
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004586 s (model generation: 0.003876,  model checking: 0.000710):

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

}

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

}

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

}

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  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:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 0  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.003533 s (model generation: 0.003513,  model checking: 0.000020):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 0  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.003460 s (model generation: 0.003433,  model checking: 0.000027):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.003390 s (model generation: 0.003346,  model checking: 0.000044):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1  ;  (leq([b, a])) -> BOT -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 4, which took 0.003585 s (model generation: 0.003472,  model checking: 0.000113):

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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 5, which took 0.007237 s (model generation: 0.004400,  model checking: 0.002837):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.006714 s (model generation: 0.006566,  model checking: 0.000148):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4  ;  (leq([b, a])) -> BOT -> 2
}
Sat witness: Yes: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.009633 s (model generation: 0.009145,  model checking: 0.000488):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.012739 s (model generation: 0.011403,  model checking: 0.001336):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]), {
_al -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.008602 s (model generation: 0.008594,  model checking: 0.000008):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 3  ;  () -> leq([b, b]) -> 3  ;  () -> sort([nil, nil]) -> 3  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.011315 s (model generation: 0.009218,  model checking: 0.002097):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 3  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.014932 s (model generation: 0.012878,  model checking: 0.002054):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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.017362 s (model generation: 0.011627,  model checking: 0.005735):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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 13, which took 0.006247 s (model generation: 0.005092,  model checking: 0.001155):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7  ;  (leq([b, a])) -> BOT -> 5
}
Sat witness: Yes: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 14, which took 0.019908 s (model generation: 0.014239,  model checking: 0.005669):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 5  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.029126 s (model generation: 0.015259,  model checking: 0.013867):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  () -> leq([a, y]) -> 6  ;  () -> leq([b, b]) -> 4  ;  () -> sort([nil, nil]) -> 4  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 5  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]), {
_al -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 16, which took 0.009200 s (model generation: 0.006196,  model checking: 0.003004):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 5  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 5  ;  () -> sort([nil, nil]) -> 5  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 6  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 6
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.007272 s (model generation: 0.006612,  model checking: 0.000660):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 6  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 6  ;  () -> sort([nil, nil]) -> 6  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 7  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 7
}
Sat witness: Yes: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 18, which took 0.008859 s (model generation: 0.006644,  model checking: 0.002215):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830},
Q_f={q_gen_5813},
Delta=
{
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7  ;  () -> length([nil, z]) -> 7  ;  () -> leq([a, y]) -> 7  ;  () -> leq([b, b]) -> 7  ;  () -> sort([nil, nil]) -> 7  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 10  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 8  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(a, cons(b, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 19, which took 0.019022 s (model generation: 0.006910,  model checking: 0.012112):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 8  ;  () -> length([nil, z]) -> 8  ;  () -> leq([a, y]) -> 8  ;  () -> leq([b, b]) -> 8  ;  () -> sort([nil, nil]) -> 8  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 8  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 10  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 11  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 10  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10  ;  (leq([b, a])) -> BOT -> 9
}
Sat witness: Yes: ((length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]), {
_ol -> z  ;  _pl -> cons(b, nil)  ;  _ql -> s(z)  ;  l -> nil
})

-------------------------------------------
Step 20, which took 0.018353 s (model generation: 0.006777,  model checking: 0.011576):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 9  ;  () -> length([nil, z]) -> 9  ;  () -> leq([a, y]) -> 9  ;  () -> leq([b, b]) -> 9  ;  () -> sort([nil, nil]) -> 9  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 9  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 10  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 11  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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(a, nil)
})

-------------------------------------------
Step 21, which took 0.016203 s (model generation: 0.007757,  model checking: 0.008446):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> length([nil, z]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 10  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 10  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 11  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 11
}
Sat witness: Yes: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 22, which took 0.013203 s (model generation: 0.008584,  model checking: 0.004619):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, b>() -> q_gen_5830
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 10  ;  () -> length([nil, z]) -> 10  ;  () -> leq([a, y]) -> 10  ;  () -> leq([b, b]) -> 10  ;  () -> sort([nil, nil]) -> 10  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 10  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 13  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 11  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 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, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(a, cons(a, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 23, which took 0.018428 s (model generation: 0.009272,  model checking: 0.009156):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 11  ;  () -> length([nil, z]) -> 11  ;  () -> leq([a, y]) -> 11  ;  () -> leq([b, b]) -> 11  ;  () -> sort([nil, nil]) -> 11  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 11  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 13  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 14  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 13  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13  ;  (leq([b, a])) -> BOT -> 12
}
Sat witness: Yes: ((length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]), {
_ol -> s(z)  ;  _pl -> cons(b, cons(b, nil))  ;  _ql -> s(s(z))  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.020419 s (model generation: 0.009784,  model checking: 0.010635):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862, q_gen_5863},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5863, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5860
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
<nil, a>() -> q_gen_5863
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 12  ;  () -> length([nil, z]) -> 12  ;  () -> leq([a, y]) -> 12  ;  () -> leq([b, b]) -> 12  ;  () -> sort([nil, nil]) -> 12  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 12  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 13  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 14  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 13
}
Sat witness: Yes: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 25, which took 0.019406 s (model generation: 0.010012,  model checking: 0.009394):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5860, q_gen_5861, q_gen_5862, q_gen_5863},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5863, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5860
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
<nil, a>() -> q_gen_5863
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 13  ;  () -> length([nil, z]) -> 13  ;  () -> leq([a, y]) -> 13  ;  () -> leq([b, b]) -> 13  ;  () -> sort([nil, nil]) -> 13  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 13  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 16  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 14  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14  ;  (leq([b, a])) -> BOT -> 14
}
Sat witness: Yes: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(b, cons(b, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 26, which took 0.022586 s (model generation: 0.011727,  model checking: 0.010859):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824},
Q_f={q_gen_5817},
Delta=
{
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5818
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5846, q_gen_5860, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5846, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<cons, cons>(q_gen_5846, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<b, b>() -> q_gen_5830
<a, a>() -> q_gen_5846
<a, b>() -> q_gen_5846
<b, a>() -> q_gen_5846
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5860) -> q_gen_5860
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5860
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 14  ;  () -> length([nil, z]) -> 14  ;  () -> leq([a, y]) -> 14  ;  () -> leq([b, b]) -> 14  ;  () -> sort([nil, nil]) -> 14  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 14  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 16  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 17  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15  ;  (leq([b, a])) -> BOT -> 15
}
Sat witness: Yes: ((length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]), {
_ol -> s(z)  ;  _pl -> cons(a, cons(b, nil))  ;  _ql -> s(s(z))  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 0.812607 s (model generation: 0.011852,  model checking: 0.800755):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824, q_gen_5851, q_gen_5858},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5851
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
<b, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5859, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5859) -> q_gen_5859
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5859
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 14  ;  () -> length([nil, z]) -> 14  ;  () -> leq([a, y]) -> 14  ;  () -> leq([b, b]) -> 14  ;  () -> sort([nil, nil]) -> 14  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 17  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 16  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 17  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15  ;  (leq([b, a])) -> BOT -> 15
}
Sat witness: Yes: ((insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]), {
_al -> cons(a, cons(b, cons(b, nil)))  ;  x -> b  ;  y -> a  ;  z -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.043926 s (model generation: 0.013866,  model checking: 0.030060):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824, q_gen_5851, q_gen_5858},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5851
<cons>(q_gen_5819, q_gen_5851) -> q_gen_5851
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, a>(q_gen_5819, q_gen_5851) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
<b, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5859, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5859) -> q_gen_5859
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5859
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 15  ;  () -> length([nil, z]) -> 15  ;  () -> leq([a, y]) -> 15  ;  () -> leq([b, b]) -> 15  ;  () -> sort([nil, nil]) -> 15  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 17  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 16  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 17  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 16  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 16
}
Sat witness: Yes: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 29, which took 0.018530 s (model generation: 0.014399,  model checking: 0.004131):

Model:
|_
{
insert -> 
{{{
Q={q_gen_5817, q_gen_5818, q_gen_5819, q_gen_5821, q_gen_5822, q_gen_5823, q_gen_5824, q_gen_5851, q_gen_5858},
Q_f={q_gen_5817},
Delta=
{
<nil>() -> q_gen_5818
<a>() -> q_gen_5819
<b>() -> q_gen_5819
<cons>(q_gen_5819, q_gen_5818) -> q_gen_5851
<cons>(q_gen_5819, q_gen_5851) -> q_gen_5851
<cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5821
<nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5821
<cons, a>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, a>(q_gen_5819, q_gen_5851) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5818) -> q_gen_5822
<cons, b>(q_gen_5819, q_gen_5851) -> q_gen_5822
<nil, a>() -> q_gen_5822
<nil, b>() -> q_gen_5822
<a, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<a, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5818) -> q_gen_5823
<b, cons>(q_gen_5819, q_gen_5851) -> q_gen_5823
<a, a>() -> q_gen_5824
<a, b>() -> q_gen_5824
<b, a>() -> q_gen_5824
<b, b>() -> q_gen_5824
<a, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<b, cons, cons>(q_gen_5824, q_gen_5823, q_gen_5822, q_gen_5821) -> q_gen_5817
<b, nil, cons>(q_gen_5819, q_gen_5818) -> q_gen_5817
<a, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
<b, nil, cons>(q_gen_5819, q_gen_5851) -> q_gen_5858
}

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

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

Datatype: <elt, elt>
Convolution form: complete
}}}
  ;  sort -> 
{{{
Q={q_gen_5813, q_gen_5828, q_gen_5829, q_gen_5830, q_gen_5859, q_gen_5861, q_gen_5862},
Q_f={q_gen_5813},
Delta=
{
<nil>() -> q_gen_5861
<a>() -> q_gen_5862
<b>() -> q_gen_5862
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5813) -> q_gen_5813
<nil, nil>() -> q_gen_5813
<nil, a>() -> q_gen_5828
<nil, b>() -> q_gen_5828
<a, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<a, nil>() -> q_gen_5829
<b, cons>(q_gen_5862, q_gen_5861) -> q_gen_5829
<b, nil>() -> q_gen_5829
<a, a>() -> q_gen_5830
<a, b>() -> q_gen_5830
<b, a>() -> q_gen_5830
<b, b>() -> q_gen_5830
<cons, cons>(q_gen_5830, q_gen_5829, q_gen_5828, q_gen_5859) -> q_gen_5859
<nil, cons>(q_gen_5862, q_gen_5861) -> q_gen_5859
}

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 16  ;  () -> length([nil, z]) -> 16  ;  () -> leq([a, y]) -> 16  ;  () -> leq([b, b]) -> 16  ;  () -> sort([nil, nil]) -> 16  ;  (insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 17  ;  (insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 19  ;  (length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 17  ;  (length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 17  ;  (leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18  ;  (leq([b, a])) -> BOT -> 17
}
Sat witness: Yes: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> cons(a, nil)  ;  _gl -> cons(b, cons(b, nil))  ;  y -> a  ;  z -> cons(b, nil)
})

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