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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)])}
(append([_pn, _qn, _rn]) /\ append([_pn, _qn, _sn])) -> eq_eltlist([_rn, _sn])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un])}
(reverse([_vn, _wn]) /\ reverse([_vn, _xn])) -> eq_eltlist([_wn, _xn])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
(invsorted, P:
{() -> invsorted([cons(x, nil)])
() -> invsorted([nil])}
)
}

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


over-approximation: {append, leq, reverse, sorted}
under-approximation: {invsorted, leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 0
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 0
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 0
(leq([b, a])) -> BOT -> 0
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 0
}


Solving took 0.587345 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<a, b>() -> q_gen_3567
<b, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010374 s (model generation: 0.010146,  model checking: 0.000228):

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

}

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.009033 s (model generation: 0.008960,  model checking: 0.000073):

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

}

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.011214 s (model generation: 0.011149,  model checking: 0.000065):

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

}

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.008757 s (model generation: 0.008722,  model checking: 0.000035):

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

}

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.008887 s (model generation: 0.008846,  model checking: 0.000041):

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

}

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.013024 s (model generation: 0.012974,  model checking: 0.000050):

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

}

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 0
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> invsorted([nil]), {

})

-------------------------------------------
Step 6, which took 0.036735 s (model generation: 0.010541,  model checking: 0.026194):

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

}

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

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> invsorted([cons(x, nil)]) -> 3
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> invsorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 7, which took 0.011066 s (model generation: 0.010914,  model checking: 0.000152):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> invsorted([cons(x, nil)]) -> 3
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.011163 s (model generation: 0.009075,  model checking: 0.002088):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> invsorted([cons(x, nil)]) -> 3
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 1
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 2
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.009597 s (model generation: 0.009438,  model checking: 0.000159):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567},
Q_f={q_gen_3564},
Delta=
{
<nil, nil>() -> q_gen_3566
<b, b>() -> q_gen_3567
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> invsorted([cons(x, nil)]) -> 3
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 2
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 4
(leq([b, a])) -> BOT -> 3
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 3
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.010054 s (model generation: 0.009880,  model checking: 0.000174):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567},
Q_f={q_gen_3564},
Delta=
{
<nil, nil>() -> q_gen_3566
<b, b>() -> q_gen_3567
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> invsorted([cons(x, nil)]) -> 3
() -> invsorted([nil]) -> 3
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 3
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.012576 s (model generation: 0.012432,  model checking: 0.000144):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567},
Q_f={q_gen_3564},
Delta=
{
<nil, nil>() -> q_gen_3566
<b, b>() -> q_gen_3567
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> invsorted([cons(x, nil)]) -> 6
() -> invsorted([nil]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 4
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 4
}
Sat witness: Found: (() -> invsorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.010905 s (model generation: 0.010633,  model checking: 0.000272):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567},
Q_f={q_gen_3564},
Delta=
{
<nil, nil>() -> q_gen_3566
<b, b>() -> q_gen_3567
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> invsorted([cons(x, nil)]) -> 6
() -> invsorted([nil]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 4
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 13, which took 0.018217 s (model generation: 0.016178,  model checking: 0.002039):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567},
Q_f={q_gen_3564},
Delta=
{
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> invsorted([cons(x, nil)]) -> 6
() -> invsorted([nil]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 4
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 5
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.015165 s (model generation: 0.015023,  model checking: 0.000142):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> invsorted([cons(x, nil)]) -> 6
() -> invsorted([nil]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 7
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 5
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> nil  ;  _un -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.013820 s (model generation: 0.012207,  model checking: 0.001613):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> invsorted([cons(x, nil)]) -> 7
() -> invsorted([nil]) -> 5
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> reverse([nil, nil]) -> 5
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 5
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 7
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 10
(leq([b, a])) -> BOT -> 6
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 6
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.017764 s (model generation: 0.017345,  model checking: 0.000419):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> invsorted([cons(x, nil)]) -> 7
() -> invsorted([nil]) -> 6
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> reverse([nil, nil]) -> 6
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 6
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 10
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 10
(leq([b, a])) -> BOT -> 7
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 7
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> nil  ;  _un -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.017354 s (model generation: 0.015222,  model checking: 0.002132):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> invsorted([cons(x, nil)]) -> 8
() -> invsorted([nil]) -> 7
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 7
() -> reverse([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 8
() -> sorted([nil]) -> 7
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 10
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 13
(leq([b, a])) -> BOT -> 8
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 8
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.013546 s (model generation: 0.012918,  model checking: 0.000628):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, b, a>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> invsorted([cons(x, nil)]) -> 9
() -> invsorted([nil]) -> 8
() -> leq([a, y]) -> 9
() -> leq([b, b]) -> 8
() -> reverse([nil, nil]) -> 8
() -> sorted([cons(x, nil)]) -> 9
() -> sorted([nil]) -> 8
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 13
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 13
(leq([b, a])) -> BOT -> 9
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 9
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> nil  ;  _un -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.017708 s (model generation: 0.015635,  model checking: 0.002073):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, b, a>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> invsorted([cons(x, nil)]) -> 10
() -> invsorted([nil]) -> 9
() -> leq([a, y]) -> 10
() -> leq([b, b]) -> 9
() -> reverse([nil, nil]) -> 9
() -> sorted([cons(x, nil)]) -> 10
() -> sorted([nil]) -> 9
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 13
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 16
(leq([b, a])) -> BOT -> 10
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 10
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.017577 s (model generation: 0.016662,  model checking: 0.000915):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> invsorted([cons(x, nil)]) -> 11
() -> invsorted([nil]) -> 10
() -> leq([a, y]) -> 11
() -> leq([b, b]) -> 10
() -> reverse([nil, nil]) -> 10
() -> sorted([cons(x, nil)]) -> 11
() -> sorted([nil]) -> 10
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 16
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 16
(leq([b, a])) -> BOT -> 11
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 11
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> cons(b, nil)  ;  _un -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.021517 s (model generation: 0.019930,  model checking: 0.001587):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> invsorted([cons(x, nil)]) -> 12
() -> invsorted([nil]) -> 11
() -> leq([a, y]) -> 12
() -> leq([b, b]) -> 11
() -> reverse([nil, nil]) -> 11
() -> sorted([cons(x, nil)]) -> 12
() -> sorted([nil]) -> 11
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 16
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 19
(leq([b, a])) -> BOT -> 12
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 12
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.020135 s (model generation: 0.019201,  model checking: 0.000934):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> invsorted([cons(x, nil)]) -> 13
() -> invsorted([nil]) -> 12
() -> leq([a, y]) -> 13
() -> leq([b, b]) -> 12
() -> reverse([nil, nil]) -> 12
() -> sorted([cons(x, nil)]) -> 13
() -> sorted([nil]) -> 12
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 19
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 19
(leq([b, a])) -> BOT -> 13
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 13
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> nil  ;  _un -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.024840 s (model generation: 0.022725,  model checking: 0.002115):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> invsorted([cons(x, nil)]) -> 14
() -> invsorted([nil]) -> 13
() -> leq([a, y]) -> 14
() -> leq([b, b]) -> 13
() -> reverse([nil, nil]) -> 13
() -> sorted([cons(x, nil)]) -> 14
() -> sorted([nil]) -> 13
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 19
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 22
(leq([b, a])) -> BOT -> 14
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 14
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.026023 s (model generation: 0.025024,  model checking: 0.000999):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> invsorted([cons(x, nil)]) -> 15
() -> invsorted([nil]) -> 14
() -> leq([a, y]) -> 15
() -> leq([b, b]) -> 14
() -> reverse([nil, nil]) -> 14
() -> sorted([cons(x, nil)]) -> 15
() -> sorted([nil]) -> 14
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 22
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 22
(leq([b, a])) -> BOT -> 15
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 15
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> cons(a, nil)  ;  _un -> cons(a, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.029696 s (model generation: 0.025422,  model checking: 0.004274):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> invsorted([cons(x, nil)]) -> 16
() -> invsorted([nil]) -> 15
() -> leq([a, y]) -> 16
() -> leq([b, b]) -> 15
() -> reverse([nil, nil]) -> 15
() -> sorted([cons(x, nil)]) -> 16
() -> sorted([nil]) -> 15
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 22
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 25
(leq([b, a])) -> BOT -> 16
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 16
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.032606 s (model generation: 0.031601,  model checking: 0.001005):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> invsorted([cons(x, nil)]) -> 17
() -> invsorted([nil]) -> 16
() -> leq([a, y]) -> 17
() -> leq([b, b]) -> 16
() -> reverse([nil, nil]) -> 16
() -> sorted([cons(x, nil)]) -> 17
() -> sorted([nil]) -> 16
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 25
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 25
(leq([b, a])) -> BOT -> 17
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 17
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> nil  ;  _un -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.039694 s (model generation: 0.035009,  model checking: 0.004685):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<b, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> invsorted([cons(x, nil)]) -> 18
() -> invsorted([nil]) -> 17
() -> leq([a, y]) -> 18
() -> leq([b, b]) -> 17
() -> reverse([nil, nil]) -> 17
() -> sorted([cons(x, nil)]) -> 18
() -> sorted([nil]) -> 17
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 25
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 28
(leq([b, a])) -> BOT -> 18
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 18
}
Sat witness: Found: ((append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]), {
_on -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.045522 s (model generation: 0.044110,  model checking: 0.001412):

Model:
|_
{
append -> 
{{{
Q={q_gen_3564, q_gen_3566, q_gen_3567, q_gen_3579, q_gen_3580, q_gen_3581},
Q_f={q_gen_3564},
Delta=
{
<cons>(q_gen_3580, q_gen_3579) -> q_gen_3579
<nil>() -> q_gen_3579
<a>() -> q_gen_3580
<b>() -> q_gen_3580
<cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3566
<nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3566
<nil, nil>() -> q_gen_3566
<a, a>() -> q_gen_3567
<a, b>() -> q_gen_3567
<b, a>() -> q_gen_3567
<b, b>() -> q_gen_3567
<cons, cons, cons>(q_gen_3581, q_gen_3564) -> q_gen_3564
<cons, nil, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, cons, cons>(q_gen_3567, q_gen_3566) -> q_gen_3564
<nil, nil, cons>(q_gen_3580, q_gen_3579) -> q_gen_3564
<nil, nil, nil>() -> q_gen_3564
<a, a, a>() -> q_gen_3581
<a, b, a>() -> q_gen_3581
<b, a, b>() -> q_gen_3581
<b, b, b>() -> q_gen_3581
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  invsorted -> 
{{{
Q={q_gen_3561, q_gen_3563},
Q_f={q_gen_3561},
Delta=
{
<cons>(q_gen_3563, q_gen_3561) -> q_gen_3561
<nil>() -> q_gen_3561
<a>() -> q_gen_3563
<b>() -> q_gen_3563
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> invsorted([cons(x, nil)]) -> 19
() -> invsorted([nil]) -> 18
() -> leq([a, y]) -> 19
() -> leq([b, b]) -> 18
() -> reverse([nil, nil]) -> 18
() -> sorted([cons(x, nil)]) -> 19
() -> sorted([nil]) -> 18
(append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]) -> 28
(append([t1, l2, _on])) -> append([cons(h1, t1), l2, cons(h1, _on)]) -> 28
(leq([b, a])) -> BOT -> 19
(reverse([l, _yn]) /\ sorted([l])) -> invsorted([_yn]) -> 19
}
Sat witness: Found: ((append([_tn, cons(h1, nil), _un]) /\ reverse([t1, _tn])) -> reverse([cons(h1, t1), _un]), {
_tn -> cons(b, nil)  ;  _un -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

Total time: 0.587345
Reason for stopping: Proved