Solving ../../benchmarks/smtlib/true/length_reverse_eq_nat.smt2...

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



Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{
append(nil, l2, l2) <= True
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)
}
eq_natlist(_qk, _rk) <= append(_ok, _pk, _qk) /\ append(_ok, _pk, _rk)
)
(reverse, F:
{
reverse(nil, nil) <= True
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)
}
eq_natlist(_vk, _wk) <= reverse(_uk, _vk) /\ reverse(_uk, _wk)
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_xk)) <= length(ll, _xk)
}
eq_nat(_zk, _al) <= length(_yk, _al) /\ length(_yk, _zk)
)
}

properties:
{
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)
}


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), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}


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

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005996 s (model generation: 0.005941,  model checking: 0.000055):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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



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




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

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006348 s (model generation: 0.006288,  model checking: 0.000060):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(nil, nil, nil) <= True
length(nil, z) <= True
reverse(nil, nil) <= True
}

Current best model:
|_
name: None

append ->
[
append : <natlist * natlist * natlist>
{
  append(nil, nil, nil) <= True
}
]


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


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



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




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.011989 s (model generation: 0.011917,  model checking: 0.000072):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(nil, nil) <= True
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> nil  ;  _tk -> cons(_ipor_0, _ipor_1)  ;  t1 -> nil
}

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_kpor_0, _kpor_1)  ;  l2 -> cons(_lpor_0, _lpor_1)  ;  t1 -> nil
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 3, which took 0.020029 s (model generation: 0.019887,  model checking: 0.000142):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(z)  ;  _cl -> cons(_opor_0, _opor_1)  ;  _dl -> s(s(_wpor_0))  ;  l1 -> cons(_qpor_0, _qpor_1)
}

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


-------------------------------------------
Step 4, which took 0.015042 s (model generation: 0.014911,  model checking: 0.000131):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= length(cons(z, nil), s(s(z)))
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(z))  ;  _cl -> cons(_ypor_0, nil)  ;  _dl -> s(z)  ;  l1 -> cons(_aqor_0, cons(_pqor_0, nil))
}

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


-------------------------------------------
Step 5, which took 0.011759 s (model generation: 0.011603,  model checking: 0.000156):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= length(cons(z, nil), s(s(z)))
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> nil  ;  _tk -> cons(s(_jror_0), _zqor_1)  ;  t1 -> nil
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(z)  ;  _cl -> cons(z, cons(_wror_0, nil))  ;  _dl -> s(s(z))  ;  l1 -> cons(_eror_0, nil)
}

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


-------------------------------------------
Step 6, which took 0.012246 s (model generation: 0.012140,  model checking: 0.000106):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> nil  ;  _tk -> cons(_hsor_0, cons(_rsor_0, _rsor_1))  ;  t1 -> nil
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 7, which took 0.013422 s (model generation: 0.013281,  model checking: 0.000141):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, nil))) <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_tsor_0, nil)  ;  _tk -> cons(_usor_0, nil)  ;  t1 -> cons(_vsor_0, nil)
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 8, which took 0.031801 s (model generation: 0.031692,  model checking: 0.000109):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, nil)), cons(z, nil)) <= append(cons(z, nil), cons(z, nil), cons(z, nil))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, nil))) <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= length(cons(z, cons(z, nil)), s(s(z))) /\ reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
}

Current best model:
|_
name: None

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


;
length ->
[
length : <natlist * nat>
{
  _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 : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

length(cons(x, ll), s(_xk)) <= length(ll, _xk)  :
Yes: {
_xk -> s(z)  ;  ll -> cons(_ztor_0, _ztor_1)
}


-------------------------------------------
Step 9, which took 0.022948 s (model generation: 0.022755,  model checking: 0.000193):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_euor_0, nil)  ;  _tk -> cons(_fuor_0, cons(_cvor_0, cons(_hvor_0, _hvor_1)))  ;  t1 -> cons(_guor_0, nil)
}

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_nuor_0, cons(_gvor_0, nil))  ;  l2 -> cons(_ouor_0, cons(_fvor_0, nil))  ;  t1 -> nil
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 10, which took 0.041699 s (model generation: 0.040970,  model checking: 0.000729):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil)))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(s(z)))  ;  _cl -> cons(_mwor_0, cons(_bxor_0, nil))  ;  _dl -> s(s(z))  ;  l1 -> cons(_owor_0, cons(_axor_0, cons(_oxor_0, nil)))
}

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


-------------------------------------------
Step 11, which took 0.146022 s (model generation: 0.145676,  model checking: 0.000346):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil)))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_vxor_0, nil)  ;  _tk -> cons(_wxor_0, cons(_yyor_0, nil))  ;  t1 -> cons(_xxor_0, nil)
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(z))  ;  _cl -> cons(_iyor_0, cons(_ryor_0, cons(_gzor_0, nil)))  ;  _dl -> s(s(s(z)))  ;  l1 -> cons(_kyor_0, cons(_qyor_0, nil))
}

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


-------------------------------------------
Step 12, which took 0.117587 s (model generation: 0.117274,  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), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_pzor_0, cons(_oapr_0, nil))  ;  _tk -> cons(_qzor_0, cons(_mapr_0, nil))  ;  t1 -> cons(_rzor_0, cons(_napr_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_vzor_0, cons(_lapr_0, nil))  ;  l2 -> cons(_wzor_0, nil)  ;  t1 -> cons(_xzor_0, _xzor_1)
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 13, which took 0.174891 s (model generation: 0.174509,  model checking: 0.000382):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_lbpr_0, nil)  ;  l2 -> cons(_mbpr_0, cons(_gcpr_0, nil))  ;  t1 -> cons(_nbpr_0, nil)
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 14, which took 0.245100 s (model generation: 0.244436,  model checking: 0.000664):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_wdpr_0, cons(_cgpr_0, cons(_ihpr_0, nil)))  ;  l2 -> cons(_xdpr_0, cons(_bgpr_0, cons(_hhpr_0, nil)))  ;  t1 -> nil
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 15, which took 0.430026 s (model generation: 0.429161,  model checking: 0.000865):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> nil  ;  _tk -> cons(_yhpr_0, cons(_xkpr_0, cons(_klpr_0, nil)))  ;  t1 -> nil
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 16, which took 0.465599 s (model generation: 0.464863,  model checking: 0.000736):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_dmpr_0, cons(_wnpr_0, nil))  ;  _tk -> cons(_empr_0, cons(_vnpr_0, nil))  ;  h1 -> s(z)  ;  t1 -> cons(_fmpr_0, cons(_ynpr_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_ympr_0, cons(_rnpr_0, nil))  ;  l2 -> cons(s(_knpr_0), cons(_snpr_0, nil))  ;  t1 -> nil
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 17, which took 0.591410 s (model generation: 0.590597,  model checking: 0.000813):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk)  :
Yes: {
_nk -> cons(_nqpr_0, cons(_dtpr_0, cons(_ktpr_0, nil)))  ;  l2 -> cons(_oqpr_0, cons(_etpr_0, nil))  ;  t1 -> cons(_pqpr_0, nil)
}

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 18, which took 0.753269 s (model generation: 0.752054,  model checking: 0.001215):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_pupr_0, nil)  ;  _tk -> cons(_qupr_0, cons(_gypr_0, cons(_mypr_0, cons(_vxpr_0, nil))))  ;  t1 -> cons(_rupr_0, nil)
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


-------------------------------------------
Step 19, which took 0.846498 s (model generation: 0.845170,  model checking: 0.001328):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _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)) <= 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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_vzpr_0, cons(_fgqr_0, nil))  ;  _tk -> cons(_wzpr_0, nil)  ;  t1 -> cons(_xzpr_0, cons(_hgqr_0, nil))
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> z  ;  _cl -> cons(_gdqr_0, cons(_qdqr_0, nil))  ;  _dl -> s(s(z))  ;  l1 -> nil
}

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


-------------------------------------------
Step 20, which took 0.747938 s (model generation: 0.742706,  model checking: 0.005232):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, nil)) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= reverse(nil, cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _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_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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_ohqr_0, cons(_pgrr_0, cons(_sgrr_0, _sgrr_1)))  ;  _tk -> cons(_phqr_0, nil)  ;  t1 -> cons(_qhqr_0, nil)
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(z)  ;  _cl -> cons(_gfrr_0, cons(_dgrr_0, cons(_hgrr_0, nil)))  ;  _dl -> s(s(s(z)))  ;  l1 -> cons(_ifrr_0, nil)
}

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


-------------------------------------------
Step 21, which took 0.721741 s (model generation: 0.710026,  model checking: 0.011715):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= append(cons(z, cons(z, cons(z, nil))), cons(z, nil), cons(z, nil)) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, nil)) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, nil), nil, cons(z, cons(z, nil))) <= append(nil, nil, cons(z, nil))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= reverse(nil, cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _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)) <= reverse(x_0_1, x_1_1)
  reverse(cons(x_0_0, x_0_1), nil) <= _r_1(x_0_1)
  reverse(nil, nil) <= True
}
]



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




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(z))  ;  _cl -> nil  ;  _dl -> z  ;  l1 -> cons(_tprr_0, cons(_cqrr_0, nil))
}

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


-------------------------------------------
Step 22, which took 0.831203 s (model generation: 0.785203,  model checking: 0.046000):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= append(cons(z, cons(z, cons(z, nil))), cons(z, nil), cons(z, nil)) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, nil)) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, nil), nil, cons(z, cons(z, nil))) <= append(nil, nil, cons(z, nil))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, cons(z, nil)), nil)
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= reverse(nil, cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  _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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(s(s(z))))  ;  _cl -> cons(_fdtr_0, cons(_wdtr_0, nil))  ;  _dl -> s(s(z))  ;  l1 -> cons(_hdtr_0, cons(_vdtr_0, cons(_ietr_0, cons(_letr_0, nil))))
}

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


-------------------------------------------
Step 23, which took 7.753744 s (model generation: 7.752977,  model checking: 0.000767):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
False <= append(cons(z, cons(z, cons(z, nil))), cons(z, nil), cons(z, nil)) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, nil)) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
reverse(cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, nil), nil, cons(z, cons(z, nil))) <= append(nil, nil, cons(z, nil))
False <= length(cons(z, cons(z, cons(z, cons(z, nil)))), s(s(s(s(z))))) /\ reverse(cons(z, cons(z, cons(z, cons(z, nil)))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) /\ reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, cons(z, nil)), nil)
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= reverse(nil, cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

append ->
[
append : <natlist * natlist * natlist>
{
  _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_3(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_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1)
  append(nil, nil, nil) <= True
}
]


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



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




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
No: ()

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
Yes: {
_bl -> s(s(z))  ;  _cl -> cons(_htxr_0, cons(_stxr_0, nil))  ;  _dl -> s(s(s(_guxr_0)))  ;  l1 -> cons(_jtxr_0, cons(_qtxr_0, nil))
}

length(cons(x, ll), s(_xk)) <= length(ll, _xk)  :
Yes: {
_xk -> s(s(_vtxr_0))  ;  ll -> cons(_ltxr_0, cons(_utxr_0, nil))
}


-------------------------------------------
Step 24, which took 4.454541 s (model generation: 4.454286,  model checking: 0.000255):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk) -> 0
append(cons(h1, t1), l2, cons(h1, _nk)) <= append(t1, l2, _nk) -> 0
eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl) -> 0
length(cons(x, ll), s(_xk)) <= length(ll, _xk) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= True
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True
append(cons(z, nil), nil, cons(z, nil)) <= True
append(nil, cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
append(nil, cons(z, nil), cons(z, nil)) <= True
append(nil, nil, nil) <= True
length(cons(z, cons(z, cons(z, nil))), s(s(s(z)))) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
reverse(cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
reverse(cons(s(z), cons(z, cons(z, nil))), cons(z, cons(z, nil))) <= append(cons(z, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, nil)))
False <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, nil)))
reverse(cons(z, cons(z, cons(z, nil))), cons(z, nil)) <= append(cons(z, cons(z, nil)), cons(z, nil), cons(z, nil))
append(cons(z, cons(z, nil)), cons(z, cons(z, nil)), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil))
reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, cons(z, nil)))))
False <= append(cons(z, nil), cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(cons(z, nil), cons(z, nil), cons(z, nil))
append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil)))
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, cons(z, nil))))) <= append(nil, cons(z, cons(z, cons(z, nil))), cons(z, cons(z, cons(z, nil))))
reverse(cons(z, nil), cons(s(z), nil)) <= append(nil, cons(z, nil), cons(s(z), nil))
False <= append(nil, cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
append(cons(z, nil), nil, cons(z, cons(z, nil))) <= append(nil, nil, cons(z, nil))
False <= length(cons(z, cons(z, cons(z, cons(z, nil)))), s(s(s(s(z))))) /\ reverse(cons(z, cons(z, cons(z, cons(z, nil)))), cons(z, cons(z, nil)))
False <= length(cons(z, cons(z, nil)), s(s(s(z))))
False <= length(cons(z, nil), s(s(z)))
False <= reverse(cons(z, cons(z, cons(z, nil))), cons(z, cons(z, nil)))
False <= reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, nil))))
False <= reverse(cons(z, cons(z, nil)), cons(z, nil))
False <= reverse(cons(z, cons(z, nil)), nil)
False <= reverse(cons(z, nil), cons(z, cons(z, cons(z, nil))))
False <= reverse(cons(z, nil), cons(z, cons(z, nil)))
False <= reverse(nil, cons(z, cons(z, nil)))
}

Current best model:
|_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|




Answer of teacher:

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

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

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

reverse(cons(h1, t1), _tk) <= append(_sk, cons(h1, nil), _tk) /\ reverse(t1, _sk)  :
Yes: {
_sk -> cons(_puxr_0, cons(_qvxr_0, nil))  ;  _tk -> cons(_quxr_0, cons(_rvxr_0, cons(_bwxr_0, cons(_ewxr_0, _ewxr_1))))  ;  t1 -> cons(_ruxr_0, cons(_svxr_0, nil))
}

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

eq_nat(_bl, _dl) <= length(_cl, _dl) /\ length(l1, _bl) /\ reverse(l1, _cl)  :
No: ()

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


Total time: 26.163573
Learner time: 18.400323
Teacher time: 0.072525
Reasons for stopping: Yes: |_
name: None

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


;
reverse ->
[
reverse : <natlist * natlist>
{
  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: {nat, natlist}
_|