Solving ../../benchmarks/smtlib/true/length_reverse_leq_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, _dna)) <= append(t1, l2, _dna)
}
eq_natlist(_gna, _hna) <= append(_ena, _fna, _gna) /\ append(_ena, _fna, _hna)
)
(reverse, F:
{
reverse(nil, nil) <= True
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)
}
eq_natlist(_lna, _mna) <= reverse(_kna, _lna) /\ reverse(_kna, _mna)
)
(leq, P:
{
leq(z, s(nn2)) <= True
leq(z, z) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(length, F:
{
length(nil, z) <= True
length(cons(x, ll), s(_nna)) <= length(ll, _nna)
}
eq_nat(_pna, _qna) <= length(_ona, _pna) /\ length(_ona, _qna)
)
}

properties:
{
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)
}


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

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}


Solving took 32.644907 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)) <= _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
  _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_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_3(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
}
]


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


;
reverse ->
[
reverse : <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.006088 s (model generation: 0.005996,  model checking: 0.000092):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


;
leq ->
[
leq : <nat * 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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 1, which took 0.006444 s (model generation: 0.006348,  model checking: 0.000096):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

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


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


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


;
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(_bmbs_0, _bmbs_1)
}

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

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

reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> z  ;  _sna -> nil  ;  _tna -> z  ;  l1 -> nil
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> nil  ;  _vna -> z  ;  _wna -> z  ;  l1 -> nil
}

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

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

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

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


-------------------------------------------
Step 2, which took 0.009608 s (model generation: 0.009491,  model checking: 0.000117):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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
leq(z, 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
}
]


;
leq ->
[
leq : <nat * nat>
{
  leq(z, 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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> nil  ;  _jna -> cons(_qmbs_0, _qmbs_1)  ;  t1 -> nil
}

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_smbs_0, _smbs_1)  ;  l2 -> cons(_tmbs_0, _tmbs_1)  ;  t1 -> nil
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 3, which took 0.012836 s (model generation: 0.012717,  model checking: 0.000119):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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
leq(s(z), s(z)) <= True
leq(z, 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
}
]


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(z, 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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 4, which took 0.013500 s (model generation: 0.013402,  model checking: 0.000098):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 5, which took 0.015680 s (model generation: 0.015570,  model checking: 0.000110):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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
leq(s(z), s(z)) <= True
leq(z, z) <= True
reverse(cons(z, nil), cons(z, nil)) <= True
reverse(nil, nil) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
}

Current best model:
|_
name: None

append ->
[
append : <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
}
]


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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

}


-------------------------------------------
Step 6, which took 0.017138 s (model generation: 0.016913,  model checking: 0.000225):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

append ->
[
append : <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
}
]


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(_xnbs_0))  ;  _sna -> cons(_enbs_0, _enbs_1)  ;  _tna -> s(z)  ;  l1 -> cons(_gnbs_0, _gnbs_1)
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_hnbs_0, _hnbs_1)  ;  _vna -> s(s(_xnbs_0))  ;  _wna -> s(z)  ;  l1 -> cons(_knbs_0, _knbs_1)
}

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

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

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

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


-------------------------------------------
Step 7, which took 0.012699 s (model generation: 0.012455,  model checking: 0.000244):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

append ->
[
append : <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)) <= leq(x_0_0, x_1_0)
  length(nil, z) <= True
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, z) <= True
}
]


;
leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, 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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(z)  ;  _sna -> cons(s(z), _aobs_1)  ;  _tna -> s(s(z))  ;  l1 -> cons(z, _cobs_1)
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(s(z), _dobs_1)  ;  _vna -> s(s(z))  ;  _wna -> s(z)  ;  l1 -> cons(z, _gobs_1)
}

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

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

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

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


-------------------------------------------
Step 8, which took 0.014170 s (model generation: 0.013952,  model checking: 0.000218):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

append ->
[
append : <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
}
]


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(z))  ;  _sna -> cons(_zpbs_0, nil)  ;  _tna -> s(z)  ;  l1 -> cons(_bqbs_0, cons(_arbs_0, nil))
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_cqbs_0, cons(_arbs_0, nil))  ;  _vna -> s(s(z))  ;  _wna -> s(z)  ;  l1 -> cons(_fqbs_0, nil)
}

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

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

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

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


-------------------------------------------
Step 9, which took 0.014762 s (model generation: 0.014553,  model checking: 0.000209):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

append ->
[
append : <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
}
]


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> nil  ;  _jna -> cons(_krbs_0, cons(_isbs_0, _isbs_1))  ;  t1 -> nil
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 10, which took 0.022325 s (model generation: 0.021994,  model checking: 0.000331):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

append ->
[
append : <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
}
]


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_ksbs_0, nil)  ;  _jna -> cons(_lsbs_0, nil)  ;  t1 -> cons(_msbs_0, nil)
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 11, which took 0.035509 s (model generation: 0.035098,  model checking: 0.000411):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

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


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 12, which took 0.025617 s (model generation: 0.025356,  model checking: 0.000261):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_ivbs_0, nil)  ;  _jna -> cons(_jvbs_0, cons(_uwbs_0, cons(_zwbs_0, _zwbs_1)))  ;  t1 -> cons(_kvbs_0, nil)
}

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_rvbs_0, cons(_ywbs_0, nil))  ;  l2 -> cons(_svbs_0, cons(_xwbs_0, nil))  ;  t1 -> nil
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 13, which took 0.039225 s (model generation: 0.038681,  model checking: 0.000544):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


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

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(s(z)))  ;  _sna -> cons(_eybs_0, cons(_lzbs_0, nil))  ;  _tna -> s(s(z))  ;  l1 -> cons(_gybs_0, cons(_kzbs_0, cons(_yzbs_0, nil)))
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_lybs_0, cons(_pzbs_0, cons(_eacs_0, nil)))  ;  _vna -> s(s(s(z)))  ;  _wna -> s(s(z))  ;  l1 -> cons(_oybs_0, cons(_ozbs_0, nil))
}

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

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

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

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


-------------------------------------------
Step 14, which took 0.106878 s (model generation: 0.106512,  model checking: 0.000366):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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(s(z), nil), s(z)) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, 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)))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(s(s(z))), s(s(z))) <= 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)))
leq(s(s(s(z))), s(s(z))) <= 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 <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), 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) <= True
  _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  append(nil, nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


;
reverse ->
[
reverse : <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  :
Yes: {
l2 -> cons(_macs_0, cons(_vbcs_0, _vbcs_1))
}

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

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

reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_nacs_0, cons(_zbcs_0, nil))  ;  _jna -> cons(_oacs_0, cons(_xbcs_0, nil))  ;  t1 -> cons(_pacs_0, cons(_ybcs_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_tacs_0, cons(_dccs_0, nil))  ;  l2 -> cons(_uacs_0, _uacs_1)  ;  t1 -> cons(_vacs_0, _vacs_1)
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 15, which took 0.207676 s (model generation: 0.207180,  model checking: 0.000496):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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(s(z), nil), s(z)) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, z) <= 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, 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))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(s(s(z))), s(s(z))) <= 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)))
leq(s(s(s(z))), s(s(z))) <= 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 <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), 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_0_1, x_2_1)
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


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



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_lccs_0, cons(_kecs_0, cons(_mecs_0, _mecs_1)))
}

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

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

reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_vccs_0, nil)  ;  _jna -> cons(_wccs_0, cons(_secs_0, nil))  ;  t1 -> cons(_xccs_0, nil)
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 16, which took 0.240676 s (model generation: 0.240193,  model checking: 0.000483):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, 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))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(s(s(z))), s(s(z))) <= 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)))
leq(s(s(s(z))), s(s(z))) <= 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 <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), 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_2(cons(x_0_0, x_0_1)) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


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



--
Equality automata are defined for: {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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 17, which took 0.238711 s (model generation: 0.238186,  model checking: 0.000525):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, 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))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(s(s(z))), s(s(z))) <= 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)))
leq(s(s(s(z))), s(s(z))) <= 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)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(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_2(cons(x_0_0, x_0_1)) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


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



--
Equality automata are defined for: {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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 18, which took 0.223498 s (model generation: 0.222916,  model checking: 0.000582):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


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

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_yjcs_0, nil)  ;  l2 -> cons(_zjcs_0, cons(_hlcs_0, nil))  ;  t1 -> cons(_akcs_0, nil)
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 19, which took 0.329213 s (model generation: 0.328407,  model checking: 0.000806):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


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

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_xmcs_0, cons(_rpcs_0, cons(_xqcs_0, nil)))  ;  l2 -> cons(_ymcs_0, cons(_qpcs_0, cons(_wqcs_0, nil)))  ;  t1 -> nil
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 20, which took 0.567854 s (model generation: 0.567153,  model checking: 0.000701):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(z, cons(z, nil)), cons(z, nil), cons(z, cons(z, cons(z, nil)))) <= True
append(cons(z, nil), cons(z, cons(z, cons(z, nil))), cons(z, 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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(z, nil)), s(s(z))) <= True
length(cons(z, nil), s(z)) <= True
length(nil, z) <= True
leq(s(z), s(z)) <= True
leq(z, 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))
False <= append(nil, cons(z, nil), cons(z, cons(z, nil)))
False <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(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 <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(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_2(cons(x_0_0, x_0_1)) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= reverse(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]


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


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


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



--
Equality automata are defined for: {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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(s(z)))  ;  _sna -> cons(_gscs_0, cons(z, nil))  ;  _tna -> s(s(z))  ;  l1 -> cons(_iscs_0, cons(s(z), nil))
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_nscs_0, cons(z, nil))  ;  _vna -> s(s(z))  ;  _wna -> s(s(s(z)))  ;  l1 -> cons(_qscs_0, cons(s(z), nil))
}

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

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

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

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


-------------------------------------------
Step 21, which took 0.539551 s (model generation: 0.538587,  model checking: 0.000964):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> nil  ;  _jna -> cons(_wvcs_0, cons(_jzcs_0, cons(_wzcs_0, nil)))  ;  t1 -> nil
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 22, which took 0.582461 s (model generation: 0.581854,  model checking: 0.000607):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_pads_0, cons(_wcds_0, nil))  ;  _jna -> cons(_qads_0, cons(_vcds_0, nil))  ;  h1 -> s(z)  ;  t1 -> cons(_rads_0, cons(_ycds_0, nil))
}

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_kbds_0, cons(_rcds_0, nil))  ;  l2 -> cons(s(_kcds_0), cons(_scds_0, nil))  ;  t1 -> nil
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 23, which took 1.017705 s (model generation: 1.016903,  model checking: 0.000802):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


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

append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna)  :
Yes: {
_dna -> cons(_nfds_0, cons(_rids_0, cons(_yids_0, nil)))  ;  l2 -> cons(_ofds_0, cons(_sids_0, nil))  ;  t1 -> cons(_pfds_0, nil)
}

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 24, which took 1.463596 s (model generation: 1.462700,  model checking: 0.000896):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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, cons(z, nil))), cons(z, 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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(s(z), nil)), 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
leq(s(z), s(z)) <= True
leq(z, 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)))
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(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
False <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(z), nil)), cons(z, cons(z, nil)))
leq(s(s(z)), s(s(s(z)))) <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(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 <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(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>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(z) <= True
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) /\ leq(x_0_0, x_1_0)
  length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_1_0)
  length(nil, z) <= True
  leq(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0)
  leq(z, s(x_1_0)) <= _r_2(x_1_0)
  leq(z, z) <= True
}
]


;
leq ->
[
leq : <nat * nat>
{
  _r_2(z) <= True
  leq(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0)
  leq(z, s(x_1_0)) <= _r_2(x_1_0)
  leq(z, 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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(z))  ;  _sna -> cons(_slds_0, cons(_nods_0, _nods_1))  ;  _tna -> s(z)  ;  l1 -> cons(z, cons(_ppds_0, _ppds_1))
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(z, cons(_mpds_0, nil))  ;  _vna -> s(s(z))  ;  _wna -> s(z)  ;  l1 -> cons(_wmds_0, cons(_npds_0, nil))
}

length(cons(x, ll), s(_nna)) <= length(ll, _nna)  :
Yes: {
_nna -> s(s(z))  ;  ll -> cons(z, cons(_oods_0, _oods_1))  ;  x -> z
}

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

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

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


-------------------------------------------
Step 25, which took 1.390457 s (model generation: 1.389295,  model checking: 0.001162):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_jqds_0, cons(_nuds_0, nil))  ;  _jna -> cons(_kqds_0, nil)  ;  t1 -> cons(_lqds_0, cons(_puds_0, nil))
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 26, which took 1.558829 s (model generation: 1.556697,  model checking: 0.002132):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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_1(x_0_1) /\ _r_1(x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1)
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
No: ()

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
Yes: {
_rna -> s(s(s(s(z))))  ;  _sna -> cons(_lces_0, cons(_iees_0, nil))  ;  _tna -> s(s(z))  ;  l1 -> cons(_nces_0, cons(_hees_0, cons(_aees_0, cons(_dees_0, nil))))
}

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_sces_0, cons(_mees_0, cons(_rdes_0, cons(_dees_0, nil))))  ;  _vna -> s(s(s(s(z))))  ;  _wna -> s(s(z))  ;  l1 -> cons(_vces_0, cons(_lees_0, nil))
}

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

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

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

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


-------------------------------------------
Step 27, which took 1.598971 s (model generation: 1.597186,  model checking: 0.001785):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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, cons(z, nil))), cons(z, 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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(s(z), nil)), s(s(z))) <= 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
leq(s(s(z)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, 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))
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)))
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(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
False <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(z), nil)), cons(z, cons(z, nil)))
leq(s(s(z)), s(s(s(z)))) <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(z), nil)), cons(z, cons(z, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= 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)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(z, cons(z, cons(z, cons(z, nil)))), s(s(s(s(z))))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil)))))
False <= length(cons(z, cons(z, nil)), s(z))
False <= length(cons(z, nil), s(s(z)))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(s(z))) <= leq(s(z), s(s(s(z))))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(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, 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)) <= 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(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), 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, cons(x_2_0, x_2_1)) <= _r_1(x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= reverse(x_0_1, x_1_1)
  reverse(nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_jges_0, nil)  ;  _jna -> cons(_kges_0, cons(_xmes_0, cons(_bnes_0, cons(_cnes_0, _cnes_1))))  ;  t1 -> cons(_lges_0, nil)
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


-------------------------------------------
Step 28, which took 2.224243 s (model generation: 2.220267,  model checking: 0.003976):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

Accumulated learning constraints:
{
append(cons(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, cons(z, nil))), cons(z, 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, cons(z, nil))), cons(z, cons(z, 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(s(z), nil), s(z)) <= True
length(cons(z, cons(s(z), nil)), s(s(z))) <= 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
leq(s(s(z)), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, 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)))
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(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
leq(s(z), s(s(z))) <= length(cons(s(z), nil), s(s(z))) /\ reverse(cons(z, nil), cons(s(z), nil))
False <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(z), nil)), cons(z, cons(z, nil)))
leq(s(s(z)), s(s(s(z)))) <= length(cons(z, cons(s(z), nil)), s(s(s(z)))) /\ reverse(cons(z, cons(s(z), nil)), cons(z, cons(z, nil)))
leq(s(s(s(s(z)))), s(s(z))) <= 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)))
leq(s(s(s(s(z)))), s(s(z))) <= length(cons(z, cons(z, cons(z, cons(z, nil)))), s(s(s(s(z))))) /\ reverse(cons(z, cons(z, nil)), cons(z, cons(z, cons(z, cons(z, nil)))))
False <= length(cons(z, cons(z, nil)), s(z))
False <= length(cons(z, nil), s(s(z)))
False <= leq(s(s(s(z))), s(s(z)))
leq(s(z), s(s(z))) <= leq(s(s(z)), s(s(s(z))))
False <= leq(s(s(z)), s(z))
leq(z, s(s(z))) <= leq(s(z), s(s(s(z))))
leq(z, s(z)) <= leq(s(z), s(s(z)))
False <= leq(s(z), z)
leq(s(z), s(s(z))) <= leq(z, s(z))
False <= reverse(cons(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, 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(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) /\ append(x_0_1, x_1_1, x_2_1) /\ reverse(x_1_1, x_2_1)
  append(cons(x_0_0, x_0_1), 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(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)) <= _r_1(x_1_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append(nil, nil, nil) <= True
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ reverse(x_0_1, x_1_1)
  reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ reverse(x_0_1, x_1_1)
  reverse(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  reverse(nil, nil) <= True
}
]


;
length ->
[
length : <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
}
]


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


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



--
Equality automata are defined for: {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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_poes_0, cons(_odfs_0, _odfs_1))  ;  _jna -> cons(_qoes_0, cons(_pdfs_0, cons(_qdfs_0, _qdfs_1)))  ;  t1 -> nil
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
Yes: {
_una -> cons(_oyes_0, cons(_hzes_0, nil))  ;  _vna -> s(s(z))  ;  _wna -> z  ;  l1 -> nil
}

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

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

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

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


-------------------------------------------
Step 29, which took 5.716660 s (model generation: 5.716124,  model checking: 0.000536):

Clauses:
{
append(nil, l2, l2) <= True -> 0
length(nil, z) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina) -> 0
append(cons(h1, t1), l2, cons(h1, _dna)) <= append(t1, l2, _dna) -> 0
leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna) -> 0
leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una) -> 0
length(cons(x, ll), s(_nna)) <= length(ll, _nna) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
}

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


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


;
reverse ->
[
reverse : <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), _jna) <= append(_ina, cons(h1, nil), _jna) /\ reverse(t1, _ina)  :
Yes: {
_ina -> cons(_sdfs_0, cons(_hffs_0, nil))  ;  _jna -> cons(_tdfs_0, cons(_iffs_0, cons(_sffs_0, cons(_vffs_0, _vffs_1))))  ;  t1 -> cons(_udfs_0, cons(_jffs_0, nil))
}

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

leq(_rna, _tna) <= length(_sna, _tna) /\ length(l1, _rna) /\ reverse(l1, _sna)  :
No: ()

leq(_vna, _wna) <= length(_una, _vna) /\ length(l1, _wna) /\ reverse(l1, _una)  :
No: ()

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

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

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

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


Total time: 32.644907
Learner time: 18.232686
Teacher time: 0.019894
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)) <= _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
  _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_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_3(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
}
]


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


;
reverse ->
[
reverse : <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}
_|