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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, y])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(insert, F:
{() -> insert([x, nil, cons(x, nil)])
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_bl, _cl, _dl]) /\ insert([_bl, _cl, _el])) -> eq_eltlist([_dl, _el])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl])}
(sort([_hl, _il]) /\ sort([_hl, _jl])) -> eq_eltlist([_il, _jl])
)
(length, F:
{() -> length([nil, z])
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)])}
(length([_ll, _ml]) /\ length([_ll, _nl])) -> eq_nat([_ml, _nl])
)
}

properties:
{(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql])}


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

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 0
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 0
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 0
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 0
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
}


Solving took 0.256495 seconds.
Proved
Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2494
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<a, b>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005098 s (model generation: 0.004746,  model checking: 0.000352):

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

}

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

}

Datatype: <eltlist, nat>
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
}}}

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.004549 s (model generation: 0.004525,  model checking: 0.000024):

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

}

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 2, which took 0.004099 s (model generation: 0.004076,  model checking: 0.000023):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 3, which took 0.004230 s (model generation: 0.004186,  model checking: 0.000044):

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

}

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 4, which took 0.005888 s (model generation: 0.005765,  model checking: 0.000123):

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489},
Q_f={q_gen_2489},
Delta=
{
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 5, which took 0.010639 s (model generation: 0.010161,  model checking: 0.000478):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489},
Q_f={q_gen_2489},
Delta=
{
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 6, which took 0.011345 s (model generation: 0.011075,  model checking: 0.000270):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489},
Q_f={q_gen_2489},
Delta=
{
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 1
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 1
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.011814 s (model generation: 0.011485,  model checking: 0.000329):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 1
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.015309 s (model generation: 0.011701,  model checking: 0.003608):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]), {
_al -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.012571 s (model generation: 0.012540,  model checking: 0.000031):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 3
() -> leq([b, b]) -> 3
() -> sort([nil, nil]) -> 3
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 2
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.013216 s (model generation: 0.012844,  model checking: 0.000372):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 3
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.014746 s (model generation: 0.013905,  model checking: 0.000841):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.014888 s (model generation: 0.012940,  model checking: 0.001948):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 13, which took 0.013546 s (model generation: 0.013255,  model checking: 0.000291):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 4
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 4
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _kl])) -> length([cons(x, ll), s(_kl)]), {
_kl -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 14, which took 0.015350 s (model generation: 0.013627,  model checking: 0.001723):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 4
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 5
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.015990 s (model generation: 0.014546,  model checking: 0.001444):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 5
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]), {
_al -> cons(a, cons(a, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 16, which took 0.018408 s (model generation: 0.016216,  model checking: 0.002192):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2494
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> length([nil, z]) -> 5
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> sort([nil, nil]) -> 5
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 7
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 6
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 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.018657 s (model generation: 0.017523,  model checking: 0.001134):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2494
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<a, b>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 7
() -> length([nil, z]) -> 6
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> sort([nil, nil]) -> 6
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 7
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 10
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 7
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 8
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
}
Sat witness: Found: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.021803 s (model generation: 0.018497,  model checking: 0.003306):

Model:
|_
{
insert -> 
{{{
Q={q_gen_2490, q_gen_2491, q_gen_2492, q_gen_2494, q_gen_2495},
Q_f={q_gen_2490},
Delta=
{
<nil>() -> q_gen_2491
<a>() -> q_gen_2492
<b>() -> q_gen_2492
<cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2494
<nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2494
<a, a>() -> q_gen_2495
<a, b>() -> q_gen_2495
<b, a>() -> q_gen_2495
<b, b>() -> q_gen_2495
<a, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<a, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
<b, cons, cons>(q_gen_2495, q_gen_2494) -> q_gen_2490
<b, nil, cons>(q_gen_2492, q_gen_2491) -> q_gen_2490
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_2489, q_gen_2497},
Q_f={q_gen_2489},
Delta=
{
<a>() -> q_gen_2497
<b>() -> q_gen_2497
<cons, s>(q_gen_2497, q_gen_2489) -> q_gen_2489
<nil, z>() -> q_gen_2489
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> insert([x, nil, cons(x, nil)]) -> 8
() -> length([nil, z]) -> 7
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 7
() -> sort([nil, nil]) -> 7
(insert([x, z, _al]) /\ not leq([x, y])) -> insert([x, cons(y, z), cons(y, _al)]) -> 8
(insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]) -> 13
(length([_pl, _ql]) /\ length([l, _ol]) /\ sort([l, _pl])) -> eq_nat([_ol, _ql]) -> 8
(length([ll, _kl])) -> length([cons(x, ll), s(_kl)]) -> 9
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 8
}
Sat witness: Found: ((insert([y, _fl, _gl]) /\ sort([z, _fl])) -> sort([cons(y, z), _gl]), {
_fl -> nil  ;  _gl -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

Total time: 0.256495
Reason for stopping: Proved