Solving ../../benchmarks/smtlib/true/sort_length_eq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{
leq(a, y) <= True
leq(b, b) <= True
False <= leq(b, a)
}
)
(insert, F:
{
insert(x, nil, cons(x, nil)) <= True
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)
}
eq_eltlist(_et, _ft) <= insert(_ct, _dt, _et) /\ insert(_ct, _dt, _ft)
)
(sort, F:
{
sort(nil, nil) <= True
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)
}
eq_eltlist(_jt, _kt) <= sort(_it, _jt) /\ sort(_it, _kt)
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_lt)) <= length(ll, _lt)
}
eq_nat(_nt, _ot) <= length(_mt, _nt) /\ length(_mt, _ot)
)
}

properties:
{
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)
}


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

Clause system for inference is:

{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}


Solving took 0.746553 seconds.
Yes: |_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006063 s (model generation: 0.005945,  model checking: 0.000118):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  
}
]


;
length ->
[
length : <eltlist * nat>
{
  
}
]


;
leq ->
[
leq : <elt * elt>
{
  
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
Yes: {
x -> b
}

length(nil, z) <= True  :
Yes: {

}

leq(a, y) <= True  :
Yes: {
y -> b
}

leq(b, b) <= True  :
Yes: {

}

sort(nil, nil) <= True  :
Yes: {

}

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
No: ()

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 1, which took 0.006682 s (model generation: 0.006587,  model checking: 0.000095):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(b, nil, cons(b, nil)) <= True
length(nil, z) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
Yes: {
x -> a
}

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
Yes: {
y -> a
}

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
Yes: {
_bt -> cons(_jwuxa_0, _jwuxa_1)  ;  x -> b  ;  y -> a  ;  z -> nil
}

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> nil  ;  _ht -> cons(_owuxa_0, _owuxa_1)  ;  y -> b  ;  z -> nil
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
Yes: {
_lt -> z  ;  ll -> nil
}

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
Yes: {
x -> b  ;  y -> b
}

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 2, which took 0.011212 s (model generation: 0.011115,  model checking: 0.000097):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
insert(b, cons(a, nil), cons(a, cons(a, nil))) \/ leq(b, a) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= True
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, a) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
No: ()

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(z)  ;  _qt -> cons(_ywuxa_0, _ywuxa_1)  ;  _rt -> s(s(_kxuxa_0))  ;  l -> cons(_axuxa_0, _axuxa_1)
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
Yes: {
x -> a  ;  y -> b
}

False <= leq(b, a)  :
Yes: {

}


-------------------------------------------
Step 3, which took 0.012285 s (model generation: 0.012022,  model checking: 0.000263):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z))) /\ sort(cons(a, nil), cons(a, nil))
False <= leq(b, a)
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
No: ()

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(z)  ;  _qt -> cons(_mxuxa_0, cons(_dyuxa_0, nil))  ;  _rt -> s(s(z))  ;  l -> cons(_oxuxa_0, nil)
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 4, which took 0.016060 s (model generation: 0.015483,  model checking: 0.000577):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ sort(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z))) /\ sort(cons(a, nil), cons(a, nil))
False <= leq(b, a)
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> nil  ;  _ht -> cons(_wyuxa_0, cons(_hzuxa_0, _hzuxa_1))  ;  y -> b  ;  z -> nil
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 5, which took 0.034368 s (model generation: 0.034259,  model checking: 0.000109):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ sort(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z))) /\ sort(cons(a, nil), cons(a, nil))
False <= leq(b, a)
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  _r_1(z) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
No: ()

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
Yes: {
_lt -> s(z)  ;  ll -> cons(_nzuxa_0, _nzuxa_1)
}

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 6, which took 0.023523 s (model generation: 0.023390,  model checking: 0.000133):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(nil, nil) <= True
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z))) /\ sort(cons(a, nil), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= True
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  _r_1(b) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> nil  ;  _ht -> cons(_wzuxa_0, _wzuxa_1)  ;  y -> a  ;  z -> nil
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(z)  ;  _qt -> cons(_iavxa_0, _iavxa_1)  ;  _rt -> s(s(_ravxa_0))  ;  l -> cons(b, _kavxa_1)
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 7, which took 0.020930 s (model generation: 0.020711,  model checking: 0.000219):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= leq(b, a)
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= True
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= True
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  _r_1(a, nil) <= True
  _r_1(b, cons(x_1_0, x_1_1)) <= True
  _r_1(b, nil) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> nil  ;  _ht -> cons(_xavxa_0, cons(_qbvxa_0, _qbvxa_1))  ;  y -> a  ;  z -> nil
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(s(z))  ;  _qt -> cons(_jbvxa_0, nil)  ;  _rt -> s(z)  ;  l -> cons(b, cons(_icvxa_0, nil))
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 8, which took 0.022994 s (model generation: 0.022678,  model checking: 0.000316):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> cons(_zcvxa_0, nil)  ;  _ht -> cons(_advxa_0, nil)  ;  y -> b  ;  z -> cons(_cdvxa_0, nil)
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 9, which took 0.054862 s (model generation: 0.054598,  model checking: 0.000264):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> cons(_levxa_0, nil)  ;  _ht -> cons(_mevxa_0, nil)  ;  y -> a  ;  z -> cons(_oevxa_0, nil)
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 10, which took 0.050551 s (model generation: 0.050171,  model checking: 0.000380):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  _r_2(a) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0) /\ length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  _r_1(nil) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> cons(_zfvxa_0, nil)  ;  _ht -> cons(_agvxa_0, cons(_bhvxa_0, _bhvxa_1))  ;  y -> a  ;  z -> cons(_cgvxa_0, _cgvxa_1)
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(s(z))  ;  _qt -> cons(a, nil)  ;  _rt -> s(z)  ;  l -> cons(a, cons(a, nil))
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
Yes: {
_lt -> z  ;  ll -> nil  ;  x -> b
}

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 11, which took 0.058145 s (model generation: 0.057709,  model checking: 0.000436):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, cons(a, nil)))
False <= insert(a, cons(a, nil), cons(a, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(nil) <= True
  _r_2(cons(x_0_0, x_0_1)) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> cons(_xhvxa_0, nil)  ;  _ht -> cons(_yhvxa_0, cons(_ejvxa_0, cons(_hjvxa_0, _hjvxa_1)))  ;  y -> a  ;  z -> cons(_aivxa_0, nil)
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 12, which took 0.067878 s (model generation: 0.067606,  model checking: 0.000272):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil))))
sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, cons(a, nil)))
False <= insert(a, cons(a, nil), cons(a, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(nil) <= True
  _r_2(b) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
Yes: {
_bt -> cons(b, _ojvxa_1)  ;  x -> b  ;  y -> a  ;  z -> nil
}

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> nil  ;  _ht -> cons(b, cons(_xkvxa_0, _xkvxa_1))  ;  y -> b  ;  z -> nil
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
Yes: {
x -> a  ;  y -> a
}

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 13, which took 0.086062 s (model generation: 0.085735,  model checking: 0.000327):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= insert(a, cons(a, nil), cons(a, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
Yes: {
_bt -> cons(_alvxa_0, cons(_mmvxa_0, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(_dlvxa_0, _dlvxa_1)
}

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
Yes: {
_gt -> cons(_qlvxa_0, cons(_qmvxa_0, nil))  ;  _ht -> cons(_rlvxa_0, cons(_omvxa_0, nil))  ;  y -> b  ;  z -> cons(_tlvxa_0, cons(_pmvxa_0, nil))
}

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
No: ()

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
Yes: {
x -> b  ;  y -> b  ;  z -> cons(_umvxa_0, _umvxa_1)
}

False <= leq(b, a)  :
No: ()


-------------------------------------------
Step 14, which took 0.137201 s (model generation: 0.136117,  model checking: 0.001084):

Clauses:
{
insert(x, nil, cons(x, nil)) <= True -> 0
length(nil, z) <= True -> 0
leq(a, y) <= True -> 0
leq(b, b) <= True -> 0
sort(nil, nil) <= True -> 0
insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt) -> 0
sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt) -> 0
eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt) -> 0
length(cons(x, ll), s(_lt)) <= length(ll, _lt) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}

Accumulated learning constraints:
{
insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True
insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True
insert(a, nil, cons(a, nil)) <= True
insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True
insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True
insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True
insert(b, nil, cons(b, nil)) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
sort(cons(a, nil), cons(a, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= insert(a, cons(a, nil), cons(a, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil)))
insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil)))
insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil))
sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(nil) <= True
  _r_2(cons(x_0_0, x_0_1)) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  _r_1(nil) <= True
  _r_2(cons(x_0_0, x_0_1)) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1)
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|




Answer of teacher:

insert(x, nil, cons(x, nil)) <= True  :
No: ()

length(nil, z) <= True  :
No: ()

leq(a, y) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

sort(nil, nil) <= True  :
No: ()

insert(x, cons(y, z), cons(y, _bt)) \/ leq(x, y) <= insert(x, z, _bt)  :
No: ()

sort(cons(y, z), _ht) <= insert(y, _gt, _ht) /\ sort(z, _gt)  :
No: ()

eq_nat(_pt, _rt) <= length(_qt, _rt) /\ length(l, _pt) /\ sort(l, _qt)  :
Yes: {
_pt -> s(s(s(z)))  ;  _qt -> cons(_jrvxa_0, cons(_yrvxa_0, nil))  ;  _rt -> s(s(z))  ;  l -> cons(_lrvxa_0, cons(_xrvxa_0, cons(_lsvxa_0, nil)))
}

length(cons(x, ll), s(_lt)) <= length(ll, _lt)  :
No: ()

insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)  :
No: ()

False <= leq(b, a)  :
No: ()


Total time: 0.746553
Learner time: 0.604126
Teacher time: 0.004690
Reasons for stopping: Yes: |_
name: None

insert ->
[
insert : <elt * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(nil) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length ->
[
length : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


;
sort ->
[
sort : <eltlist * eltlist>
{
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= sort(x_0_1, x_1_1)
  sort(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|