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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_yh, _zh, _ai]) /\ insert([_yh, _zh, _bi])) -> eq_eltlist([_ai, _bi])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di])}
(sort([_ei, _fi]) /\ sort([_ei, _gi])) -> eq_eltlist([_fi, _gi])
)
(sorted, P:
{() -> sorted([cons(x, nil)])
() -> sorted([nil])}
)
}

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


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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 0
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
(sort([l, _hi])) -> sorted([_hi]) -> 0
}


Solving took 0.213387 seconds.
Proved
Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2109
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<a, b>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<a, a>() -> q_gen_2112
<a, b>() -> q_gen_2112
<b, a>() -> q_gen_2112
<b, b>() -> q_gen_2112
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009018 s (model generation: 0.008748,  model checking: 0.000270):

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> 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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> sorted([nil]), {

})

-------------------------------------------
Step 1, which took 0.007448 s (model generation: 0.007380,  model checking: 0.000068):

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

}

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

}

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

}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 2, which took 0.007712 s (model generation: 0.007452,  model checking: 0.000260):

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

}

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

}

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

}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 3, which took 0.008152 s (model generation: 0.008116,  model checking: 0.000036):

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

}

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

}

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

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 4, which took 0.007712 s (model generation: 0.007668,  model checking: 0.000044):

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

}

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

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

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 5, which took 0.008741 s (model generation: 0.008617,  model checking: 0.000124):

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

}

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

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

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
(sort([l, _hi])) -> sorted([_hi]) -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 6, which took 0.011212 s (model generation: 0.007606,  model checking: 0.003606):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

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

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _hi])) -> sorted([_hi]) -> 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.008472 s (model generation: 0.008068,  model checking: 0.000404):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

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

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 1
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _hi])) -> sorted([_hi]) -> 2
}
Sat witness: Found: ((insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]), {
_ci -> nil  ;  _di -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.008717 s (model generation: 0.008366,  model checking: 0.000351):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
(sort([l, _hi])) -> sorted([_hi]) -> 2
}
Sat witness: Found: ((insert([x, z, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]), {
_xh -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.010186 s (model generation: 0.010059,  model checking: 0.000127):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 3
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.010353 s (model generation: 0.010178,  model checking: 0.000175):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 4
}
Sat witness: Found: (() -> sorted([cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 11, which took 0.009443 s (model generation: 0.009304,  model checking: 0.000139):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 4
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 12, which took 0.010952 s (model generation: 0.010555,  model checking: 0.000397):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 4
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 13, which took 0.010958 s (model generation: 0.010514,  model checking: 0.000444):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 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.010885 s (model generation: 0.010557,  model checking: 0.000328):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 4
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 5
}
Sat witness: Found: ((insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]), {
_ci -> nil  ;  _di -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.011576 s (model generation: 0.010761,  model checking: 0.000815):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<a, b>() -> q_gen_2112
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 7
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
(sort([l, _hi])) -> sorted([_hi]) -> 5
}
Sat witness: Found: ((insert([x, z, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]), {
_xh -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 16, which took 0.014654 s (model generation: 0.013785,  model checking: 0.000869):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2109
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<a, b>() -> q_gen_2112
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 7
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 6
(sort([l, _hi])) -> sorted([_hi]) -> 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.014456 s (model generation: 0.013912,  model checking: 0.000544):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2109
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<a, b>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<a, b>() -> q_gen_2112
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 7
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
(sort([l, _hi])) -> sorted([_hi]) -> 7
}
Sat witness: Found: ((insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]), {
_ci -> nil  ;  _di -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.015823 s (model generation: 0.014500,  model checking: 0.001323):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2105, q_gen_2106, q_gen_2107, q_gen_2109, q_gen_2110},
Q_f={q_gen_2105},
Delta=
{
<nil>() -> q_gen_2106
<a>() -> q_gen_2107
<b>() -> q_gen_2107
<cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2109
<nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2109
<a, a>() -> q_gen_2110
<a, b>() -> q_gen_2110
<b, a>() -> q_gen_2110
<b, b>() -> q_gen_2110
<a, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<a, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
<b, cons, cons>(q_gen_2110, q_gen_2109) -> q_gen_2105
<b, nil, cons>(q_gen_2107, q_gen_2106) -> q_gen_2105
}

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

Datatype: <elt, elt>
Convolution form: left
}}}
  ;  sort -> 
{{{
Q={q_gen_2102, q_gen_2112},
Q_f={q_gen_2102},
Delta=
{
<cons, cons>(q_gen_2112, q_gen_2102) -> q_gen_2102
<nil, nil>() -> q_gen_2102
<a, a>() -> q_gen_2112
<a, b>() -> q_gen_2112
<b, b>() -> q_gen_2112
}

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

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

}
--
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, _xh]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _xh)]) -> 8
(insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 8
(sort([l, _hi])) -> sorted([_hi]) -> 8
}
Sat witness: Found: ((insert([y, _ci, _di]) /\ sort([z, _ci])) -> sort([cons(y, z), _di]), {
_ci -> nil  ;  _di -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

Total time: 0.213387
Reason for stopping: Proved