Solving ../../benchmarks/smtlib/true/merge_length_leq.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:
{
(leq, P:
{
leq(a, n2) <= True
leq(b, b) <= True
False <= leq(b, a)
}
)
(leqnat, P:
{
leqnat(z, n2) <= True
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2)
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2))
False <= leqnat(s(nn1), z)
}
)
(merge, F:
{
merge(cons(z, xs), nil, cons(z, xs)) <= True
merge(nil, y, y) <= True
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)
}
eq_eltlist(_fja, _gja) <= merge(_dja, _eja, _fja) /\ merge(_dja, _eja, _gja)
)
(append, F:
{
append(nil, l2, l2) <= True
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja)
}
eq_eltlist(_kja, _lja) <= append(_ija, _jja, _kja) /\ append(_ija, _jja, _lja)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)
}
eq_nat(_pja, _qja) <= plus(_nja, _oja, _pja) /\ plus(_nja, _oja, _qja)
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_rja)) <= length(ll, _rja)
}
eq_nat(_tja, _uja) <= length(_sja, _tja) /\ length(_sja, _uja)
)
}

properties:
{
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)
}


over-approximation: {append, length, merge, plus}
under-approximation: {append, leqnat, plus}

Clause system for inference is:

{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}


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

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


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


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



--
Equality automata are defined for: {elt, eltlist, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006186 s (model generation: 0.006076,  model checking: 0.000110):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  
}
]


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



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




Answer of teacher:

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

}

leq(a, n2) <= True  :
Yes: {
n2 -> b
}

leq(b, b) <= True  :
Yes: {

}

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
Yes: {

}

merge(nil, y, y) <= True  :
Yes: {
y -> nil
}

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 1, which took 0.007608 s (model generation: 0.007477,  model checking: 0.000131):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(nil, z) <= True
leq(a, b) <= True
leq(b, b) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, nil, nil) <= True
}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <elt * elt>
{
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
Yes: {
n2 -> a
}

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
Yes: {
y -> cons(_izjaa_0, _izjaa_1)
}

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> z  ;  _wja -> nil  ;  _xja -> z  ;  l1 -> nil  ;  l2 -> nil
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> z  ;  _yja -> z  ;  _zja -> nil  ;  l1 -> nil  ;  l2 -> nil
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
Yes: {
_cja -> cons(_zzjaa_0, _zzjaa_1)  ;  y2 -> a  ;  ys -> nil  ;  z -> b
}

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 2, which took 0.014303 s (model generation: 0.014110,  model checking: 0.000193):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
leq(b, a) \/ merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, a) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> z  ;  _wja -> cons(_oakaa_0, _oakaa_1)  ;  _xja -> s(_pakaa_0)  ;  l1 -> nil  ;  l2 -> cons(_rakaa_0, _rakaa_1)
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(_xakaa_0)  ;  _yja -> s(_yakaa_0)  ;  _zja -> cons(_zakaa_0, _zakaa_1)  ;  l1 -> nil  ;  l2 -> cons(_bbkaa_0, _bbkaa_1)
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
Yes: {

}

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 3, which took 0.017644 s (model generation: 0.017477,  model checking: 0.000167):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= leq(b, a)
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 4, which took 0.015809 s (model generation: 0.015676,  model checking: 0.000133):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= leq(b, a)
leqnat(s(z), z) <= leqnat(s(s(z)), s(z))
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

}

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 5, which took 0.011826 s (model generation: 0.011605,  model checking: 0.000221):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> s(s(_rckaa_0))  ;  _wja -> cons(_rbkaa_0, _rbkaa_1)  ;  _xja -> s(z)  ;  l1 -> cons(_tbkaa_0, _tbkaa_1)  ;  l2 -> nil
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(z)  ;  _yja -> s(s(_rckaa_0))  ;  _zja -> cons(_xbkaa_0, _xbkaa_1)  ;  l1 -> cons(_ybkaa_0, _ybkaa_1)  ;  l2 -> cons(_zbkaa_0, _zbkaa_1)
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 6, which took 0.012051 s (model generation: 0.011775,  model checking: 0.000276):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
length(cons(a, nil), s(z)) <= True
length(nil, z) <= True
leq(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= length(cons(a, nil), s(s(z)))
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> s(s(z))  ;  _wja -> cons(_uckaa_0, nil)  ;  _xja -> s(z)  ;  l1 -> cons(_wckaa_0, cons(_fekaa_0, nil))  ;  l2 -> cons(_xckaa_0, _xckaa_1)
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(z)  ;  _yja -> s(s(z))  ;  _zja -> cons(_kdkaa_0, nil)  ;  l1 -> nil  ;  l2 -> cons(_mdkaa_0, cons(_fekaa_0, nil))
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 7, which took 0.021099 s (model generation: 0.020851,  model checking: 0.000248):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

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

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 8, which took 0.024625 s (model generation: 0.024372,  model checking: 0.000253):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

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

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 9, which took 0.027214 s (model generation: 0.026936,  model checking: 0.000278):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
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(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  merge(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> s(s(_zikaa_0))  ;  _wja -> cons(a, _whkaa_1)  ;  _xja -> s(z)  ;  l1 -> cons(b, _yhkaa_1)  ;  l2 -> nil
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(z)  ;  _yja -> s(s(_zikaa_0))  ;  _zja -> cons(a, _hikaa_1)  ;  l1 -> nil  ;  l2 -> cons(b, _jikaa_1)
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 10, which took 0.028430 s (model generation: 0.028030,  model checking: 0.000400):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
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(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, nil, nil) <= True
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ merge(cons(b, nil), nil, cons(a, nil))
False <= length(cons(b, nil), s(s(z))) /\ merge(nil, cons(b, nil), cons(a, nil))
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
}

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  _r_1(nil, a) <= True
  merge(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_1_0)
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_0)
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
Yes: {
y -> cons(b, nil)
}

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> s(s(z))  ;  _wja -> cons(_akkaa_0, nil)  ;  _xja -> s(z)  ;  l1 -> cons(_ckkaa_0, cons(_smkaa_0, nil))  ;  l2 -> nil
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(z)  ;  _yja -> s(s(z))  ;  _zja -> cons(_gkkaa_0, nil)  ;  l1 -> cons(_hkkaa_0, nil)  ;  l2 -> cons(a, cons(_smkaa_0, nil))
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
Yes: {
_bja -> cons(a, _mlkaa_1)  ;  xs -> nil  ;  y2 -> b  ;  ys -> nil  ;  z -> b
}

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
Yes: {
_cja -> cons(_emkaa_0, _emkaa_1)  ;  xs -> cons(_ymkaa_0, _ymkaa_1)  ;  y2 -> a  ;  ys -> nil  ;  z -> b
}

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 11, which took 0.041441 s (model generation: 0.041049,  model checking: 0.000392):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
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(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, cons(b, nil), cons(b, nil)) <= True
merge(nil, nil, nil) <= True
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), nil, cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ merge(cons(b, nil), nil, cons(a, nil))
False <= length(cons(b, nil), s(s(z))) /\ merge(nil, cons(b, nil), cons(a, nil))
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(b, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, cons(a, nil)), nil, cons(a, nil))
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
merge(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) <= merge(nil, cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


;
merge ->
[
merge : <eltlist * eltlist * eltlist>
{
  _r_1(nil) <= True
  merge(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)
  merge(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1)
  merge(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1)
  merge(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
Yes: {
xs -> cons(_yqkaa_0, _yqkaa_1)
}

merge(nil, y, y) <= True  :
Yes: {
y -> cons(_dnkaa_0, cons(_yqkaa_0, _yqkaa_1))
}

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
No: ()

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
No: ()

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
Yes: {
_bja -> cons(_sokaa_0, _sokaa_1)  ;  xs -> cons(_tokaa_0, nil)  ;  y2 -> b  ;  ys -> nil  ;  z -> a
}

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
Yes: {
_cja -> cons(_qqkaa_0, _qqkaa_1)  ;  xs -> nil  ;  y2 -> a  ;  ys -> cons(_sqkaa_0, nil)  ;  z -> b
}

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


-------------------------------------------
Step 12, which took 0.060829 s (model generation: 0.060292,  model checking: 0.000537):

Clauses:
{
length(nil, z) <= True -> 0
leq(a, n2) <= True -> 0
leq(b, b) <= True -> 0
merge(cons(z, xs), nil, cons(z, xs)) <= True -> 0
merge(nil, y, y) <= True -> 0
append(cons(h1, t1), l2, cons(h1, _hja)) <= append(t1, l2, _hja) -> 0
leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja) -> 0
leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja) -> 0
length(cons(x, ll), s(_rja)) <= length(ll, _rja) -> 0
merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja) -> 0
False <= leq(b, a) -> 0
leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0
leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0
False <= leqnat(s(nn1), z) -> 0
leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja) -> 0
plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja) -> 0
}

Accumulated learning constraints:
{
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(a, a) <= True
leq(a, b) <= True
leq(b, b) <= True
leqnat(s(z), s(z)) <= True
leqnat(z, s(z)) <= True
leqnat(z, z) <= True
merge(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True
merge(cons(a, nil), nil, cons(a, nil)) <= True
merge(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
merge(nil, cons(a, nil), cons(a, nil)) <= True
merge(nil, cons(b, nil), cons(b, nil)) <= True
merge(nil, nil, nil) <= True
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, cons(a, nil)), nil, cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ merge(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ merge(cons(b, nil), nil, cons(a, nil))
False <= length(cons(b, nil), s(s(z))) /\ merge(nil, cons(b, nil), cons(a, nil))
False <= leq(b, a)
False <= leqnat(s(s(z)), s(z))
False <= leqnat(s(z), z)
merge(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, nil))) <= merge(cons(a, nil), cons(b, nil), cons(a, nil))
merge(cons(b, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, cons(a, nil)), nil, cons(a, nil))
merge(cons(b, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= merge(cons(b, nil), cons(a, nil), cons(a, nil))
merge(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) <= merge(cons(b, nil), nil, cons(a, nil))
merge(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) <= merge(nil, cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


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


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



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




Answer of teacher:

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

leq(a, n2) <= True  :
No: ()

leq(b, b) <= True  :
No: ()

merge(cons(z, xs), nil, cons(z, xs)) <= True  :
No: ()

merge(nil, y, y) <= True  :
No: ()

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

leqnat(_vja, _xja) <= length(_wja, _xja) /\ length(l1, _vja) /\ merge(l1, l2, _wja)  :
Yes: {
_vja -> s(s(s(z)))  ;  _wja -> cons(_irkaa_0, cons(_xukaa_0, nil))  ;  _xja -> s(s(z))  ;  l1 -> cons(_krkaa_0, cons(_wukaa_0, cons(_gvkaa_0, nil)))  ;  l2 -> nil
}

leqnat(_yja, _aka) <= length(_zja, _aka) /\ length(l2, _yja) /\ merge(l1, l2, _zja)  :
Yes: {
_aka -> s(s(z))  ;  _yja -> s(s(s(z)))  ;  _zja -> cons(_trkaa_0, cons(_xukaa_0, nil))  ;  l1 -> nil  ;  l2 -> cons(_vrkaa_0, cons(_wukaa_0, cons(_gvkaa_0, nil)))
}

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

merge(cons(z, xs), cons(y2, ys), cons(z, _bja)) <= leq(z, y2) /\ merge(xs, cons(y2, ys), _bja)  :
No: ()

False <= leq(b, a)  :
No: ()

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

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

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

leq(z, y2) \/ merge(cons(z, xs), cons(y2, ys), cons(y2, _cja)) <= merge(cons(z, xs), ys, _cja)  :
No: ()

plus(n, s(mm), s(_mja)) <= plus(n, mm, _mja)  :
No: ()


Total time: 0.356347
Learner time: 0.285726
Teacher time: 0.003339
Reasons for stopping: Yes: |_
name: None

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


;
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 : <elt * elt>
{
  leq(a, a) <= True
  leq(a, b) <= True
  leq(b, b) <= True
}
]


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


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


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



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