Solving ../../benchmarks/smtlib/true/isaplanner_prop20.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 -> {ncons, nnil}
}
definition:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(insert_nat, F:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)
}
eq_natlist(_ve, _we) <= insert_nat(_te, _ue, _ve) /\ insert_nat(_te, _ue, _we)
)
(sort_nat, F:
{
sort_nat(nnil, nnil) <= True
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)
}
eq_natlist(_af, _bf) <= sort_nat(_ze, _af) /\ sort_nat(_ze, _bf)
)
(length_nat, F:
{
length_nat(nnil, z) <= True
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)
}
eq_nat(_ef, _ff) <= length_nat(_df, _ef) /\ length_nat(_df, _ff)
)
}

properties:
{
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)
}


over-approximation: {insert_nat, length_nat, sort_nat}
under-approximation: {}

Clause system for inference is:

{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}


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

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(nnil, ncons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(nnil) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
Yes: {
x -> z
}

length_nat(nnil, z) <= True  :
Yes: {

}

leq_nat(z, n2) <= True  :
Yes: {
n2 -> z
}

sort_nat(nnil, nnil) <= True  :
Yes: {

}

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 1, which took 0.007661 s (model generation: 0.006778,  model checking: 0.000883):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(nnil, z) <= True
leq_nat(z, z) <= True
sort_nat(nnil, nnil) <= True
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


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


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
Yes: {
x -> s(_wdxe_0)
}

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
Yes: {
n2 -> s(_xdxe_0)
}

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
Yes: {
_se -> ncons(_ydxe_0, _ydxe_1)  ;  x -> z  ;  y -> s(_aexe_0)  ;  z -> nnil
}

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> nnil  ;  _ye -> ncons(_dexe_0, _dexe_1)  ;  y -> z  ;  z -> nnil
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
Yes: {
_cf -> z  ;  ll -> nnil
}

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
Yes: {
x -> z  ;  y -> z
}

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

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


-------------------------------------------
Step 2, which took 0.012316 s (model generation: 0.012172,  model checking: 0.000144):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= True
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
Yes: {
_se -> ncons(_mexe_0, _mexe_1)  ;  x -> s(_nexe_0)  ;  y -> z  ;  z -> nnil
}

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
Yes: {
_gf -> s(z)  ;  _hf -> ncons(_rexe_0, _rexe_1)  ;  _if -> s(s(_dfxe_0))  ;  l -> ncons(_texe_0, _texe_1)
}

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
Yes: {
x -> s(_uexe_0)  ;  y -> s(_vexe_0)
}

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

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


-------------------------------------------
Step 3, which took 0.013678 s (model generation: 0.013356,  model checking: 0.000322):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) \/ leq_nat(s(z), z) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= length_nat(ncons(z, nnil), s(s(z)))
leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
Yes: {
_gf -> s(z)  ;  _hf -> ncons(_ffxe_0, ncons(_wfxe_0, nnil))  ;  _if -> s(s(z))  ;  l -> ncons(_hfxe_0, nnil)
}

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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

}


-------------------------------------------
Step 4, which took 0.013545 s (model generation: 0.013319,  model checking: 0.000226):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= length_nat(ncons(z, ncons(z, nnil)), s(s(z))) /\ sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> nnil  ;  _ye -> ncons(_pgxe_0, ncons(_khxe_0, _khxe_1))  ;  y -> z  ;  z -> nnil
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 5, which took 0.024239 s (model generation: 0.024066,  model checking: 0.000173):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, ncons(z, nnil)), s(s(z))) /\ sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  _r_1(z, z) <= True
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
Yes: {
_cf -> z  ;  ll -> nnil  ;  x -> s(_dixe_0)
}

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 6, which took 0.027708 s (model generation: 0.027514,  model checking: 0.000194):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, ncons(z, nnil)), s(s(z))) /\ sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= True
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  _r_1(s(x_0_0), z) <= True
  _r_1(z, z) <= True
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
Yes: {
_cf -> s(z)  ;  ll -> ncons(z, _jixe_1)  ;  x -> z
}

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 7, which took 0.027152 s (model generation: 0.026886,  model checking: 0.000266):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

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


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  _r_1(nnil) <= True
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> nnil  ;  _ye -> ncons(_ojxe_0, ncons(_rkxe_0, _rkxe_1))  ;  y -> s(_pjxe_0)  ;  z -> nnil
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
Yes: {
_gf -> s(s(z))  ;  _hf -> ncons(_akxe_0, nnil)  ;  _if -> s(z)  ;  l -> ncons(_ckxe_0, ncons(_tkxe_0, nnil))
}

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 8, which took 0.030068 s (model generation: 0.029754,  model checking: 0.000314):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

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


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> ncons(_klxe_0, nnil)  ;  _ye -> ncons(_llxe_0, nnil)  ;  y -> z  ;  z -> ncons(_nlxe_0, nnil)
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 9, which took 0.059858 s (model generation: 0.059380,  model checking: 0.000478):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= insert_nat(z, ncons(z, nnil), ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(ncons(x_0_0, x_0_1)) <= True
  _r_2(nnil) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= True
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> ncons(_ymxe_0, nnil)  ;  _ye -> ncons(_zmxe_0, nnil)  ;  y -> s(_anxe_0)  ;  z -> ncons(_bnxe_0, nnil)
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 10, which took 0.070055 s (model generation: 0.069571,  model checking: 0.000484):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
sort_nat(ncons(s(z), ncons(z, nnil)), ncons(z, nnil)) <= insert_nat(s(z), ncons(z, nnil), ncons(z, nnil))
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
False <= insert_nat(z, ncons(z, nnil), ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(nnil) <= True
  _r_2(ncons(x_0_0, x_0_1)) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> ncons(_wpxe_0, nnil)  ;  _ye -> ncons(_xpxe_0, ncons(_jrxe_0, ncons(_mrxe_0, _mrxe_1)))  ;  y -> z  ;  z -> ncons(_zpxe_0, nnil)
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 11, which took 0.083277 s (model generation: 0.082732,  model checking: 0.000545):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
sort_nat(ncons(s(z), ncons(z, nnil)), ncons(z, nnil)) <= insert_nat(s(z), ncons(z, nnil), ncons(z, nnil))
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
sort_nat(ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, ncons(z, nnil))))
False <= insert_nat(z, ncons(z, nnil), ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(nnil) <= True
  _r_2(ncons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
Yes: {
_se -> ncons(_trxe_0, ncons(_euxe_0, nnil))  ;  x -> s(_urxe_0)  ;  y -> z  ;  z -> ncons(_wrxe_0, _wrxe_1)
}

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> ncons(_nsxe_0, ncons(_ztxe_0, nnil))  ;  _ye -> ncons(_osxe_0, ncons(_xtxe_0, nnil))  ;  y -> z  ;  z -> ncons(_qsxe_0, ncons(_ytxe_0, nnil))
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
Yes: {
x -> z  ;  y -> z  ;  z -> ncons(_duxe_0, _duxe_1)
}

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

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


-------------------------------------------
Step 12, which took 0.133794 s (model generation: 0.132604,  model checking: 0.001190):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil)))
sort_nat(ncons(s(z), ncons(z, nnil)), ncons(z, nnil)) <= insert_nat(s(z), ncons(z, nnil), ncons(z, nnil))
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
sort_nat(ncons(z, ncons(z, ncons(z, nnil))), ncons(z, ncons(z, nnil))) <= insert_nat(z, ncons(z, ncons(z, nnil)), ncons(z, ncons(z, nnil))) /\ sort_nat(ncons(z, ncons(z, nnil)), ncons(z, ncons(z, nnil)))
sort_nat(ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, ncons(z, nnil))))
False <= insert_nat(z, ncons(z, nnil), ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(nnil) <= True
  _r_2(ncons(x_0_0, x_0_1)) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_1(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  _r_1(nnil) <= True
  _r_2(ncons(x_0_0, x_0_1)) <= True
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1)
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
No: ()

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
Yes: {
_gf -> s(s(s(z)))  ;  _hf -> ncons(_czxe_0, ncons(_faye_0, nnil))  ;  _if -> s(s(z))  ;  l -> ncons(_ezxe_0, ncons(_eaye_0, ncons(_saye_0, nnil)))
}

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


-------------------------------------------
Step 13, which took 0.135372 s (model generation: 0.134901,  model checking: 0.000471):

Clauses:
{
insert_nat(x, nnil, ncons(x, nnil)) <= True -> 0
length_nat(nnil, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
sort_nat(nnil, nnil) <= True -> 0
insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se) -> 0
sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe) -> 0
eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf) -> 0
length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
insert_nat(s(z), ncons(s(z), nnil), ncons(s(z), ncons(s(z), nnil))) <= True
insert_nat(s(z), nnil, ncons(s(z), nnil)) <= True
insert_nat(z, ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= True
insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, nnil))) <= True
insert_nat(z, nnil, ncons(z, nnil)) <= True
length_nat(ncons(s(z), nnil), s(z)) <= True
length_nat(ncons(z, ncons(z, nnil)), s(s(z))) <= True
length_nat(ncons(z, nnil), s(z)) <= True
length_nat(nnil, z) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
sort_nat(ncons(z, nnil), ncons(z, nnil)) <= True
sort_nat(nnil, nnil) <= True
insert_nat(s(z), ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil)))
sort_nat(ncons(s(z), ncons(z, nnil)), ncons(z, nnil)) <= insert_nat(s(z), ncons(z, nnil), ncons(z, nnil))
sort_nat(ncons(s(z), nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, ncons(z, nnil)))
insert_nat(s(z), ncons(z, nnil), ncons(z, ncons(z, nnil))) <= insert_nat(s(z), nnil, ncons(z, nnil))
sort_nat(ncons(z, ncons(z, ncons(z, nnil))), ncons(z, ncons(z, nnil))) <= insert_nat(z, ncons(z, ncons(z, nnil)), ncons(z, ncons(z, nnil))) /\ sort_nat(ncons(z, ncons(z, nnil)), ncons(z, ncons(z, nnil)))
sort_nat(ncons(z, ncons(z, nnil)), ncons(z, ncons(z, ncons(z, nnil)))) <= insert_nat(z, ncons(z, nnil), ncons(z, ncons(z, ncons(z, nnil))))
False <= insert_nat(z, ncons(z, nnil), ncons(z, nnil))
False <= insert_nat(z, nnil, ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, ncons(z, ncons(z, nnil))), s(s(s(z)))) /\ sort_nat(ncons(z, ncons(z, ncons(z, nnil))), ncons(z, ncons(z, nnil)))
False <= length_nat(ncons(z, nnil), s(s(z)))
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= sort_nat(ncons(z, ncons(z, nnil)), ncons(z, nnil))
False <= sort_nat(ncons(z, nnil), ncons(z, ncons(z, nnil)))
}

Current best model:
|_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  _r_1(nnil, ncons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(nnil) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  _r_2(nnil) <= True
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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




Answer of teacher:

insert_nat(x, nnil, ncons(x, nnil)) <= True  :
No: ()

length_nat(nnil, z) <= True  :
No: ()

leq_nat(z, n2) <= True  :
No: ()

sort_nat(nnil, nnil) <= True  :
No: ()

insert_nat(x, ncons(y, z), ncons(y, _se)) \/ leq_nat(x, y) <= insert_nat(x, z, _se)  :
No: ()

sort_nat(ncons(y, z), _ye) <= insert_nat(y, _xe, _ye) /\ sort_nat(z, _xe)  :
Yes: {
_xe -> ncons(_xbye_0, nnil)  ;  _ye -> ncons(_ybye_0, ncons(_veye_0, nnil))  ;  y -> s(_zbye_0)  ;  z -> ncons(_acye_0, nnil)
}

eq_nat(_gf, _if) <= length_nat(_hf, _if) /\ length_nat(l, _gf) /\ sort_nat(l, _hf)  :
No: ()

length_nat(ncons(x, ll), s(_cf)) <= length_nat(ll, _cf)  :
No: ()

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

insert_nat(x, ncons(y, z), ncons(x, ncons(y, z))) <= leq_nat(x, y)  :
No: ()

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

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


Total time: 0.791517
Learner time: 0.639813
Teacher time: 0.005778
Reasons for stopping: Yes: |_
name: None

insert_nat ->
[
insert_nat : <nat * natlist * natlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(nnil, ncons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(nnil) <= True
  insert_nat(s(x_0_0), ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(s(x_0_0), nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  insert_nat(z, ncons(x_1_0, x_1_1), ncons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  insert_nat(z, nnil, ncons(x_2_0, x_2_1)) <= _r_2(x_2_1)
}
]


;
length_nat ->
[
length_nat : <natlist * nat>
{
  length_nat(ncons(x_0_0, x_0_1), s(x_1_0)) <= length_nat(x_0_1, x_1_0)
  length_nat(nnil, z) <= True
}
]


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


;
sort_nat ->
[
sort_nat : <natlist * natlist>
{
  sort_nat(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= sort_nat(x_0_1, x_1_1)
  sort_nat(nnil, nnil) <= True
}
]



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