Solving ../../benchmarks/smtlib/true/isaplanner_prop68.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: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(leq, P:
{
leq(z, s(nn2)) <= True
leq(z, z) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_hia)) <= length(ll, _hia)
}
eq_nat(_jia, _kia) <= length(_iia, _jia) /\ length(_iia, _kia)
)
(delete, F:
{
delete(x, nil, nil) <= True
delete(h, cons(h, t), _lia) <= delete(h, t, _lia)
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)
}
eq_natlist(_pia, _qia) <= delete(_nia, _oia, _pia) /\ delete(_nia, _oia, _qia)
)
}

properties:
{
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)
}


over-approximation: {delete, length}
under-approximation: {leq}

Clause system for inference is:

{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}


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

delete ->
[
delete : <nat * natlist * natlist>
{
  _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(cons(x_0_0, x_0_1), nil) <= True
  _r_1(nil, nil) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



--
Equality automata are defined for: {nat, natlist}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006152 s (model generation: 0.006084,  model checking: 0.000068):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  
}
]


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


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



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




Answer of teacher:

delete(x, nil, nil) <= True  :
Yes: {
x -> z
}

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

}

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
No: ()

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 1, which took 0.007847 s (model generation: 0.007280,  model checking: 0.000567):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
delete(z, nil, nil) <= True
length(nil, z) <= True
}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(z, nil, nil) <= True
}
]


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


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



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




Answer of teacher:

delete(x, nil, nil) <= True  :
Yes: {
x -> s(_anrk_0)
}

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
Yes: {
_lia -> nil  ;  h -> z  ;  t -> nil
}

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> nil  ;  _sia -> z  ;  _tia -> z  ;  i -> z  ;  l -> nil
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
Yes: {
_mia -> nil  ;  h -> s(_knrk_0)  ;  t -> nil  ;  x -> z
}

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 2, which took 0.011291 s (model generation: 0.011158,  model checking: 0.000133):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
delete(s(z), nil, nil) <= True
delete(z, cons(s(z), nil), cons(s(z), nil)) <= True
delete(z, cons(z, nil), nil) <= True
delete(z, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(z, z) <= True
}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


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



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
Yes: {
_lia -> nil  ;  h -> s(_qnrk_0)  ;  t -> nil
}

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> nil  ;  _sia -> z  ;  _tia -> s(_znrk_0)  ;  i -> z  ;  l -> cons(_bork_0, _bork_1)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
Yes: {
_mia -> nil  ;  h -> z  ;  t -> nil  ;  x -> s(_jork_0)
}

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 3, which took 0.021108 s (model generation: 0.020987,  model checking: 0.000121):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
delete(s(z), cons(s(z), nil), nil) <= True
delete(s(z), cons(z, nil), cons(z, nil)) <= True
delete(s(z), nil, nil) <= True
delete(z, cons(s(z), nil), cons(s(z), nil)) <= True
delete(z, cons(z, nil), nil) <= True
delete(z, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
No: ()

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(_mork_0)  ;  nn2 -> z
}

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 4, which took 0.016677 s (model generation: 0.016547,  model checking: 0.000130):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
delete(s(z), cons(s(z), nil), nil) <= True
delete(s(z), cons(z, nil), cons(z, nil)) <= True
delete(s(z), nil, nil) <= True
delete(z, cons(s(z), nil), cons(s(z), nil)) <= True
delete(z, cons(z, nil), nil) <= True
delete(z, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(s(x_0_0), z) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
No: ()

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
Yes: {

}


-------------------------------------------
Step 5, which took 0.017574 s (model generation: 0.016976,  model checking: 0.000598):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
delete(s(z), cons(s(z), nil), nil) <= True
delete(s(z), cons(z, nil), cons(z, nil)) <= True
delete(s(z), nil, nil) <= True
delete(z, cons(s(z), nil), cons(s(z), nil)) <= True
delete(z, cons(z, nil), nil) <= True
delete(z, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_tork_0, _tork_1)  ;  _sia -> s(s(_kprk_0))  ;  _tia -> s(z)  ;  i -> z  ;  l -> cons(_xork_0, _xork_1)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 6, which took 0.019606 s (model generation: 0.018993,  model checking: 0.000613):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_rprk_0, cons(_qqrk_0, nil))  ;  _sia -> s(s(z))  ;  _tia -> s(z)  ;  i -> z  ;  l -> cons(_vprk_0, nil)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 7, which took 0.027497 s (model generation: 0.027318,  model checking: 0.000179):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  _r_1(z, z) <= True
  leq(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
No: ()

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> s(_nrrk_0)
}

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 8, which took 0.022176 s (model generation: 0.021915,  model checking: 0.000261):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
No: ()

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 9, which took 0.025873 s (model generation: 0.025604,  model checking: 0.000269):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _r_1(s(x_0_0)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_0)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(s(_ourk_0), _ntrk_1)  ;  _sia -> s(s(_rurk_0))  ;  _tia -> s(z)  ;  i -> z  ;  l -> cons(_rtrk_0, _rtrk_1)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 10, which took 0.029737 s (model generation: 0.029390,  model checking: 0.000347):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _r_1(s(x_0_0)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
Yes: {
_lia -> cons(_turk_0, _turk_1)  ;  h -> z  ;  t -> cons(s(_cwrk_0), _vurk_1)
}

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_wurk_0, _wurk_1)  ;  _sia -> s(s(_fwrk_0))  ;  _tia -> s(z)  ;  i -> s(_zurk_0)  ;  l -> cons(_avrk_0, _avrk_1)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 11, which took 0.022719 s (model generation: 0.022453,  model checking: 0.000266):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _r_1(nil) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_kwrk_0, cons(_ayrk_0, nil))  ;  _sia -> s(s(z))  ;  _tia -> s(z)  ;  i -> s(_nwrk_0)  ;  l -> cons(_owrk_0, nil)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
Yes: {
_mia -> cons(_uwrk_0, nil)  ;  h -> s(_vwrk_0)  ;  t -> cons(_wwrk_0, _wwrk_1)  ;  x -> z
}

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 12, which took 0.026481 s (model generation: 0.026157,  model checking: 0.000324):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(s(x_0_0), nil) <= True
  _r_1(z, nil) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1)
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
Yes: {
_lia -> cons(_kyrk_0, cons(_gbsk_0, _gbsk_1))  ;  h -> z  ;  t -> cons(s(_fbsk_0), _myrk_1)
}

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_syrk_0, cons(_bbsk_0, nil))  ;  _sia -> s(s(z))  ;  _tia -> s(z)  ;  i -> z  ;  l -> cons(s(_absk_0), nil)
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
Yes: {
_mia -> cons(_bzrk_0, nil)  ;  h -> z  ;  t -> cons(z, _dzrk_1)  ;  x -> s(_ezrk_0)
}

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


-------------------------------------------
Step 13, which took 0.032741 s (model generation: 0.032211,  model checking: 0.000530):

Clauses:
{
delete(x, nil, nil) <= True -> 0
length(nil, z) <= True -> 0
delete(h, cons(h, t), _lia) <= delete(h, t, _lia) -> 0
leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia) -> 0
eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia) -> 0
length(cons(x, ll), s(_hia)) <= length(ll, _hia) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons(x_0_0, x_0_1), nil) <= True
  _r_1(nil, nil) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

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

delete(h, cons(h, t), _lia) <= delete(h, t, _lia)  :
No: ()

leq(_sia, _tia) <= delete(i, l, _ria) /\ length(_ria, _sia) /\ length(l, _tia)  :
Yes: {
_ria -> cons(_xbsk_0, cons(_kesk_0, cons(_resk_0, nil)))  ;  _sia -> s(s(s(z)))  ;  _tia -> s(s(z))  ;  i -> s(_acsk_0)  ;  l -> cons(_bcsk_0, cons(_jesk_0, nil))
}

eq_nat(x, h) \/ delete(x, cons(h, t), cons(h, _mia)) <= delete(x, t, _mia)  :
No: ()

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

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()


Total time: 0.326154
Learner time: 0.283074
Teacher time: 0.004405
Reasons for stopping: Yes: |_
name: None

delete ->
[
delete : <nat * natlist * natlist>
{
  _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(cons(x_0_0, x_0_1), nil) <= True
  _r_1(nil, nil) <= True
  delete(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  delete(s(x_0_0), nil, nil) <= True
  delete(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  delete(z, cons(x_1_0, x_1_1), nil) <= True
  delete(z, nil, nil) <= True
}
]


;
length ->
[
length : <natlist * 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 : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]



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