Solving ../../benchmarks/smtlib/true/append_length_leq_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:
{
(append, F:
{
append(nil, l2, l2) <= True
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)
}
eq_natlist(_wra, _xra) <= append(_ura, _vra, _wra) /\ append(_ura, _vra, _xra)
)
(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(_yra)) <= length(ll, _yra)
}
eq_nat(_asa, _bsa) <= length(_zra, _asa) /\ length(_zra, _bsa)
)
}

properties:
{
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)
}


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

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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.401372 seconds.
Yes: |_
name: None

append ->
[
append : <natlist * 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
  _r_1(nil, nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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.006115 s (model generation: 0.006058,  model checking: 0.000057):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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

append ->
[
append : <natlist * natlist * natlist>
{
  
}
]


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


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



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> nil
}

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

}

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.007059 s (model generation: 0.006942,  model checking: 0.000117):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(nil, nil, nil) <= True
length(nil, z) <= True
}

Current best model:
|_
name: None

append ->
[
append : <natlist * natlist * natlist>
{
  append(nil, 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:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_zhtd_0, _zhtd_1)
}

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> z  ;  _dsa -> nil  ;  _esa -> z  ;  l1 -> nil  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> nil  ;  l2 -> nil  ;  t1 -> nil
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
Yes: {
_yra -> 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.013638 s (model generation: 0.013540,  model checking: 0.000098):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(z, z) <= True
}

Current best model:
|_
name: None

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> z  ;  _dsa -> cons(_qitd_0, _qitd_1)  ;  _esa -> s(_ritd_0)  ;  l1 -> nil  ;  l2 -> cons(_titd_0, _titd_1)
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> cons(_uitd_0, _uitd_1)  ;  l2 -> cons(_vitd_0, _vitd_1)  ;  t1 -> nil
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.012014 s (model generation: 0.011939,  model checking: 0.000075):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

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

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

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

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


-------------------------------------------
Step 4, which took 0.013369 s (model generation: 0.013297,  model checking: 0.000072):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.013821 s (model generation: 0.013567,  model checking: 0.000254):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(_xjtd_0))  ;  _dsa -> cons(_hjtd_0, _hjtd_1)  ;  _esa -> s(z)  ;  l1 -> cons(_jjtd_0, _jjtd_1)  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.012138 s (model generation: 0.011906,  model checking: 0.000232):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= length(cons(z, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(z))  ;  _dsa -> cons(_aktd_0, nil)  ;  _esa -> s(z)  ;  l1 -> cons(_cktd_0, cons(_bltd_0, nil))  ;  l2 -> cons(_dktd_0, _dktd_1)
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.013951 s (model generation: 0.013722,  model checking: 0.000229):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= length(x_0_1, x_1_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, nil) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(z))  ;  _dsa -> cons(_pltd_0, nil)  ;  _esa -> s(z)  ;  l1 -> cons(_rltd_0, cons(_rmtd_0, nil))  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> cons(_wltd_0, _wltd_1)  ;  l2 -> cons(s(_vmtd_0), _xltd_1)  ;  t1 -> nil
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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 8, which took 0.015269 s (model generation: 0.014990,  model checking: 0.000279):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= length(x_0_1, x_2_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= length(x_0_1, x_2_0)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, nil) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(z))  ;  _dsa -> cons(s(z), nil)  ;  _esa -> s(z)  ;  l1 -> cons(_intd_0, cons(_potd_0, nil))  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> nil  ;  h1 -> s(_uotd_0)  ;  l2 -> nil  ;  t1 -> nil
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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 9, which took 0.028897 s (model generation: 0.028728,  model checking: 0.000169):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil)) /\ length(cons(s(z), nil), s(z)) /\ length(cons(z, cons(z, nil)), s(s(z)))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

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

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

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

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


-------------------------------------------
Step 10, which took 0.031822 s (model generation: 0.031457,  model checking: 0.000365):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil)) /\ length(cons(z, cons(z, nil)), s(s(z)))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
Yes: {
_yra -> s(z)  ;  ll -> cons(z, _lqtd_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 11, which took 0.033573 s (model generation: 0.033231,  model checking: 0.000342):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  _r_1(nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> cons(_urtd_0, _urtd_1)  ;  l2 -> cons(_vrtd_0, _vrtd_1)  ;  t1 -> cons(_wrtd_0, nil)
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.041479 s (model generation: 0.041064,  model checking: 0.000415):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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 <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_1(nil, nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(s(z)))  ;  _dsa -> cons(_wstd_0, cons(_gutd_0, nil))  ;  _esa -> s(s(z))  ;  l1 -> cons(_ystd_0, cons(_futd_0, cons(_putd_0, nil)))  ;  l2 -> cons(_zstd_0, _zstd_1)
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
No: ()

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.045164 s (model generation: 0.044875,  model checking: 0.000289):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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
leq(s(s(s(z))), s(s(z))) <= append(cons(z, cons(z, cons(z, nil))), cons(z, nil), cons(z, cons(z, nil))) /\ length(cons(z, cons(z, cons(z, nil))), s(s(s(z))))
False <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

append ->
[
append : <natlist * natlist * natlist>
{
  _r_1(nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= append(x_0_1, x_1_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, cons(x_2_0, x_2_1)) <= True
  append(nil, 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:

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> cons(_lvtd_0, _lvtd_1)  ;  l2 -> nil  ;  t1 -> cons(_nvtd_0, nil)
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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 14, which took 0.049716 s (model generation: 0.049246,  model checking: 0.000470):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa) -> 0
append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra) -> 0
length(cons(x, ll), s(_yra)) <= length(ll, _yra) -> 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:
{
append(cons(s(z), nil), nil, cons(s(z), nil)) <= True
append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, 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
leq(s(s(s(z))), s(s(z))) <= append(cons(z, cons(z, cons(z, nil))), cons(z, nil), cons(z, cons(z, nil))) /\ length(cons(z, cons(z, cons(z, nil))), s(s(s(z))))
False <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
False <= append(cons(z, cons(z, nil)), nil, cons(s(z), nil))
False <= append(cons(z, cons(z, nil)), nil, cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(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

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

append(nil, l2, l2) <= True  :
No: ()

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

leq(_csa, _esa) <= append(l1, l2, _dsa) /\ length(_dsa, _esa) /\ length(l1, _csa)  :
Yes: {
_csa -> s(s(s(z)))  ;  _dsa -> cons(_zwtd_0, cons(s(z), nil))  ;  _esa -> s(s(z))  ;  l1 -> cons(_bxtd_0, cons(_mytd_0, cons(_vytd_0, nil)))  ;  l2 -> cons(_cxtd_0, _cxtd_1)
}

append(cons(h1, t1), l2, cons(h1, _tra)) <= append(t1, l2, _tra)  :
Yes: {
_tra -> cons(s(_mztd_0), nil)  ;  l2 -> nil  ;  t1 -> cons(_qxtd_0, nil)
}

length(cons(x, ll), s(_yra)) <= length(ll, _yra)  :
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.401372
Learner time: 0.334562
Teacher time: 0.003463
Reasons for stopping: Yes: |_
name: None

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