Solving ../../benchmarks/smtlib/true/length_append_to_plus.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: {
elist -> {econs, enil}  ;  elt -> {a, b}  ;  nat -> {s, z}
}
definition:
{
(append_elt, F:
{
append_elt(enil, l2, l2) <= True
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)
}
eq_elist(_pca, _qca) <= append_elt(_nca, _oca, _pca) /\ append_elt(_nca, _oca, _qca)
)
(length_elt, F:
{
length_elt(enil, z) <= True
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)
}
eq_nat(_tca, _uca) <= length_elt(_sca, _tca) /\ length_elt(_sca, _uca)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)
}
eq_nat(_yca, _zca) <= plus(_wca, _xca, _yca) /\ plus(_wca, _xca, _zca)
)
}

properties:
{
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)
}


over-approximation: {append_elt, length_elt, plus}
under-approximation: {}

Clause system for inference is:

{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}


Solving took 60.765363 seconds.
Maybe:  timeout during learnerLast solver state:

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, econs(a, enil))), enil, econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(s(z)), s(s(s(z))))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_4(econs(x_0_0, x_0_1)) <= True
  _r_5(enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_0_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007236 s (model generation: 0.007158,  model checking: 0.000078):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
Yes: {
l2 -> enil
}

length_elt(enil, z) <= True  :
Yes: {

}

plus(n, z, n) <= True  :
Yes: {
n -> z
}

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
No: ()

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.009738 s (model generation: 0.009655,  model checking: 0.000083):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(enil, enil, enil) <= True
length_elt(enil, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  append_elt(enil, enil, enil) <= True
}
]


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


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
Yes: {
l2 -> econs(_yybq_0, _yybq_1)
}

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
Yes: {
n -> s(_zybq_0)
}

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
No: ()

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> enil  ;  l2 -> enil  ;  t1 -> enil
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
Yes: {
_rca -> z  ;  ll -> enil
}

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> z  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 2, which took 0.012798 s (model generation: 0.012565,  model checking: 0.000233):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_pzbq_0, _pzbq_1)  ;  _bda -> s(z)  ;  _cda -> z  ;  _dda -> s(_szbq_0)  ;  _eda -> s(s(_hacq_0))  ;  l1 -> enil  ;  l2 -> econs(_vzbq_0, _vzbq_1)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_wzbq_0, _wzbq_1)  ;  l2 -> econs(_xzbq_0, _xzbq_1)  ;  t1 -> enil
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(_zzbq_0)  ;  mm -> z  ;  n -> s(_bacq_0)
}


-------------------------------------------
Step 3, which took 0.029150 s (model generation: 0.028951,  model checking: 0.000199):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_pacq_0, _pacq_1)  ;  _bda -> s(z)  ;  _cda -> s(_racq_0)  ;  _dda -> z  ;  _eda -> s(s(_obcq_0))  ;  l1 -> econs(_uacq_0, _uacq_1)  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(z)  ;  mm -> s(_ebcq_0)  ;  n -> z
}


-------------------------------------------
Step 4, which took 0.019299 s (model generation: 0.019109,  model checking: 0.000190):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_rbcq_0, _rbcq_1)  ;  _bda -> s(z)  ;  _cda -> s(_tbcq_0)  ;  _dda -> s(_ubcq_0)  ;  _eda -> s(s(_xccq_0))  ;  l1 -> econs(_wbcq_0, _wbcq_1)  ;  l2 -> econs(_xbcq_0, _xbcq_1)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 5, which took 0.035783 s (model generation: 0.035529,  model checking: 0.000254):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_2(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_zccq_0, econs(_gecq_0, _gecq_1))  ;  _bda -> s(z)  ;  _cda -> s(_bdcq_0)  ;  _dda -> s(_cdcq_0)  ;  _eda -> s(s(_mecq_0))  ;  l1 -> econs(_edcq_0, _edcq_1)  ;  l2 -> econs(_fdcq_0, _fdcq_1)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 6, which took 0.035122 s (model generation: 0.034858,  model checking: 0.000264):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_2(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_oecq_0, econs(_ggcq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(z)  ;  _dda -> s(z)  ;  _eda -> s(z)  ;  l1 -> econs(_tecq_0, enil)  ;  l2 -> econs(_uecq_0, enil)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 7, which took 0.068042 s (model generation: 0.067810,  model checking: 0.000232):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= length_elt(econs(a, econs(a, enil)), s(s(z))) /\ plus(s(z), s(z), s(z))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  _r_2(enil) <= True
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_ygcq_0, enil)  ;  _bda -> s(s(_licq_0))  ;  _cda -> z  ;  _dda -> s(z)  ;  _eda -> s(z)  ;  l1 -> enil  ;  l2 -> econs(_ehcq_0, enil)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
Yes: {
_rca -> s(_lhcq_0)  ;  ll -> econs(_mhcq_0, enil)
}

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


-------------------------------------------
Step 8, which took 0.077528 s (model generation: 0.077172,  model checking: 0.000356):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= True
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_uicq_0, econs(_vkcq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(z)  ;  _dda -> z  ;  _eda -> s(z)  ;  l1 -> econs(_zicq_0, enil)  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(s(_ykcq_0))  ;  mm -> s(z)  ;  n -> s(_ujcq_0)
}


-------------------------------------------
Step 9, which took 0.208659 s (model generation: 0.208296,  model checking: 0.000363):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_olcq_0, econs(_qncq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> z  ;  _dda -> s(z)  ;  _eda -> s(z)  ;  l1 -> enil  ;  l2 -> econs(_ulcq_0, enil)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_bmcq_0, enil)  ;  l2 -> enil  ;  t1 -> econs(_dmcq_0, _dmcq_1)
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(s(_cncq_0))  ;  mm -> z  ;  n -> s(s(_bncq_0))
}


-------------------------------------------
Step 10, which took 0.232905 s (model generation: 0.232504,  model checking: 0.000401):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(z), s(s(s(z)))) <= plus(s(s(z)), z, s(s(z)))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_1(enil, enil) <= True
  _r_2(enil, econs(x_1_0, x_1_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
Yes: {
n -> s(s(_cqcq_0))
}

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_vncq_0, econs(_kqcq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(z)  ;  _dda -> s(z)  ;  _eda -> s(s(s(_wqcq_0)))  ;  l1 -> econs(_aocq_0, enil)  ;  l2 -> econs(_bocq_0, enil)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_xocq_0, econs(_iqcq_0, _iqcq_1))  ;  l2 -> econs(_yocq_0, _yocq_1)  ;  t1 -> econs(_zocq_0, enil)
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 11, which took 0.381383 s (model generation: 0.380774,  model checking: 0.000609):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(enil, econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(enil, enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
Yes: {
n -> s(s(s(_qucq_0)))
}

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_arcq_0, econs(_fvcq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(s(z))  ;  _dda -> s(z)  ;  _eda -> s(z)  ;  l1 -> econs(_frcq_0, econs(_sucq_0, enil))  ;  l2 -> econs(_grcq_0, enil)
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_atcq_0, econs(_uucq_0, _uucq_1))  ;  l2 -> econs(_btcq_0, econs(_tucq_0, _tucq_1))  ;  t1 -> enil
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(z)  ;  mm -> s(s(_qucq_0))  ;  n -> z
}


-------------------------------------------
Step 12, which took 0.655117 s (model generation: 0.654276,  model checking: 0.000841):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  _r_4(enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_3(x_0_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(z) <= True
  _r_2(s(x_0_0)) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ plus(x_0_0, x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0)
  plus(z, z, s(x_2_0)) <= _r_1(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
Yes: {
l2 -> econs(_mvcq_0, econs(_tbdq_0, _tbdq_1))
}

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> enil  ;  _bda -> z  ;  _cda -> z  ;  _dda -> z  ;  _eda -> s(z)  ;  l1 -> enil  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(z)  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 13, which took 0.642199 s (model generation: 0.641450,  model checking: 0.000749):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(enil, econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(enil, enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= _r_3(x_0_0)
  _r_4(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_4(x_1_0) /\ _r_4(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_icdq_0, econs(_vhdq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(z)  ;  _dda -> s(s(z))  ;  _eda -> s(z)  ;  l1 -> econs(_ncdq_0, enil)  ;  l2 -> econs(_ocdq_0, econs(_vgdq_0, enil))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(z)
}


-------------------------------------------
Step 14, which took 0.711764 s (model generation: 0.710539,  model checking: 0.001225):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(enil, econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(enil, enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= _r_3(x_0_0)
  _r_4(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_4(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_2_0) /\ _r_4(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_4(x_1_0) /\ _r_4(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_cjdq_0, econs(_zodq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(s(z))  ;  _dda -> z  ;  _eda -> s(z)  ;  l1 -> econs(_hjdq_0, econs(_yodq_0, enil))  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_nkdq_0, econs(_kpdq_0, enil))  ;  l2 -> econs(_okdq_0, econs(_jpdq_0, econs(_updq_0, enil)))  ;  t1 -> enil
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 15, which took 0.968308 s (model generation: 0.966447,  model checking: 0.001861):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_1(enil, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  _r_1(enil, enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_yrdq_0, econs(_wbeq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(s(z))  ;  _dda -> s(s(z))  ;  _eda -> s(z)  ;  l1 -> econs(_dsdq_0, econs(_ybeq_0, enil))  ;  l2 -> econs(_esdq_0, econs(_zbeq_0, enil))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 16, which took 1.002371 s (model generation: 0.999728,  model checking: 0.002643):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_3(enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_0_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_1_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_0_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0)) <= _r_2(x_0_0)
  _r_1(z) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_1(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_qgeq_0, enil)  ;  _bda -> s(z)  ;  _cda -> s(s(z))  ;  _dda -> s(s(z))  ;  _eda -> s(s(_zveq_0))  ;  l1 -> econs(_vgeq_0, econs(_oueq_0, enil))  ;  l2 -> econs(_wgeq_0, econs(_queq_0, enil))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_kpeq_0, enil)  ;  l2 -> econs(_lpeq_0, econs(_cweq_0, enil))  ;  t1 -> enil
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 17, which took 1.321649 s (model generation: 1.317228,  model checking: 0.004421):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_1(enil, econs(x_1_0, x_1_1)) <= _r_4(x_1_1)
  _r_1(enil, enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_sweq_0, econs(_ikfq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(s(z))  ;  _dda -> s(s(s(z)))  ;  _eda -> s(z)  ;  l1 -> econs(_xweq_0, econs(_pmfq_0, enil))  ;  l2 -> econs(_yweq_0, econs(_qmfq_0, econs(_lmfq_0, enil)))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
}


-------------------------------------------
Step 18, which took 1.399433 s (model generation: 1.396495,  model checking: 0.002938):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_0_1) /\ _r_4(x_1_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_3(x_0_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_4(x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0)) <= _r_2(x_0_0)
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_2(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_1(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_gqfq_0, econs(_ohgq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> s(s(s(z)))  ;  _dda -> z  ;  _eda -> s(z)  ;  l1 -> econs(_lqfq_0, econs(_wggq_0, econs(_cggq_0, enil)))  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
Yes: {
_mca -> econs(_rufq_0, enil)  ;  l2 -> econs(_sufq_0, econs(_tfgq_0, _tfgq_1))  ;  t1 -> econs(_tufq_0, enil)
}

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca)  :
Yes: {
_vca -> s(z)  ;  mm -> s(z)  ;  n -> s(s(z))
}


-------------------------------------------
Step 19, which took 1.675374 s (model generation: 1.673883,  model checking: 0.001491):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, econs(a, enil))), enil, econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(enil, econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_1)
  _r_2(enil, enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_3(z) <= True
  _r_4(s(x_0_0)) <= _r_3(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_4(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_2_0) /\ _r_4(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_4(x_0_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) /\ _r_4(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_4(x_1_0) /\ _r_4(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_qigq_0, enil)  ;  _bda -> s(z)  ;  _cda -> s(z)  ;  _dda -> z  ;  _eda -> s(s(s(z)))  ;  l1 -> econs(_vigq_0, enil)  ;  l2 -> enil
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 20, which took 39.112346 s (model generation: 39.111748,  model checking: 0.000598):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, econs(a, enil))), enil, econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_3(enil, enil) <= True
  _r_4(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_4(enil, econs(x_1_0, x_1_1)) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_0_1, x_2_1) /\ _r_4(x_1_1, x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_3(x_0_1, x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_mrgq_0, econs(_htgq_0, enil))  ;  _bda -> s(s(z))  ;  _cda -> z  ;  _dda -> s(s(z))  ;  _eda -> s(s(s(_xtgq_0)))  ;  l1 -> enil  ;  l2 -> econs(_srgq_0, econs(_gtgq_0, enil))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


-------------------------------------------
Step 21, which took 11.142325 s (model generation: 11.141664,  model checking: 0.000661):

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, econs(a, enil))), enil, econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(s(z)), s(s(s(z))))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_4(econs(x_0_0, x_0_1)) <= True
  _r_5(enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_0_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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




Answer of teacher:

append_elt(enil, l2, l2) <= True  :
No: ()

length_elt(enil, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda)  :
Yes: {
_ada -> econs(_jvgq_0, enil)  ;  _bda -> s(z)  ;  _cda -> z  ;  _dda -> s(s(z))  ;  _eda -> s(s(z))  ;  l1 -> enil  ;  l2 -> econs(_pvgq_0, econs(_oxgq_0, enil))
}

append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca)  :
No: ()

length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca)  :
No: ()

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


Total time: 60.765363
Learner time: 59.727839
Teacher time: 0.020690
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
append_elt(enil, l2, l2) <= True -> 0
length_elt(enil, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_bda, _eda) <= append_elt(l1, l2, _ada) /\ length_elt(_ada, _bda) /\ length_elt(l1, _cda) /\ length_elt(l2, _dda) /\ plus(_cda, _dda, _eda) -> 0
append_elt(econs(h1, t1), l2, econs(h1, _mca)) <= append_elt(t1, l2, _mca) -> 0
length_elt(econs(x, ll), s(_rca)) <= length_elt(ll, _rca) -> 0
plus(n, s(mm), s(_vca)) <= plus(n, mm, _vca) -> 0
}

Accumulated learning constraints:
{
append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, econs(a, enil)), enil, econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil)))) <= True
append_elt(econs(a, enil), econs(a, enil), econs(a, econs(a, enil))) <= True
append_elt(econs(a, enil), enil, econs(a, enil)) <= True
append_elt(enil, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
append_elt(enil, econs(a, enil), econs(a, enil)) <= True
append_elt(enil, enil, enil) <= True
length_elt(econs(a, econs(a, enil)), s(s(z))) <= True
length_elt(econs(a, enil), s(z)) <= True
length_elt(enil, z) <= True
plus(s(s(s(z))), z, s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(s(z)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= append_elt(econs(a, econs(a, econs(a, enil))), enil, econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil))) /\ length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ plus(s(s(z)), s(s(s(z))), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(s(z)), s(z))
False <= append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, enil)) /\ plus(s(s(z)), s(s(z)), s(s(z)))
False <= append_elt(econs(a, econs(a, enil)), econs(a, enil), econs(a, econs(a, enil))) /\ plus(s(s(z)), s(z), s(z))
False <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, econs(a, enil))) /\ plus(s(z), s(s(z)), s(z))
append_elt(econs(a, econs(a, enil)), econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= append_elt(econs(a, enil), econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(econs(a, enil), econs(a, enil), econs(a, enil))
False <= append_elt(econs(a, enil), enil, econs(a, econs(a, enil)))
append_elt(econs(a, enil), econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= append_elt(enil, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, enil)))
False <= append_elt(enil, econs(a, econs(a, enil)), econs(a, enil))
False <= append_elt(enil, econs(a, enil), econs(a, econs(a, enil)))
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(s(z)))) <= plus(s(s(z)), s(z), s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
plus(s(z), s(s(s(z))), s(s(s(z)))) <= plus(s(z), s(s(z)), s(s(z)))
False <= plus(s(z), s(z), s(s(s(z))))
False <= plus(s(z), s(z), s(z))
False <= plus(s(z), z, s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
False <= plus(z, s(s(z)), s(s(s(z))))
plus(z, s(s(s(z))), s(s(z))) <= plus(z, s(s(z)), s(z))
False <= plus(z, s(z), s(s(z)))
False <= plus(z, z, s(z))
}

Current best model:
|_
name: None

append_elt ->
[
append_elt : <elist * elist * elist>
{
  _r_4(econs(x_0_0, x_0_1)) <= True
  _r_5(enil) <= True
  append_elt(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_4(x_0_1)
  append_elt(econs(x_0_0, x_0_1), enil, econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  append_elt(enil, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  append_elt(enil, enil, enil) <= True
}
]


;
length_elt ->
[
length_elt : <elist * nat>
{
  length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0)
  length_elt(enil, z) <= True
}
]


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



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