Solving ../../benchmarks/smtlib/true/length_cons_le_fun_nat.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:
{
(le, P:
{
le(z, s(nn2)) <= True
le(s(nn1), s(nn2)) <= le(nn1, nn2)
le(nn1, nn2) <= le(s(nn1), s(nn2))
False <= le(s(nn1), z)
False <= le(z, z)
}
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_sn)) <= length(ll, _sn)
}
eq_nat(_un, _vn) <= length(_tn, _un) /\ length(_tn, _vn)
)
(fcons, F:
{
fcons(x, l, cons(x, l)) <= True
}
eq_natlist(_yn, _zn) <= fcons(_wn, _xn, _yn) /\ fcons(_wn, _xn, _zn)
)
}

properties:
{
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)
}


over-approximation: {fcons, length}
under-approximation: {le}

Clause system for inference is:

{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}


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

fcons ->
[
fcons : <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(nil, cons(x_1_0, x_1_1)) <= True
  fcons(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)
  fcons(s(x_0_0), nil, cons(x_2_0, x_2_1)) <= True
  fcons(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  fcons(z, nil, cons(x_2_0, x_2_1)) <= True
}
]


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



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

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
Yes: {
l -> nil  ;  x -> z
}

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

}

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
No: ()

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006066 s (model generation: 0.005982,  model checking: 0.000084):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

fcons ->
[
fcons : <nat * natlist * natlist>
{
  fcons(z, nil, cons(x_2_0, x_2_1)) <= True
}
]


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
Yes: {
l -> nil  ;  x -> s(_oihq_0)
}

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
No: ()

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.008848 s (model generation: 0.008725,  model checking: 0.000123):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
Yes: {
l -> cons(_vihq_0, _vihq_1)  ;  x -> z
}

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
Yes: {
_ao -> z  ;  _bo -> cons(_yihq_0, _yihq_1)  ;  _co -> s(_zihq_0)  ;  l -> nil  ;  x -> s(_bjhq_0)
}

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 3, which took 0.013197 s (model generation: 0.013126,  model checking: 0.000071):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
Yes: {
l -> cons(_hjhq_0, _hjhq_1)  ;  x -> s(_ijhq_0)
}

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
Yes: {
_ao -> s(_jjhq_0)  ;  _bo -> cons(_kjhq_0, _kjhq_1)  ;  _co -> s(_ljhq_0)  ;  l -> cons(_mjhq_0, _mjhq_1)  ;  x -> z
}

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 4, which took 0.017149 s (model generation: 0.017076,  model checking: 0.000073):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
No: ()

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
No: ()

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 5, which took 0.014758 s (model generation: 0.014101,  model checking: 0.000657):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
No: ()

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
No: ()

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

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

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

False <= le(z, z)  :
Yes: {

}

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


-------------------------------------------
Step 6, which took 0.021142 s (model generation: 0.020855,  model checking: 0.000287):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
No: ()

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
Yes: {
_ao -> s(z)  ;  _bo -> cons(_zjhq_0, _zjhq_1)  ;  _co -> s(z)  ;  l -> cons(_bkhq_0, _bkhq_1)  ;  x -> s(_ckhq_0)
}

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

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

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

}

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 7, which took 0.021021 s (model generation: 0.020717,  model checking: 0.000304):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
No: ()

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
Yes: {
_ao -> s(z)  ;  _bo -> cons(_hlhq_0, cons(_vlhq_0, _vlhq_1))  ;  _co -> s(z)  ;  l -> cons(_jlhq_0, _jlhq_1)  ;  x -> z
}

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 8, which took 0.016397 s (model generation: 0.016220,  model checking: 0.000177):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
No: ()

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
Yes: {
_ao -> s(s(z))  ;  _bo -> cons(_mmhq_0, cons(_enhq_0, nil))  ;  _co -> s(s(z))  ;  l -> cons(_omhq_0, cons(_hnhq_0, nil))  ;  x -> z
}

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

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

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

False <= le(z, z)  :
No: ()

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


-------------------------------------------
Step 9, which took 0.018251 s (model generation: 0.018108,  model checking: 0.000143):

Clauses:
{
fcons(x, l, cons(x, l)) <= True -> 0
length(nil, z) <= True -> 0
le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
length(cons(x, ll), s(_sn)) <= length(ll, _sn) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

fcons(x, l, cons(x, l)) <= True  :
Yes: {
l -> cons(_wnhq_0, cons(_wohq_0, _wohq_1))  ;  x -> z
}

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

le(_ao, _co) <= fcons(x, l, _bo) /\ length(_bo, _co) /\ length(l, _ao)  :
No: ()

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

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

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

False <= le(z, z)  :
No: ()

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


Total time: 0.164277
Learner time: 0.140324
Teacher time: 0.001970
Reasons for stopping: Yes: |_
name: None

fcons ->
[
fcons : <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(nil, cons(x_1_0, x_1_1)) <= True
  fcons(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)
  fcons(s(x_0_0), nil, cons(x_2_0, x_2_1)) <= True
  fcons(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  fcons(z, nil, cons(x_2_0, x_2_1)) <= True
}
]


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



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