Solving ../../benchmarks/smtlib/false/sort_bug_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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y)
}
eq_eltlist(_fdb, _gdb) <= insert(_ddb, _edb, _fdb) /\ insert(_ddb, _edb, _gdb)
)
(sort, F:
{
sort(nil, nil) <= True
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)
}
eq_eltlist(_kdb, _ldb) <= sort(_jdb, _kdb) /\ sort(_jdb, _ldb)
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)
}
eq_nat(_odb, _pdb) <= length(_ndb, _odb) /\ length(_ndb, _pdb)
)
}

properties:
{
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)
}


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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 0
insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0
False <= leq(b, a) -> 0
}


Solving took 1.695574 seconds.
No: Contradictory set of ground constraints:
{
False <= True
insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True
insert(a, cons(b, cons(a, nil)), cons(a, cons(b, 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(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(cons(b, cons(a, nil)), cons(b, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, cons(b, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(a, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil))
False <= insert(a, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(a, nil), cons(b, nil)) <= insert(a, nil, cons(b, nil))
sort(cons(b, cons(a, cons(b, nil))), cons(b, cons(a, nil))) <= insert(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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)))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, cons(a, nil)), cons(b, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
False <= sort(cons(b, nil), nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007727 s (model generation: 0.007150,  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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
No: ()

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.007032 s (model generation: 0.006886,  model checking: 0.000146):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
Yes: {
_cdb -> cons(_dirqw_0, _dirqw_1)  ;  x -> b  ;  y -> a  ;  z -> nil
}

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(_iirqw_0, _iirqw_1)  ;  y -> b  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
Yes: {
_mdb -> 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.010677 s (model generation: 0.010527,  model checking: 0.000150):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
No: ()

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> cons(_sirqw_0, _sirqw_1)  ;  _sdb -> s(s(_ejrqw_0))  ;  l -> cons(_uirqw_0, _uirqw_1)
}

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.012679 s (model generation: 0.012497,  model checking: 0.000182):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
No: ()

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> cons(_gjrqw_0, cons(_xjrqw_0, nil))  ;  _sdb -> s(s(z))  ;  l -> cons(_ijrqw_0, nil)
}

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.011924 s (model generation: 0.011702,  model checking: 0.000222):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(_qkrqw_0, cons(_blrqw_0, _blrqw_1))  ;  y -> b  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.021228 s (model generation: 0.021061,  model checking: 0.000167):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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)) <= 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(_hlrqw_0, _hlrqw_1)  ;  y -> a  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> cons(_tlrqw_0, _tlrqw_1)  ;  _sdb -> s(s(_cmrqw_0))  ;  l -> cons(b, _vlrqw_1)
}

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

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

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


-------------------------------------------
Step 6, which took 0.022467 s (model generation: 0.022326,  model checking: 0.000141):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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(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, 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)))
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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
No: ()

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
Yes: {
_mdb -> s(z)  ;  ll -> cons(_imrqw_0, _imrqw_1)
}

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

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


-------------------------------------------
Step 7, which took 0.022668 s (model generation: 0.022261,  model checking: 0.000407):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(_rmrqw_0, cons(_knrqw_0, _knrqw_1))  ;  y -> a  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(s(z))  ;  _rdb -> cons(_dnrqw_0, nil)  ;  _sdb -> s(z)  ;  l -> cons(b, cons(_corqw_0, nil))
}

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.024289 s (model generation: 0.024030,  model checking: 0.000259):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_torqw_0, nil)  ;  _idb -> cons(_uorqw_0, nil)  ;  y -> b  ;  z -> cons(_worqw_0, nil)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.047625 s (model generation: 0.047109,  model checking: 0.000516):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_xprqw_0, nil)  ;  _idb -> cons(_yprqw_0, cons(_zqrqw_0, _zqrqw_1))  ;  y -> a  ;  z -> cons(_aqrqw_0, _aqrqw_1)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(s(z))  ;  _rdb -> cons(a, nil)  ;  _sdb -> s(z)  ;  l -> cons(a, cons(a, nil))
}

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
Yes: {
_mdb -> 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 10, which took 0.057562 s (model generation: 0.057304,  model checking: 0.000258):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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, 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)) <= 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)) <= _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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(b, cons(_wsrqw_0, _wsrqw_1))  ;  y -> b  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

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

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

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


-------------------------------------------
Step 11, which took 0.061578 s (model generation: 0.061321,  model checking: 0.000257):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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, 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(b) <= 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)) <= _r_2(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_qtrqw_0, nil)  ;  _idb -> cons(b, nil)  ;  y -> b  ;  z -> cons(_ttrqw_0, nil)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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.067277 s (model generation: 0.066777,  model checking: 0.000500):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, 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, 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(b) <= 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)) <= _r_2(x_1_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
Yes: {
_cdb -> cons(_zurqw_0, _zurqw_1)  ;  x -> b  ;  y -> a  ;  z -> cons(b, _cvrqw_1)
}

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(b, nil)  ;  _idb -> cons(_qvrqw_0, nil)  ;  y -> b  ;  z -> cons(_svrqw_0, nil)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

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

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

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


-------------------------------------------
Step 13, which took 0.073969 s (model generation: 0.073469,  model checking: 0.000500):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, 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, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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(b) <= 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)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
Yes: {
_cdb -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
}

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(b, nil)  ;  _idb -> cons(b, nil)  ;  y -> b  ;  z -> cons(_zxrqw_0, nil)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
No: ()

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

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

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


-------------------------------------------
Step 14, which took 0.080523 s (model generation: 0.079981,  model checking: 0.000542):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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(a, nil), 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, nil), cons(a, nil)) <= True
sort(cons(b, cons(a, nil)), cons(b, 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, nil, cons(a, cons(a, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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(b) <= 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)) <= _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>
{
  _r_2(b) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0)
  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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(b, _ozrqw_1)  ;  _idb -> cons(a, nil)  ;  y -> a  ;  z -> cons(_rzrqw_0, _rzrqw_1)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> cons(b, cons(_mbsqw_0, nil))  ;  _sdb -> s(s(z))  ;  l -> cons(_pasqw_0, nil)
}

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

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

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


-------------------------------------------
Step 15, which took 0.183593 s (model generation: 0.183039,  model checking: 0.000554):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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(a, nil), 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, nil), cons(a, nil)) <= True
sort(cons(b, cons(a, nil)), cons(b, 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(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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(a, nil), cons(b, cons(a, nil)))
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_2(nil) <= True
  _r_3(b) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0)
  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_3(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(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>
{
  _r_1(cons(x_0_0, x_0_1), b) <= True
  _r_1(nil, a) <= True
  _r_2(nil) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> nil  ;  _idb -> cons(b, nil)  ;  y -> a  ;  z -> nil
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(s(z))  ;  _rdb -> cons(b, nil)  ;  _sdb -> s(z)  ;  l -> cons(_odsqw_0, cons(_besqw_0, nil))
}

length(cons(x, ll), s(_mdb)) <= length(ll, _mdb)  :
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 16, which took 0.194383 s (model generation: 0.193637,  model checking: 0.000746):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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(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(cons(b, cons(a, nil)), cons(b, nil)) <= True
sort(nil, nil) <= True
False <= insert(a, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(a, nil), cons(b, nil)) <= insert(a, nil, cons(b, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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(a, nil), cons(b, cons(a, nil)))
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, cons(a, nil)), cons(b, 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)) <= True
  _r_2(nil) <= True
  _r_3(b) <= 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_3(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(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>
{
  _r_3(b) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0)
  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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_yesqw_0, cons(b, _zjsqw_1))  ;  _idb -> cons(_zesqw_0, cons(_xjsqw_0, nil))  ;  y -> a  ;  z -> cons(a, cons(b, _yjsqw_1))
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> cons(b, cons(_vhsqw_0, nil))  ;  _sdb -> s(s(z))  ;  l -> cons(b, nil)
}

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

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

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


-------------------------------------------
Step 17, which took 0.316271 s (model generation: 0.315018,  model checking: 0.001253):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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(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(cons(b, cons(a, nil)), cons(b, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, cons(b, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= insert(a, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(a, nil), cons(b, nil)) <= insert(a, nil, cons(b, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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(a, nil), cons(b, cons(a, nil)))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, cons(a, nil)), cons(a, nil))
False <= length(cons(b, cons(a, nil)), s(s(z))) /\ sort(cons(b, nil), cons(b, cons(a, nil)))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, cons(a, nil)), cons(b, 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
  _r_3(b) <= True
  insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_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_3(x_2_0)
  insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(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>
{
  _r_1(nil) <= True
  _r_3(b) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0)
  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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_omsqw_0, cons(b, nil))  ;  _idb -> cons(b, cons(_xrsqw_0, nil))  ;  y -> b  ;  z -> cons(a, cons(b, _yrsqw_1))
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(s(z))  ;  _rdb -> cons(b, nil)  ;  _sdb -> s(z)  ;  l -> cons(b, cons(_wosqw_0, nil))
}

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

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

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


-------------------------------------------
Step 18, which took 0.449049 s (model generation: 0.447763,  model checking: 0.001286):

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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb) -> 0
sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb) -> 0
eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb) -> 0
length(cons(x, ll), s(_mdb)) <= length(ll, _mdb) -> 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, cons(a, nil)), cons(a, cons(b, 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(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(cons(b, cons(a, nil)), cons(b, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, cons(b, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= insert(a, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(a, nil), cons(b, nil)) <= insert(a, nil, cons(b, nil))
sort(cons(b, cons(a, cons(b, nil))), cons(b, cons(a, nil))) <= insert(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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)))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, cons(a, nil)), cons(b, 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(a) <= 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) /\ _r_2(x_2_0)
  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(nil) <= True
  _r_2(a) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) /\ length(x_0_1, x_1_0)
  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_2(a) <= True
  _r_3(b) <= True
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ sort(x_0_1, x_1_1)
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0)
  sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ sort(x_0_1, x_1_1)
  sort(cons(x_0_0, x_0_1), nil) <= _r_3(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), _cdb) \/ leq(x, y) <= insert(x, z, _cdb)  :
No: ()

sort(cons(y, z), _idb) <= insert(y, _hdb, _idb) /\ sort(z, _hdb)  :
Yes: {
_hdb -> cons(_dtsqw_0, _dtsqw_1)  ;  _idb -> cons(b, _etsqw_1)  ;  y -> a  ;  z -> cons(b, _gtsqw_1)
}

eq_nat(_qdb, _sdb) <= length(_rdb, _sdb) /\ length(l, _qdb) /\ sort(l, _rdb)  :
Yes: {
_qdb -> s(z)  ;  _rdb -> nil  ;  _sdb -> z  ;  l -> cons(b, nil)
}

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

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

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


Total time: 1.695574
Learner time: 1.663858
Teacher time: 0.008663
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True
insert(a, cons(b, cons(a, nil)), cons(a, cons(b, 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(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(cons(b, cons(a, nil)), cons(b, nil)) <= True
sort(nil, nil) <= True
sort(cons(a, cons(a, cons(b, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(a, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil))
False <= insert(a, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil))
False <= insert(a, nil, cons(a, cons(a, nil)))
sort(cons(a, nil), cons(b, nil)) <= insert(a, nil, cons(b, nil))
sort(cons(b, cons(a, cons(b, nil))), cons(b, cons(a, nil))) <= insert(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil)))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil))
insert(b, cons(a, cons(b, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil))
sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(b, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, 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, 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)))
False <= leq(b, a)
False <= sort(cons(a, cons(a, nil)), cons(a, nil))
False <= sort(cons(a, cons(a, nil)), cons(b, nil))
False <= sort(cons(a, nil), cons(a, cons(a, nil)))
False <= sort(cons(b, nil), nil)
}