Solving ../../benchmarks/smtlib/true/length_reverse_eq.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, _mg)) <= append(t1, l2, _mg)
}
eq_eltlist(_pg, _qg) <= append(_ng, _og, _pg) /\ append(_ng, _og, _qg)
)
(reverse, F:
{
reverse(nil, nil) <= True
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)
}
eq_eltlist(_ug, _vg) <= reverse(_tg, _ug) /\ reverse(_tg, _vg)
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_wg)) <= length(ll, _wg)
}
eq_nat(_yg, _zg) <= length(_xg, _yg) /\ length(_xg, _zg)
)
}

properties:
{
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)
}


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

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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 0
}


Solving took 17.021001 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)) <= 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)
  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
}
]


;
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.006063 s (model generation: 0.005997,  model checking: 0.000066):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
length ->
[
length : <eltlist * 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006526 s (model generation: 0.006459,  model checking: 0.000067):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
}
]


;
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(_mcgr_0, _mcgr_1)
}

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

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

reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.008564 s (model generation: 0.008477,  model checking: 0.000087):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> nil  ;  _sg -> cons(_tcgr_0, _tcgr_1)  ;  t1 -> nil
}

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_vcgr_0, _vcgr_1)  ;  l2 -> cons(_wcgr_0, _wcgr_1)  ;  t1 -> nil
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 3, which took 0.021240 s (model generation: 0.021078,  model checking: 0.000162):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(z)  ;  _bh -> cons(_zcgr_0, _zcgr_1)  ;  _ch -> s(s(_hdgr_0))  ;  l1 -> cons(_bdgr_0, _bdgr_1)
}

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


-------------------------------------------
Step 4, which took 0.013424 s (model generation: 0.013286,  model checking: 0.000138):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
reverse(cons(a, nil), cons(a, nil)) <= True
reverse(nil, nil) <= True
False <= length(cons(a, nil), 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)) <= length(x_0_1, x_1_0)
  length(nil, 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(z)  ;  _bh -> cons(_jdgr_0, cons(_aegr_0, nil))  ;  _ch -> s(s(z))  ;  l1 -> cons(_ldgr_0, nil)
}

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


-------------------------------------------
Step 5, which took 0.011388 s (model generation: 0.011288,  model checking: 0.000100):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), 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)) <= length(x_0_1, x_1_0)
  length(nil, 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> nil  ;  _sg -> cons(_kegr_0, cons(_uegr_0, _uegr_1))  ;  t1 -> nil
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 6, which took 0.011902 s (model generation: 0.011732,  model checking: 0.000170):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), 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)) <= 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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_wegr_0, nil)  ;  _sg -> cons(_xegr_0, nil)  ;  t1 -> cons(_yegr_0, nil)
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 7, which took 0.012824 s (model generation: 0.012603,  model checking: 0.000221):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), 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)) <= 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(cons(x_0_0, x_0_1), nil) <= True
  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
}
]


;
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(cons(x_0_0, x_0_1), nil) <= 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_yfgr_0, nil)  ;  _sg -> cons(_zfgr_0, cons(_ghgr_0, cons(_ihgr_0, _ihgr_1)))  ;  t1 -> cons(_aggr_0, nil)
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(z)  ;  _bh -> nil  ;  _ch -> z  ;  l1 -> cons(_oggr_0, nil)
}

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


-------------------------------------------
Step 8, which took 0.025111 s (model generation: 0.025024,  model checking: 0.000087):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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
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))
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, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, nil), nil)
}

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(z) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_1_0)
  length(nil, 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

length(cons(x, ll), s(_wg)) <= length(ll, _wg)  :
Yes: {
_wg -> s(z)  ;  ll -> cons(_ohgr_0, _ohgr_1)
}


-------------------------------------------
Step 9, which took 0.026752 s (model generation: 0.026604,  model checking: 0.000148):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), 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(cons(x_0_0, x_0_1), nil) <= True
  _r_1(nil, nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= 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)) <= _r_1(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
}
]


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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons(x_0_0, x_0_1), nil) <= True
  _r_1(nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(z))  ;  _bh -> cons(_aigr_0, nil)  ;  _ch -> s(z)  ;  l1 -> cons(_cigr_0, cons(_ligr_0, nil))
}

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


-------------------------------------------
Step 10, which took 0.025106 s (model generation: 0.024759,  model checking: 0.000347):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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))
False <= append(nil, cons(a, nil), cons(a, cons(a, nil)))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
}

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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(s(z)))  ;  _bh -> cons(_tjgr_0, cons(_ikgr_0, nil))  ;  _ch -> s(s(z))  ;  l1 -> cons(_vjgr_0, cons(_hkgr_0, cons(_vkgr_0, nil)))
}

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


-------------------------------------------
Step 11, which took 0.061102 s (model generation: 0.060834,  model checking: 0.000268):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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))
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, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), 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)) <= reverse(x_0_1, x_1_1)
  _r_1(nil, nil) <= True
  _r_2(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_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)) <= _r_1(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, x_1_1)
  reverse(nil, cons(x_1_0, x_1_1)) <= True
  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
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  _r_1(nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  reverse(nil, 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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_flgr_0, _flgr_1)  ;  _sg -> cons(_glgr_0, cons(_lmgr_0, _lmgr_1))  ;  t1 -> nil
}

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_olgr_0, cons(_fmgr_0, nil))  ;  l2 -> cons(_plgr_0, cons(_emgr_0, nil))  ;  t1 -> nil
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> z  ;  _bh -> cons(_wlgr_0, nil)  ;  _ch -> s(z)  ;  l1 -> nil
}

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


-------------------------------------------
Step 12, which took 0.091211 s (model generation: 0.090908,  model checking: 0.000303):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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)))
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, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, 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)) <= True
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_2(nil, nil) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_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_2(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
}
]


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


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_2(nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(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(_smgr_0, cons(_nngr_0, nil))
}

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

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

reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_tmgr_0, nil)  ;  _sg -> cons(_umgr_0, cons(_wngr_0, nil))  ;  t1 -> cons(_vmgr_0, nil)
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(z))  ;  _bh -> cons(_gngr_0, cons(_pngr_0, cons(_eogr_0, nil)))  ;  _ch -> s(s(s(z)))  ;  l1 -> cons(_ingr_0, cons(_ongr_0, nil))
}

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


-------------------------------------------
Step 13, which took 0.087096 s (model generation: 0.086710,  model checking: 0.000386):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 0
}

Accumulated learning constraints:
{
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, nil), s(z)) <= True
length(nil, 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, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, 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)) <= 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_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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_nogr_0, cons(_mpgr_0, nil))  ;  _sg -> cons(_oogr_0, cons(_kpgr_0, nil))  ;  t1 -> cons(_pogr_0, cons(_lpgr_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_togr_0, cons(_jpgr_0, nil))  ;  l2 -> cons(_uogr_0, nil)  ;  t1 -> cons(_vogr_0, _vogr_1)
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 14, which took 0.134007 s (model generation: 0.133603,  model checking: 0.000404):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, 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)) <= _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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_jqgr_0, nil)  ;  l2 -> cons(_kqgr_0, cons(_ergr_0, nil))  ;  t1 -> cons(_lqgr_0, nil)
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 15, which took 0.213985 s (model generation: 0.213100,  model checking: 0.000885):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, 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)) <= _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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_usgr_0, cons(_avgr_0, cons(_gwgr_0, nil)))  ;  l2 -> cons(_vsgr_0, cons(_zugr_0, cons(_fwgr_0, nil)))  ;  t1 -> nil
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 16, which took 0.332989 s (model generation: 0.332099,  model checking: 0.000890):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, 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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> nil  ;  _sg -> cons(_wwgr_0, cons(_vzgr_0, cons(_iahr_0, nil)))  ;  t1 -> nil
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 17, which took 0.344349 s (model generation: 0.343548,  model checking: 0.000801):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, 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)) <= _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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg)  :
Yes: {
_mg -> cons(_tbhr_0, cons(_jehr_0, cons(_qehr_0, nil)))  ;  l2 -> cons(_ubhr_0, cons(_kehr_0, nil))  ;  t1 -> cons(_vbhr_0, nil)
}

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 18, which took 0.717451 s (model generation: 0.716355,  model checking: 0.001096):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, 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)) <= 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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_vfhr_0, nil)  ;  _sg -> cons(_wfhr_0, cons(_mjhr_0, cons(_sjhr_0, cons(_bjhr_0, nil))))  ;  t1 -> cons(_xfhr_0, nil)
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


-------------------------------------------
Step 19, which took 0.501475 s (model generation: 0.500323,  model checking: 0.001152):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, 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
}
]


;
reverse ->
[
reverse : <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)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, cons(x_1_0, x_1_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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_hlhr_0, cons(_mrhr_0, nil))  ;  _sg -> cons(_ilhr_0, nil)  ;  t1 -> cons(_jlhr_0, cons(_nrhr_0, nil))
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> z  ;  _bh -> cons(_mohr_0, cons(_wohr_0, nil))  ;  _ch -> s(s(z))  ;  l1 -> nil
}

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


-------------------------------------------
Step 20, which took 0.593897 s (model generation: 0.591834,  model checking: 0.002063):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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 <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, cons(a, nil)))
False <= reverse(nil, cons(a, 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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(z)  ;  _bh -> cons(_nyhr_0, cons(_mzhr_0, cons(_pzhr_0, nil)))  ;  _ch -> s(s(s(z)))  ;  l1 -> cons(_pyhr_0, nil)
}

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


-------------------------------------------
Step 21, which took 0.517681 s (model generation: 0.505888,  model checking: 0.011793):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, cons(a, nil)))
False <= reverse(nil, cons(a, 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)) <= 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(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_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
}
]


;
reverse ->
[
reverse : <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)
  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(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(z))  ;  _bh -> nil  ;  _ch -> z  ;  l1 -> cons(_ofir_0, cons(_xfir_0, nil))
}

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


-------------------------------------------
Step 22, which took 0.595810 s (model generation: 0.552640,  model checking: 0.043170):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(a, nil)), nil)
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, cons(a, nil)))
False <= reverse(nil, cons(a, 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(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), 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
}
]


;
reverse ->
[
reverse : <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)
  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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(s(s(z))))  ;  _bh -> cons(_atjr_0, cons(_rtjr_0, nil))  ;  _ch -> s(s(z))  ;  l1 -> cons(_ctjr_0, cons(_qtjr_0, cons(_dujr_0, cons(_gujr_0, nil))))
}

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


-------------------------------------------
Step 23, which took 4.614661 s (model generation: 4.613806,  model checking: 0.000855):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, 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, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, 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, 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, cons(a, cons(a, nil))), s(s(s(z)))) /\ reverse(cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= length(cons(a, nil), s(s(z)))
False <= reverse(cons(a, cons(a, nil)), cons(a, nil))
False <= reverse(cons(a, cons(a, nil)), nil)
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, cons(a, nil)))
False <= reverse(nil, 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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
No: ()

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
Yes: {
_ah -> s(s(z))  ;  _bh -> cons(_hjor_0, cons(_vjor_0, nil))  ;  _ch -> s(s(s(_ikor_0)))  ;  l1 -> cons(_jjor_0, cons(_tjor_0, nil))
}

length(cons(x, ll), s(_wg)) <= length(ll, _wg)  :
Yes: {
_wg -> s(s(_zjor_0))  ;  ll -> cons(_pjor_0, cons(_yjor_0, nil))
}


-------------------------------------------
Step 24, which took 3.882227 s (model generation: 3.881943,  model checking: 0.000284):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg) -> 0
append(cons(h1, t1), l2, cons(h1, _mg)) <= append(t1, l2, _mg) -> 0
eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh) -> 0
length(cons(x, ll), s(_wg)) <= length(ll, _wg) -> 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, 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, cons(a, nil))), s(s(s(z)))) <= True
length(cons(a, cons(a, nil)), s(s(z))) <= True
length(cons(a, nil), s(z)) <= True
length(nil, 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))
append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))))
False <= 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, cons(a, nil)))), s(s(s(s(z))))) /\ reverse(cons(a, cons(a, cons(a, cons(a, nil)))), 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 <= reverse(cons(a, cons(a, cons(a, nil))), cons(a, 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(a, nil)), nil)
False <= reverse(cons(a, nil), cons(a, cons(a, cons(a, nil))))
False <= reverse(cons(a, nil), cons(a, cons(a, nil)))
False <= reverse(cons(a, nil), nil)
False <= reverse(nil, cons(a, cons(a, nil)))
False <= reverse(nil, 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_3(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_2(x_2_1)
  _r_2(nil) <= True
  _r_3(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_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
}
]


;
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), _sg) <= append(_rg, cons(h1, nil), _sg) /\ reverse(t1, _rg)  :
Yes: {
_rg -> cons(_tkor_0, cons(_ulor_0, nil))  ;  _sg -> cons(_ukor_0, cons(_vlor_0, cons(_fmor_0, cons(_imor_0, _imor_1))))  ;  t1 -> cons(_vkor_0, cons(_wlor_0, nil))
}

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

eq_nat(_ah, _ch) <= length(_bh, _ch) /\ length(l1, _ah) /\ reverse(l1, _bh)  :
No: ()

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


Total time: 17.021001
Learner time: 12.790899
Teacher time: 0.065943
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)) <= 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)
  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
}
]


;
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}
_|