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}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_qk, _rk, _sk]) /\ insert([_qk, _rk, _tk])) -> eq_eltlist([_sk, _tk])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk])}
(sort([_wk, _xk]) /\ sort([_wk, _yk])) -> eq_eltlist([_xk, _yk])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
}

properties:
{(sort([l, _zk])) -> sorted([_zk])}


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

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 0
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 0
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
(sort([l, _zk])) -> sorted([_zk]) -> 0
}


Solving took 0.285015 seconds.
Proved
Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2419
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<a, b>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<a, a>() -> q_gen_2422
<a, b>() -> q_gen_2422
<b, a>() -> q_gen_2422
<b, b>() -> q_gen_2422
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011359 s (model generation: 0.010120,  model checking: 0.001239):

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

}

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

}

Datatype: <elt, elt>
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:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 0
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.010445 s (model generation: 0.010310,  model checking: 0.000135):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 0
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.010689 s (model generation: 0.010566,  model checking: 0.000123):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.010658 s (model generation: 0.010596,  model checking: 0.000062):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.010760 s (model generation: 0.010626,  model checking: 0.000134):

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.011013 s (model generation: 0.010775,  model checking: 0.000238):

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

}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _zk])) -> sorted([_zk]) -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 6, which took 0.014612 s (model generation: 0.010759,  model checking: 0.003853):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 7, which took 0.011506 s (model generation: 0.011267,  model checking: 0.000239):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 1
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Found: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.012173 s (model generation: 0.011535,  model checking: 0.000638):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _zk])) -> sorted([_zk]) -> 2
}
Sat witness: Found: ((insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]), {
_pk -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.013605 s (model generation: 0.013389,  model checking: 0.000216):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 3
() -> sorted([nil]) -> 3
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 3
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.012717 s (model generation: 0.012317,  model checking: 0.000400):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 11, which took 0.012792 s (model generation: 0.012582,  model checking: 0.000210):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 12, which took 0.014810 s (model generation: 0.014350,  model checking: 0.000460):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 4
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 13, which took 0.015016 s (model generation: 0.013191,  model checking: 0.001825):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 14, which took 0.014207 s (model generation: 0.013581,  model checking: 0.000626):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 4
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Found: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.016177 s (model generation: 0.015194,  model checking: 0.000983):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<a, b>() -> q_gen_2422
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
() -> sorted([cons(x, nil)]) -> 6
() -> sorted([nil]) -> 4
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _zk])) -> sorted([_zk]) -> 5
}
Sat witness: Found: ((insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]), {
_pk -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 16, which took 0.018760 s (model generation: 0.016764,  model checking: 0.001996):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2419
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<a, b>() -> q_gen_2422
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> sort([nil, nil]) -> 5
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 5
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 6
(sort([l, _zk])) -> sorted([_zk]) -> 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 17, which took 0.018592 s (model generation: 0.017329,  model checking: 0.001263):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2419
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<a, b>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<a, b>() -> q_gen_2422
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> sort([nil, nil]) -> 6
() -> sorted([cons(x, nil)]) -> 7
() -> sorted([nil]) -> 6
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 7
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
(sort([l, _zk])) -> sorted([_zk]) -> 7
}
Sat witness: Found: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.020981 s (model generation: 0.017944,  model checking: 0.003037):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2415, q_gen_2416, q_gen_2417, q_gen_2419, q_gen_2420},
Q_f={q_gen_2415},
Delta=
{
<nil>() -> q_gen_2416
<a>() -> q_gen_2417
<b>() -> q_gen_2417
<cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2419
<nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2419
<a, a>() -> q_gen_2420
<a, b>() -> q_gen_2420
<b, a>() -> q_gen_2420
<b, b>() -> q_gen_2420
<a, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<a, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
<b, cons, cons>(q_gen_2420, q_gen_2419) -> q_gen_2415
<b, nil, cons>(q_gen_2417, q_gen_2416) -> q_gen_2415
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_2412, q_gen_2422},
Q_f={q_gen_2412},
Delta=
{
<cons, cons>(q_gen_2422, q_gen_2412) -> q_gen_2412
<nil, nil>() -> q_gen_2412
<a, a>() -> q_gen_2422
<a, b>() -> q_gen_2422
<b, b>() -> q_gen_2422
}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 8
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 7
() -> sort([nil, nil]) -> 7
() -> sorted([cons(x, nil)]) -> 8
() -> sorted([nil]) -> 7
(insert([x, z, _pk]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _pk)]) -> 8
(insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 8
(sort([l, _zk])) -> sorted([_zk]) -> 8
}
Sat witness: Found: ((insert([y, _uk, _vk]) /\ sort([z, _uk])) -> sort([cons(y, z), _vk]), {
_uk -> nil  ;  _vk -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

Total time: 0.285015
Reason for stopping: Proved