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, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)])}
(append([_kd, _ld, _md]) /\ append([_kd, _ld, _nd])) -> eq_eltlist([_md, _nd])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd])}
(reverse([_qd, _rd]) /\ reverse([_qd, _sd])) -> eq_eltlist([_rd, _sd])
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_ud, _vd, _wd]) /\ insert([_ud, _vd, _xd])) -> eq_eltlist([_wd, _xd])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd])}
(sort([_ae, _be]) /\ sort([_ae, _ce])) -> eq_eltlist([_be, _ce])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 0
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 0
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 0
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 0
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 0
}


Solving took 0.993977 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<a, b>() -> q_gen_779
<b, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011679 s (model generation: 0.010061,  model checking: 0.001618):

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

}

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

}

Datatype: <elt, eltlist, 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
}}}
  ;  sort -> 
{{{
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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.010272 s (model generation: 0.010141,  model checking: 0.000131):

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

}

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

}

Datatype: <elt, eltlist, 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
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.010446 s (model generation: 0.010312,  model checking: 0.000134):

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

}

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

}

Datatype: <elt, eltlist, 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
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 0
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.010681 s (model generation: 0.010516,  model checking: 0.000165):

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

}

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

}

Datatype: <elt, eltlist, 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
}}}
  ;  sort -> 
{{{
Q={q_gen_761},
Q_f={q_gen_761},
Delta=
{
<nil, nil>() -> q_gen_761
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 4, which took 0.010683 s (model generation: 0.010616,  model checking: 0.000067):

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

}

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

}

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

}

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 5, which took 0.010775 s (model generation: 0.010695,  model checking: 0.000080):

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

}

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

}

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

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 6, which took 0.015884 s (model generation: 0.015615,  model checking: 0.000269):

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

}

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

}

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

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 7, which took 0.011841 s (model generation: 0.011539,  model checking: 0.000302):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.011922 s (model generation: 0.011380,  model checking: 0.000542):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 2
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.014142 s (model generation: 0.013877,  model checking: 0.000265):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

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

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 1
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 2
}
Sat witness: Found: ((insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]), {
_yd -> nil  ;  _zd -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 10, which took 0.012843 s (model generation: 0.012099,  model checking: 0.000744):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 1
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 2
}
Sat witness: Found: ((insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]), {
_td -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 11, which took 0.015925 s (model generation: 0.013084,  model checking: 0.002841):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 1
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 2
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.013424 s (model generation: 0.013135,  model checking: 0.000289):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<nil, nil>() -> q_gen_778
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 2
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 3
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 13, which took 0.013801 s (model generation: 0.013393,  model checking: 0.000408):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<nil, nil>() -> q_gen_778
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> reverse([nil, nil]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 3
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 4
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 14, which took 0.015714 s (model generation: 0.015251,  model checking: 0.000463):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<nil, nil>() -> q_gen_778
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 15, which took 0.015411 s (model generation: 0.013338,  model checking: 0.002073):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<nil, nil>() -> q_gen_778
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 4
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 16, which took 0.014428 s (model generation: 0.013870,  model checking: 0.000558):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<nil, nil>() -> q_gen_778
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 17, which took 0.016686 s (model generation: 0.014328,  model checking: 0.002358):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 5
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.016015 s (model generation: 0.014634,  model checking: 0.001381):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 4
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 5
}
Sat witness: Found: ((insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]), {
_yd -> nil  ;  _zd -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 19, which took 0.017733 s (model generation: 0.015812,  model checking: 0.001921):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 4
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 7
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 5
}
Sat witness: Found: ((insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]), {
_td -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 20, which took 0.019813 s (model generation: 0.017244,  model checking: 0.002569):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779},
Q_f={q_gen_768},
Delta=
{
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 4
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 7
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 7
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 5
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.019565 s (model generation: 0.019221,  model checking: 0.000344):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> reverse([nil, nil]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 7
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 7
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 7
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 5
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> nil  ;  _pd -> cons(b, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.022400 s (model generation: 0.018562,  model checking: 0.003838):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> reverse([nil, nil]) -> 5
() -> sort([nil, nil]) -> 5
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 5
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 7
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 7
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 7
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 6
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 6
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.022041 s (model generation: 0.020277,  model checking: 0.001764):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> reverse([nil, nil]) -> 6
() -> sort([nil, nil]) -> 6
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 6
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 7
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 7
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 7
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 7
}
Sat witness: Found: ((insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]), {
_yd -> nil  ;  _zd -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 24, which took 0.024747 s (model generation: 0.022601,  model checking: 0.002146):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 7
() -> reverse([nil, nil]) -> 7
() -> sort([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 7
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 7
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 10
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 8
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 8
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 8
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.023796 s (model generation: 0.023340,  model checking: 0.000456):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 7
() -> reverse([nil, nil]) -> 7
() -> sort([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 7
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 10
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 10
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 8
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 8
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 8
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> nil  ;  _pd -> cons(a, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.027775 s (model generation: 0.024450,  model checking: 0.003325):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 8
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 8
() -> reverse([nil, nil]) -> 8
() -> sort([nil, nil]) -> 8
() -> sorted([cons(x, nil)]) -> 8
() -> sorted([nil]) -> 8
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 10
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 10
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 9
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 9
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 9
}
Sat witness: Found: ((insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]), {
_yd -> nil  ;  _zd -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 27, which took 0.028786 s (model generation: 0.023686,  model checking: 0.005100):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 9
() -> leq([a, y]) -> 9
() -> leq([b, b]) -> 9
() -> reverse([nil, nil]) -> 9
() -> sort([nil, nil]) -> 9
() -> sorted([cons(x, nil)]) -> 9
() -> sorted([nil]) -> 9
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 10
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 13
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 10
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 10
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 10
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.028233 s (model generation: 0.024967,  model checking: 0.003266):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, b, a>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 10
() -> leq([a, y]) -> 10
() -> leq([b, b]) -> 10
() -> reverse([nil, nil]) -> 10
() -> sort([nil, nil]) -> 10
() -> sorted([cons(x, nil)]) -> 10
() -> sorted([nil]) -> 10
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 13
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 13
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 11
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 11
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 11
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> nil  ;  _pd -> cons(b, cons(b, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.035751 s (model generation: 0.027165,  model checking: 0.008586):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, b, a>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 11
() -> leq([a, y]) -> 11
() -> leq([b, b]) -> 11
() -> reverse([nil, nil]) -> 11
() -> sort([nil, nil]) -> 11
() -> sorted([cons(x, nil)]) -> 11
() -> sorted([nil]) -> 11
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 13
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 16
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 12
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 14
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 12
(leq([b, a])) -> BOT -> 12
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 12
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.033675 s (model generation: 0.029240,  model checking: 0.004435):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 12
() -> leq([a, y]) -> 12
() -> leq([b, b]) -> 12
() -> reverse([nil, nil]) -> 12
() -> sort([nil, nil]) -> 12
() -> sorted([cons(x, nil)]) -> 12
() -> sorted([nil]) -> 12
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 16
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 16
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 13
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 14
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13
(leq([b, a])) -> BOT -> 13
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 13
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> cons(b, nil)  ;  _pd -> cons(b, nil)  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.039933 s (model generation: 0.033503,  model checking: 0.006430):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 13
() -> leq([a, y]) -> 13
() -> leq([b, b]) -> 13
() -> reverse([nil, nil]) -> 13
() -> sort([nil, nil]) -> 13
() -> sorted([cons(x, nil)]) -> 13
() -> sorted([nil]) -> 13
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 16
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 19
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 14
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 15
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14
(leq([b, a])) -> BOT -> 14
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 14
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 32, which took 0.039634 s (model generation: 0.034305,  model checking: 0.005329):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 14
() -> leq([a, y]) -> 14
() -> leq([b, b]) -> 14
() -> reverse([nil, nil]) -> 14
() -> sort([nil, nil]) -> 14
() -> sorted([cons(x, nil)]) -> 14
() -> sorted([nil]) -> 14
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 19
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 19
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 15
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 16
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15
(leq([b, a])) -> BOT -> 15
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 15
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> nil  ;  _pd -> cons(b, cons(a, nil))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 33, which took 0.044000 s (model generation: 0.035761,  model checking: 0.008239):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 15
() -> leq([a, y]) -> 15
() -> leq([b, b]) -> 15
() -> reverse([nil, nil]) -> 15
() -> sort([nil, nil]) -> 15
() -> sorted([cons(x, nil)]) -> 15
() -> sorted([nil]) -> 15
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 19
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 22
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 16
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 17
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16
(leq([b, a])) -> BOT -> 16
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 16
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.046964 s (model generation: 0.040831,  model checking: 0.006133):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 16
() -> leq([a, y]) -> 16
() -> leq([b, b]) -> 16
() -> reverse([nil, nil]) -> 16
() -> sort([nil, nil]) -> 16
() -> sorted([cons(x, nil)]) -> 16
() -> sorted([nil]) -> 16
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 22
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 22
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 17
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 18
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 17
(leq([b, a])) -> BOT -> 17
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 17
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> cons(a, nil)  ;  _pd -> cons(a, nil)  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.058214 s (model generation: 0.043786,  model checking: 0.014428):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 17
() -> leq([a, y]) -> 17
() -> leq([b, b]) -> 17
() -> reverse([nil, nil]) -> 17
() -> sort([nil, nil]) -> 17
() -> sorted([cons(x, nil)]) -> 17
() -> sorted([nil]) -> 17
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 22
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 25
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 18
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 19
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18
(leq([b, a])) -> BOT -> 18
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 18
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 36, which took 0.054801 s (model generation: 0.049957,  model checking: 0.004844):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 18
() -> leq([a, y]) -> 18
() -> leq([b, b]) -> 18
() -> reverse([nil, nil]) -> 18
() -> sort([nil, nil]) -> 18
() -> sorted([cons(x, nil)]) -> 18
() -> sorted([nil]) -> 18
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 25
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 25
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 19
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 20
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 19
(leq([b, a])) -> BOT -> 19
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 19
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> nil  ;  _pd -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.058283 s (model generation: 0.049311,  model checking: 0.008972):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<b, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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
() -> insert([x, nil, cons(x, nil)]) -> 19
() -> leq([a, y]) -> 19
() -> leq([b, b]) -> 19
() -> reverse([nil, nil]) -> 19
() -> sort([nil, nil]) -> 19
() -> sorted([cons(x, nil)]) -> 19
() -> sorted([nil]) -> 19
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 25
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 28
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 20
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 21
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20
(leq([b, a])) -> BOT -> 20
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 20
}
Sat witness: Found: ((append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]), {
_jd -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 38, which took 0.053263 s (model generation: 0.050613,  model checking: 0.002650):

Model:
|_
{
append -> 
{{{
Q={q_gen_768, q_gen_778, q_gen_779, q_gen_800, q_gen_801, q_gen_802},
Q_f={q_gen_768},
Delta=
{
<cons>(q_gen_801, q_gen_800) -> q_gen_800
<nil>() -> q_gen_800
<a>() -> q_gen_801
<b>() -> q_gen_801
<cons, cons>(q_gen_779, q_gen_778) -> q_gen_778
<nil, cons>(q_gen_801, q_gen_800) -> q_gen_778
<nil, nil>() -> q_gen_778
<a, a>() -> q_gen_779
<a, b>() -> q_gen_779
<b, a>() -> q_gen_779
<b, b>() -> q_gen_779
<cons, cons, cons>(q_gen_802, q_gen_768) -> q_gen_768
<cons, nil, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, cons, cons>(q_gen_779, q_gen_778) -> q_gen_768
<nil, nil, cons>(q_gen_801, q_gen_800) -> q_gen_768
<nil, nil, nil>() -> q_gen_768
<a, a, a>() -> q_gen_802
<a, b, a>() -> q_gen_802
<b, a, b>() -> q_gen_802
<b, b, b>() -> q_gen_802
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  insert -> 
{{{
Q={q_gen_765, q_gen_766, q_gen_767, q_gen_770, q_gen_771},
Q_f={q_gen_765},
Delta=
{
<nil>() -> q_gen_766
<a>() -> q_gen_767
<b>() -> q_gen_767
<cons, cons>(q_gen_771, q_gen_770) -> q_gen_770
<nil, cons>(q_gen_767, q_gen_766) -> q_gen_770
<a, a>() -> q_gen_771
<a, b>() -> q_gen_771
<b, a>() -> q_gen_771
<b, b>() -> q_gen_771
<a, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<a, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
<b, cons, cons>(q_gen_771, q_gen_770) -> q_gen_765
<b, nil, cons>(q_gen_767, q_gen_766) -> q_gen_765
}

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

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

Datatype: <eltlist, eltlist>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_761, q_gen_773},
Q_f={q_gen_761},
Delta=
{
<cons, cons>(q_gen_773, q_gen_761) -> q_gen_761
<nil, nil>() -> q_gen_761
<a, a>() -> q_gen_773
<a, b>() -> q_gen_773
<b, a>() -> q_gen_773
<b, b>() -> q_gen_773
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> insert([x, nil, cons(x, nil)]) -> 20
() -> leq([a, y]) -> 20
() -> leq([b, b]) -> 20
() -> reverse([nil, nil]) -> 20
() -> sort([nil, nil]) -> 20
() -> sorted([cons(x, nil)]) -> 20
() -> sorted([nil]) -> 20
(append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]) -> 28
(append([t1, l2, _jd])) -> append([cons(h1, t1), l2, cons(h1, _jd)]) -> 28
(insert([x, z, _td]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _td)]) -> 21
(insert([y, _yd, _zd]) /\ sort([z, _yd])) -> sort([cons(y, z), _zd]) -> 22
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 21
(leq([b, a])) -> BOT -> 21
(reverse([_de, _ee]) /\ reverse([l, _de]) /\ sorted([l])) -> sorted([_ee]) -> 21
}
Sat witness: Found: ((append([_od, cons(h1, nil), _pd]) /\ reverse([t1, _od])) -> reverse([cons(h1, t1), _pd]), {
_od -> cons(b, nil)  ;  _pd -> cons(b, nil)  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

Total time: 0.993977
Reason for stopping: Proved