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


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, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)])}
(append([_ef, _ff, _gf]) /\ append([_ef, _ff, _hf])) -> eq_eltlist([_gf, _hf])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf])}
(reverse([_kf, _lf]) /\ reverse([_kf, _mf])) -> eq_eltlist([_lf, _mf])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
(invsorted, P:
{() -> invsorted([cons(x, nil)])
() -> invsorted([nil])}
)
}

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


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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 0
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 0
(leq([b, a])) -> BOT -> 0
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 0
}


Solving took 0.348657 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<a, b>() -> q_gen_1019
<b, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<cons>(q_gen_1047, q_gen_1046) -> q_gen_1046
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<cons, nil>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010439 s (model generation: 0.010010,  model checking: 0.000429):

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

}

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

}

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

}

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

}

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

}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.010320 s (model generation: 0.010187,  model checking: 0.000133):

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

}

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

}

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

}

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

}

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

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.010377 s (model generation: 0.010249,  model checking: 0.000128):

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

}

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

}

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

}

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

}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.013778 s (model generation: 0.010294,  model checking: 0.003484):

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

}

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

}

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

}

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.010470 s (model generation: 0.010369,  model checking: 0.000101):

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

}

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

}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.005310 s (model generation: 0.005280,  model checking: 0.000030):

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

}

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

}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> invsorted([nil]), {

})

-------------------------------------------
Step 6, which took 0.005115 s (model generation: 0.005000,  model checking: 0.000115):

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

}

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

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> invsorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 7, which took 0.005313 s (model generation: 0.004826,  model checking: 0.000487):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.008812 s (model generation: 0.006771,  model checking: 0.002041):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 1
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 2
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.005464 s (model generation: 0.005032,  model checking: 0.000432):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019},
Q_f={q_gen_1016},
Delta=
{
<nil, nil>() -> q_gen_1018
<b, b>() -> q_gen_1019
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 2
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(leq([b, a])) -> BOT -> 3
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 3
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 10, which took 0.005209 s (model generation: 0.004753,  model checking: 0.000456):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019},
Q_f={q_gen_1016},
Delta=
{
<nil, nil>() -> q_gen_1018
<b, b>() -> q_gen_1019
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.007031 s (model generation: 0.005656,  model checking: 0.001375):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019},
Q_f={q_gen_1016},
Delta=
{
<nil, nil>() -> q_gen_1018
<b, b>() -> q_gen_1019
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Found: (() -> invsorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.005818 s (model generation: 0.005533,  model checking: 0.000285):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019},
Q_f={q_gen_1016},
Delta=
{
<nil, nil>() -> q_gen_1018
<b, b>() -> q_gen_1019
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(leq([b, a])) -> BOT -> 4
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 13, which took 0.007222 s (model generation: 0.005639,  model checking: 0.001583):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019},
Q_f={q_gen_1016},
Delta=
{
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 5
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.007128 s (model generation: 0.006759,  model checking: 0.000369):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 7
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 5
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.008363 s (model generation: 0.006376,  model checking: 0.001987):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035},
Q_f={q_gen_1010},
Delta=
{
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 7
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10
(leq([b, a])) -> BOT -> 6
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 6
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.007493 s (model generation: 0.006808,  model checking: 0.000685):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035},
Q_f={q_gen_1010},
Delta=
{
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 10
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10
(leq([b, a])) -> BOT -> 7
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 7
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.009527 s (model generation: 0.007250,  model checking: 0.002277):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035},
Q_f={q_gen_1010},
Delta=
{
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 10
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13
(leq([b, a])) -> BOT -> 8
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 8
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.008791 s (model generation: 0.007457,  model checking: 0.001334):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, b, a>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035},
Q_f={q_gen_1010},
Delta=
{
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 13
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13
(leq([b, a])) -> BOT -> 9
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 9
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.009228 s (model generation: 0.007284,  model checking: 0.001944):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, b, a>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 13
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 16
(leq([b, a])) -> BOT -> 10
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 10
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.009627 s (model generation: 0.009035,  model checking: 0.000592):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 16
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 16
(leq([b, a])) -> BOT -> 11
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 11
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(b, nil)  ;  _jf -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.011640 s (model generation: 0.010090,  model checking: 0.001550):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 16
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 19
(leq([b, a])) -> BOT -> 12
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 12
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.012175 s (model generation: 0.010977,  model checking: 0.001198):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 19
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 19
(leq([b, a])) -> BOT -> 13
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 13
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.013800 s (model generation: 0.012010,  model checking: 0.001790):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 19
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22
(leq([b, a])) -> BOT -> 14
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 14
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.014733 s (model generation: 0.013738,  model checking: 0.000995):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 22
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22
(leq([b, a])) -> BOT -> 15
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 15
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(a, nil)  ;  _jf -> cons(a, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.025316 s (model generation: 0.019689,  model checking: 0.005627):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 22
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25
(leq([b, a])) -> BOT -> 16
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 16
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.018403 s (model generation: 0.017820,  model checking: 0.000583):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 25
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25
(leq([b, a])) -> BOT -> 17
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 17
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> nil  ;  _jf -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.023862 s (model generation: 0.018868,  model checking: 0.004994):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<b, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<cons>(q_gen_1047, q_gen_1046) -> q_gen_1046
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 25
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(leq([b, a])) -> BOT -> 18
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 18
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.025168 s (model generation: 0.023586,  model checking: 0.001582):

Model:
|_
{
append -> 
{{{
Q={q_gen_1016, q_gen_1018, q_gen_1019, q_gen_1031, q_gen_1032, q_gen_1033},
Q_f={q_gen_1016},
Delta=
{
<cons>(q_gen_1032, q_gen_1031) -> q_gen_1031
<nil>() -> q_gen_1031
<a>() -> q_gen_1032
<b>() -> q_gen_1032
<cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1018
<nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1018
<nil, nil>() -> q_gen_1018
<a, a>() -> q_gen_1019
<a, b>() -> q_gen_1019
<b, a>() -> q_gen_1019
<b, b>() -> q_gen_1019
<cons, cons, cons>(q_gen_1033, q_gen_1016) -> q_gen_1016
<cons, nil, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, cons, cons>(q_gen_1019, q_gen_1018) -> q_gen_1016
<nil, nil, cons>(q_gen_1032, q_gen_1031) -> q_gen_1016
<nil, nil, nil>() -> q_gen_1016
<a, a, a>() -> q_gen_1033
<a, b, a>() -> q_gen_1033
<b, a, b>() -> q_gen_1033
<b, b, b>() -> q_gen_1033
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  invsorted -> 
{{{
Q={q_gen_1013, q_gen_1015},
Q_f={q_gen_1013},
Delta=
{
<cons>(q_gen_1015, q_gen_1013) -> q_gen_1013
<nil>() -> q_gen_1013
<a>() -> q_gen_1015
<b>() -> q_gen_1015
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_1010, q_gen_1035, q_gen_1046, q_gen_1047},
Q_f={q_gen_1010},
Delta=
{
<cons>(q_gen_1047, q_gen_1046) -> q_gen_1046
<nil>() -> q_gen_1046
<a>() -> q_gen_1047
<b>() -> q_gen_1047
<cons, cons>(q_gen_1035, q_gen_1010) -> q_gen_1010
<nil, cons>(q_gen_1047, q_gen_1046) -> q_gen_1010
<nil, nil>() -> q_gen_1010
<a, a>() -> q_gen_1035
<a, b>() -> q_gen_1035
<b, a>() -> q_gen_1035
<b, b>() -> q_gen_1035
}

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sorted -> 
{{{
Q={q_gen_1007, q_gen_1009},
Q_f={q_gen_1007},
Delta=
{
<cons>(q_gen_1009, q_gen_1007) -> q_gen_1007
<nil>() -> q_gen_1007
<a>() -> q_gen_1009
<b>() -> q_gen_1009
}

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

}
--
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([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]) -> 28
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(leq([b, a])) -> BOT -> 19
(reverse([l, _nf]) /\ sorted([l])) -> invsorted([_nf]) -> 19
}
Sat witness: Found: ((append([_if, cons(h1, nil), _jf]) /\ reverse([t1, _if])) -> reverse([cons(h1, t1), _jf]), {
_if -> cons(b, nil)  ;  _jf -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

Total time: 0.348657
Reason for stopping: Proved