Solving ../../benchmarks/smtlib/true/length_reverse_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, _cwa)) <= append(t1, l2, _cwa)
}
eq_eltlist(_fwa, _gwa) <= append(_dwa, _ewa, _fwa) /\ append(_dwa, _ewa, _gwa)
)
(reverse, F:
{
reverse(nil, nil) <= True
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)
}
eq_eltlist(_kwa, _lwa) <= reverse(_jwa, _kwa) /\ reverse(_jwa, _lwa)
)
(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(_mwa)) <= length(ll, _mwa)
}
eq_nat(_owa, _pwa) <= length(_nwa, _owa) /\ length(_nwa, _pwa)
)
}

properties:
{
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)
}


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

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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 27.505399 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)) <= _r_3(x_1_1)
  _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_3(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), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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>
{
  
}
]


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



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




Answer of teacher:

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

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

}

reverse(nil, nil) <= True  :
Yes: {

}

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.007771 s (model generation: 0.007692,  model checking: 0.000079):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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
reverse(nil, nil) <= 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>
{
  
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> z  ;  _rwa -> nil  ;  _swa -> z  ;  l1 -> nil
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> nil  ;  _uwa -> z  ;  _vwa -> z  ;  l1 -> nil
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> 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.009093 s (model generation: 0.008910,  model checking: 0.000183):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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
reverse(nil, nil) <= 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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> nil  ;  _iwa -> cons(_ryxr_0, _ryxr_1)  ;  t1 -> nil
}

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_tyxr_0, _tyxr_1)  ;  l2 -> cons(_uyxr_0, _uyxr_1)  ;  t1 -> nil
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.023398 s (model generation: 0.023259,  model checking: 0.000139):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= 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, z) <= True
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

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

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

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

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


-------------------------------------------
Step 4, which took 0.012813 s (model generation: 0.012737,  model checking: 0.000076):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
leq(z, s(z)) <= leq(s(z), s(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(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

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

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

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

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


-------------------------------------------
Step 5, which took 0.011727 s (model generation: 0.011664,  model checking: 0.000063):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 6, which took 0.011630 s (model generation: 0.011452,  model checking: 0.000178):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(_yzxr_0))  ;  _rwa -> cons(_fzxr_0, _fzxr_1)  ;  _swa -> s(z)  ;  l1 -> cons(_hzxr_0, _hzxr_1)
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_izxr_0, _izxr_1)  ;  _uwa -> s(s(_yzxr_0))  ;  _vwa -> s(z)  ;  l1 -> cons(_lzxr_0, _lzxr_1)
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.011743 s (model generation: 0.011543,  model checking: 0.000200):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(z))  ;  _rwa -> cons(_bayr_0, nil)  ;  _swa -> s(z)  ;  l1 -> cons(_dayr_0, cons(_abyr_0, nil))
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_eayr_0, cons(_kbyr_0, nil))  ;  _uwa -> s(s(z))  ;  _vwa -> s(z)  ;  l1 -> cons(_hayr_0, nil)
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.012667 s (model generation: 0.012501,  model checking: 0.000166):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> nil  ;  _iwa -> cons(_ubyr_0, cons(_scyr_0, _scyr_1))  ;  t1 -> nil
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.020862 s (model generation: 0.020556,  model checking: 0.000306):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_ucyr_0, nil)  ;  _iwa -> cons(_vcyr_0, nil)  ;  t1 -> cons(_wcyr_0, nil)
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 10, which took 0.024553 s (model generation: 0.024347,  model checking: 0.000206):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> 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 11, which took 0.024322 s (model generation: 0.024144,  model checking: 0.000178):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> s(z)  ;  ll -> cons(b, _pfyr_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 12, which took 0.026509 s (model generation: 0.026238,  model checking: 0.000271):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(_thyr_0))  ;  _rwa -> cons(b, _pgyr_1)  ;  _swa -> s(z)  ;  l1 -> cons(b, _rgyr_1)
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(b, _sgyr_1)  ;  _uwa -> s(s(_hiyr_0))  ;  _vwa -> s(z)  ;  l1 -> cons(b, _vgyr_1)
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> s(z)  ;  ll -> cons(b, _xgyr_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 13, which took 0.029953 s (model generation: 0.029640,  model checking: 0.000313):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_siyr_0, nil)  ;  _iwa -> cons(_tiyr_0, cons(_ekyr_0, cons(_jkyr_0, _jkyr_1)))  ;  t1 -> cons(_uiyr_0, nil)
}

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_bjyr_0, cons(_ikyr_0, nil))  ;  l2 -> cons(_cjyr_0, cons(_hkyr_0, nil))  ;  t1 -> nil
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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.041816 s (model generation: 0.041293,  model checking: 0.000523):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil)))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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)) <= 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_2_1)
  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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(s(z)))  ;  _rwa -> cons(_olyr_0, cons(_vmyr_0, nil))  ;  _swa -> s(s(z))  ;  l1 -> cons(_qlyr_0, cons(_umyr_0, cons(_inyr_0, nil)))
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_vlyr_0, cons(_zmyr_0, cons(_onyr_0, nil)))  ;  _uwa -> s(s(s(z)))  ;  _vwa -> s(s(z))  ;  l1 -> cons(_ylyr_0, cons(_ymyr_0, nil))
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 15, which took 0.144385 s (model generation: 0.144068,  model checking: 0.000317):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
reverse(cons(a, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(a, nil), cons(a, nil))
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil)))
reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= length(cons(a, cons(a, nil)), s(s(z))) /\ reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(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(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_1(nil, z) <= True
  _r_2(b, z) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(z))  ;  _rwa -> cons(_xnyr_0, nil)  ;  _swa -> s(z)  ;  l1 -> cons(_znyr_0, cons(b, _woyr_1))
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_aoyr_0, cons(b, _gpyr_1))  ;  _uwa -> s(s(z))  ;  _vwa -> s(z)  ;  l1 -> cons(_doyr_0, nil)
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> s(z)  ;  ll -> cons(a, 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 16, which took 0.123937 s (model generation: 0.123611,  model checking: 0.000326):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_ppyr_0, cons(_yqyr_0, _yqyr_1))
}

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_qpyr_0, cons(_cryr_0, nil))  ;  _iwa -> cons(_rpyr_0, cons(_aryr_0, nil))  ;  t1 -> cons(_spyr_0, cons(_bryr_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_wpyr_0, cons(_gryr_0, nil))  ;  l2 -> cons(_xpyr_0, _xpyr_1)  ;  t1 -> cons(_ypyr_0, _ypyr_1)
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 17, which took 0.195463 s (model generation: 0.195013,  model checking: 0.000450):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

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)) <= _r_2(x_1_1)
  _r_2(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), cons(x_1_0, x_1_1), cons(x_2_0, 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)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(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
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_2(nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_oryr_0, cons(_ntyr_0, cons(_ptyr_0, _ptyr_1)))
}

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_yryr_0, nil)  ;  _iwa -> cons(_zryr_0, cons(_vtyr_0, nil))  ;  t1 -> cons(_asyr_0, nil)
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 18, which took 0.258347 s (model generation: 0.257877,  model checking: 0.000470):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_2(cons(x_0_0, x_0_1)) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

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

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

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

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


-------------------------------------------
Step 19, which took 0.245602 s (model generation: 0.245079,  model checking: 0.000523):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(s(z))) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_2(cons(x_0_0, x_0_1)) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

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

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

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

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


-------------------------------------------
Step 20, which took 0.202552 s (model generation: 0.202108,  model checking: 0.000444):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

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)) <= _r_1(x_0_1, x_1_1)
  _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(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_1_1)
  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)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_bzyr_0, nil)  ;  l2 -> cons(_czyr_0, cons(_kazr_0, nil))  ;  t1 -> cons(_dzyr_0, nil)
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 21, which took 0.320883 s (model generation: 0.319899,  model checking: 0.000984):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

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)) <= _r_1(x_0_1, x_1_1)
  _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(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_1_1) /\ _r_1(x_1_1, x_2_1)
  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)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_aczr_0, cons(_uezr_0, cons(_agzr_0, nil)))  ;  l2 -> cons(_bczr_0, cons(_tezr_0, cons(_zfzr_0, nil)))  ;  t1 -> nil
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 22, which took 0.546172 s (model generation: 0.545120,  model checking: 0.001052):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> nil  ;  _iwa -> cons(_qgzr_0, cons(_dkzr_0, cons(_qkzr_0, nil)))  ;  t1 -> nil
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 23, which took 0.625806 s (model generation: 0.624918,  model checking: 0.000888):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

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)) <= _r_1(x_0_1, x_1_1)
  _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  _r_2(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), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_0_1)
  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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa)  :
Yes: {
_cwa -> cons(_slzr_0, cons(_zozr_0, cons(_gqzr_0, nil)))  ;  l2 -> cons(_tlzr_0, cons(_yozr_0, nil))  ;  t1 -> cons(_ulzr_0, nil)
}

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 24, which took 1.013431 s (model generation: 1.012281,  model checking: 0.001150):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_rqzr_0, cons(_vuzr_0, nil))  ;  _iwa -> cons(_sqzr_0, nil)  ;  t1 -> cons(_tqzr_0, cons(_xuzr_0, nil))
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 25, which took 0.993716 s (model generation: 0.991391,  model checking: 0.002325):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_2(nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(s(z)))  ;  _rwa -> cons(_tcas_0, nil)  ;  _swa -> s(z)  ;  l1 -> cons(_vcas_0, cons(_jeas_0, cons(_veas_0, nil)))
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_wcas_0, cons(_ceas_0, cons(_jeas_0, cons(_veas_0, nil))))  ;  _uwa -> s(s(s(s(z))))  ;  _vwa -> s(s(z))  ;  l1 -> cons(_zcas_0, cons(_beas_0, nil))
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 26, which took 0.960570 s (model generation: 0.958735,  model checking: 0.001835):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil)))))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(z)) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_xgas_0, nil)  ;  _iwa -> cons(_ygas_0, cons(_wmas_0, cons(_zmas_0, cons(_cnas_0, _cnas_1))))  ;  t1 -> cons(_zgas_0, nil)
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 27, which took 0.983792 s (model generation: 0.980291,  model checking: 0.003501):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil)))))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil)))))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(z)) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ reverse(x_0_1, x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ reverse(x_0_1, x_1_1)
  reverse(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_eras_0, cons(_xcbs_0, _xcbs_1))  ;  _iwa -> cons(_fras_0, cons(_wcbs_0, cons(_ycbs_0, _ycbs_1)))  ;  t1 -> nil
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_uxas_0, cons(_nyas_0, nil))  ;  _uwa -> s(s(z))  ;  _vwa -> z  ;  l1 -> nil
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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 28, which took 8.803440 s (model generation: 8.802371,  model checking: 0.001069):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil)))))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil)))))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(z)) <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil))
False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
leq(s(s(z)), z) <= reverse(nil, cons(a, cons(a, nil)))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= reverse(nil, cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
No: ()

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
Yes: {
_qwa -> s(s(s(_zgbs_0)))  ;  _rwa -> cons(_gfbs_0, cons(_mgbs_0, nil))  ;  _swa -> s(s(z))  ;  l1 -> cons(_ifbs_0, cons(_kgbs_0, nil))
}

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
Yes: {
_twa -> cons(_nfbs_0, cons(_qgbs_0, nil))  ;  _uwa -> s(s(s(_zgbs_0)))  ;  _vwa -> s(s(z))  ;  l1 -> cons(_qfbs_0, cons(_ogbs_0, nil))
}

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
Yes: {
_mwa -> s(s(_ugbs_0))  ;  ll -> cons(_wfbs_0, cons(_tgbs_0, 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 29, which took 4.547582 s (model generation: 4.547218,  model checking: 0.000364):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa) -> 0
append(cons(h1, t1), l2, cons(h1, _cwa)) <= append(t1, l2, _cwa) -> 0
leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa) -> 0
leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa) -> 0
length(cons(x, ll), s(_mwa)) <= length(ll, _mwa) -> 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, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= True
append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True
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, cons(a, nil))), cons(a, cons(a, 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(a, cons(a, nil))), s(s(s(z)))) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= 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, z) <= True
reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil)))
reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil))
append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil)))))
False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(cons(a, nil), cons(a, nil), cons(a, nil))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil)))))
False <= length(cons(a, cons(a, nil)), s(s(s(z))))
False <= length(cons(a, nil), s(s(z)))
False <= length(cons(b, nil), s(s(z))) /\ reverse(cons(b, nil), cons(b, nil))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)))
leq(s(s(s(z))), s(z)) <= reverse(cons(a, cons(a, cons(a, nil))), cons(a, nil))
False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(b, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), cons(a, cons(b, nil)))
leq(s(s(z)), z) <= reverse(nil, cons(a, cons(a, nil)))
reverse(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= reverse(nil, cons(a, cons(a, nil)))
}

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), cons(x_2_0, x_2_1)) <= True
  _r_1(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  _r_1(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  _r_1(nil, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1)
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(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_1_1, x_2_1)
  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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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




Answer of teacher:

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

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

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _iwa) <= append(_hwa, cons(h1, nil), _iwa) /\ reverse(t1, _hwa)  :
Yes: {
_hwa -> cons(_mhbs_0, cons(_bjbs_0, nil))  ;  _iwa -> cons(_nhbs_0, cons(_cjbs_0, cons(_mjbs_0, cons(_pjbs_0, _pjbs_1))))  ;  t1 -> cons(_ohbs_0, cons(_djbs_0, nil))
}

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

leq(_qwa, _swa) <= length(_rwa, _swa) /\ length(l1, _qwa) /\ reverse(l1, _rwa)  :
No: ()

leq(_uwa, _vwa) <= length(_twa, _uwa) /\ length(l1, _vwa) /\ reverse(l1, _twa)  :
No: ()

length(cons(x, ll), s(_mwa)) <= length(ll, _mwa)  :
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: 27.505399
Learner time: 20.222072
Teacher time: 0.018649
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)) <= _r_3(x_1_1)
  _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_3(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), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  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)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(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
}
]


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



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