Solving ../../benchmarks/smtlib/true/append_length_leq_elt.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{
append(nil, l2, l2) <= True
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj)
}
eq_eltlist(_bk, _ck) <= append(_zj, _ak, _bk) /\ append(_zj, _ak, _ck)
)
(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(_dk)) <= length(ll, _dk)
}
eq_nat(_fk, _gk) <= length(_ek, _fk) /\ length(_ek, _gk)
)
}

properties:
{
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)
}


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

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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.281664 seconds.
Yes: |_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _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) /\ _r_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, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005959 s (model generation: 0.005891,  model checking: 0.000068):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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 : <eltlist * eltlist * eltlist>
{
  
}
]


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


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



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




Answer of teacher:

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

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

}

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.006194 s (model generation: 0.006043,  model checking: 0.000151):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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 : <eltlist * eltlist * eltlist>
{
  append(nil, nil, nil) <= True
}
]


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


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



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




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> z  ;  _ik -> nil  ;  _jk -> z  ;  l1 -> nil  ;  l2 -> nil
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> z  ;  _lk -> nil  ;  _mk -> z  ;  l1 -> nil  ;  l2 -> nil
}

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
Yes: {
_dk -> 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.010978 s (model generation: 0.010875,  model checking: 0.000103):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(z, z) <= True
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> z  ;  _ik -> cons(_gnsd_0, _gnsd_1)  ;  _jk -> s(_hnsd_0)  ;  l1 -> nil  ;  l2 -> cons(_jnsd_0, _jnsd_1)
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> z  ;  _lk -> cons(_lnsd_0, _lnsd_1)  ;  _mk -> s(_mnsd_0)  ;  l1 -> cons(_nnsd_0, _nnsd_1)  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj)  :
Yes: {
_yj -> cons(_unsd_0, _unsd_1)  ;  l2 -> cons(_vnsd_0, _vnsd_1)  ;  t1 -> nil
}

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.014889 s (model generation: 0.014797,  model checking: 0.000092):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, 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 : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

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

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

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

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

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


-------------------------------------------
Step 4, which took 0.012467 s (model generation: 0.012391,  model checking: 0.000076):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, 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 : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.011542 s (model generation: 0.011396,  model checking: 0.000146):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, 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 : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> s(s(_hpsd_0))  ;  _ik -> cons(_hosd_0, _hosd_1)  ;  _jk -> s(z)  ;  l1 -> cons(_josd_0, _josd_1)  ;  l2 -> nil
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> s(s(_hpsd_0))  ;  _lk -> cons(_rosd_0, _rosd_1)  ;  _mk -> s(z)  ;  l1 -> nil  ;  l2 -> cons(_uosd_0, _uosd_1)
}

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.013282 s (model generation: 0.012826,  model checking: 0.000456):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, 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(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> s(s(z))  ;  _ik -> cons(_ppsd_0, nil)  ;  _jk -> s(z)  ;  l1 -> cons(_rpsd_0, cons(_vqsd_0, nil))  ;  l2 -> nil
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> s(s(z))  ;  _lk -> cons(_upsd_0, nil)  ;  _mk -> s(z)  ;  l1 -> cons(_wpsd_0, _wpsd_1)  ;  l2 -> cons(_xpsd_0, cons(_vqsd_0, nil))
}

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.019056 s (model generation: 0.018855,  model checking: 0.000201):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, 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(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * nat>
{
  _r_1(a, 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

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

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

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.021373 s (model generation: 0.021141,  model checking: 0.000232):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, 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(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * nat>
{
  _r_1(a, z) <= True
  _r_1(b, 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
Yes: {
_dk -> s(z)  ;  ll -> cons(b, _htsd_1)  ;  x -> b
}

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.024844 s (model generation: 0.024459,  model checking: 0.000385):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, cons(b, nil)), s(s(z))) <= True
length(cons(b, 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(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  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 : <eltlist * nat>
{
  _r_1(a, z) <= True
  _r_1(b, s(x_1_0)) <= True
  _r_1(b, 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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> s(s(_xvsd_0))  ;  _ik -> cons(b, _musd_1)  ;  _jk -> s(z)  ;  l1 -> cons(b, _ousd_1)  ;  l2 -> nil
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> s(s(_xvsd_0))  ;  _lk -> cons(b, _wusd_1)  ;  _mk -> s(z)  ;  l1 -> nil  ;  l2 -> cons(b, _zusd_1)
}

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

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

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

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

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


-------------------------------------------
Step 10, which took 0.025940 s (model generation: 0.025533,  model checking: 0.000407):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, cons(b, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, cons(b, nil)), s(s(z))) <= True
length(cons(b, 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(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
False <= append(nil, cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _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_1_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 : <eltlist * nat>
{
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0)
  length(nil, z) <= True
}
]


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> s(s(z))  ;  _ik -> cons(_kwsd_0, nil)  ;  _jk -> s(z)  ;  l1 -> cons(_mwsd_0, cons(_vysd_0, nil))  ;  l2 -> cons(_nwsd_0, nil)
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> s(s(z))  ;  _lk -> cons(_zwsd_0, nil)  ;  _mk -> s(z)  ;  l1 -> nil  ;  l2 -> cons(_cxsd_0, cons(_kysd_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj)  :
Yes: {
_yj -> cons(_gxsd_0, _gxsd_1)  ;  l2 -> cons(_hxsd_0, cons(_mysd_0, _mysd_1))  ;  t1 -> nil
}

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

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

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

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


-------------------------------------------
Step 11, which took 0.031874 s (model generation: 0.031572,  model checking: 0.000302):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, cons(b, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, cons(b, nil)), s(s(z))) <= True
length(cons(b, 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(a, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(nil, cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _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) /\ _r_1(x_1_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)) <= _r_1(x_1_1)
  append(nil, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_zysd_0, cons(_abtd_0, _abtd_1))
}

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
No: ()

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj)  :
Yes: {
_yj -> cons(_uzsd_0, _uzsd_1)  ;  l2 -> cons(_vzsd_0, nil)  ;  t1 -> cons(_wzsd_0, nil)
}

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.038860 s (model generation: 0.038354,  model checking: 0.000506):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk) -> 0
leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk) -> 0
append(cons(h1, t1), l2, cons(h1, _yj)) <= append(t1, l2, _yj) -> 0
length(cons(x, ll), s(_dk)) <= length(ll, _dk) -> 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(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
length(cons(a, cons(b, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(cons(b, cons(b, nil)), s(s(z))) <= True
length(cons(b, 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(a, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z)))
False <= append(nil, cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(s(z)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _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) /\ _r_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, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|




Answer of teacher:

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

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

leq(_hk, _jk) <= append(l1, l2, _ik) /\ length(_ik, _jk) /\ length(l1, _hk)  :
Yes: {
_hk -> s(s(s(z)))  ;  _ik -> cons(_kbtd_0, cons(_fdtd_0, nil))  ;  _jk -> s(s(z))  ;  l1 -> cons(_mbtd_0, cons(_edtd_0, cons(_odtd_0, nil)))  ;  l2 -> nil
}

leq(_kk, _mk) <= append(l1, l2, _lk) /\ length(_lk, _mk) /\ length(l2, _kk)  :
Yes: {
_kk -> s(s(s(z)))  ;  _lk -> cons(_ubtd_0, cons(_fdtd_0, nil))  ;  _mk -> s(s(z))  ;  l1 -> nil  ;  l2 -> cons(_xbtd_0, cons(_edtd_0, cons(_odtd_0, nil)))
}

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

length(cons(x, ll), s(_dk)) <= length(ll, _dk)  :
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.281664
Learner time: 0.234133
Teacher time: 0.003125
Reasons for stopping: Yes: |_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _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) /\ _r_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, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
}
]


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


;
leq ->
[
leq : <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: {elt, eltlist, nat}
_|