Solving ../../benchmarks/smtlib/true/drop_length_minus.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:
{
(drop_elt, F:
{
drop_elt(s(u), enil, enil) <= True
drop_elt(z, l, l) <= True
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)
}
eq_elist(_yta, _zta) <= drop_elt(_wta, _xta, _yta) /\ drop_elt(_wta, _xta, _zta)
)
(length_elt, F:
{
length_elt(enil, z) <= True
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua)
}
eq_nat(_cua, _dua) <= length_elt(_bua, _cua) /\ length_elt(_bua, _dua)
)
(minus, F:
{
minus(s(u), z, s(u)) <= True
minus(z, y, z) <= True
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)
}
eq_nat(_hua, _iua) <= minus(_fua, _gua, _hua) /\ minus(_fua, _gua, _iua)
)
}

properties:
{
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)
}


over-approximation: {drop_elt, length_elt, minus}
under-approximation: {}

Clause system for inference is:

{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}


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

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), enil)
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, econs(a, enil))), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), econs(a, econs(a, enil)))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
minus(s(s(z)), s(s(s(s(z)))), z) <= minus(s(z), s(s(s(z))), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_6(x_0_1)
  _r_3(s(x_0_0)) <= True
  _r_4(z) <= True
  _r_5(enil) <= True
  _r_6(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_5(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1)
  drop_elt(z, 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
}
]


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



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006918 s (model generation: 0.006832,  model checking: 0.000086):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  
}
]


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


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
Yes: {

}

drop_elt(z, l, l) <= True  :
Yes: {
l -> enil
}

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

}

minus(s(u), z, s(u)) <= True  :
Yes: {

}

minus(z, y, z) <= True  :
Yes: {
y -> z
}

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
No: ()

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 1, which took 0.008611 s (model generation: 0.008520,  model checking: 0.000091):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(z), enil, enil) <= True
drop_elt(z, enil, enil) <= True
length_elt(enil, z) <= True
minus(s(z), z, s(z)) <= True
minus(z, z, z) <= True
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, enil, enil) <= True
}
]


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


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
Yes: {
l -> econs(_lhde_0, _lhde_1)
}

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
Yes: {
y -> s(_mhde_0)
}

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
No: ()

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> enil  ;  u -> z  ;  x3 -> enil
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> z  ;  u -> z  ;  x2 -> z
}


-------------------------------------------
Step 2, which took 0.017145 s (model generation: 0.017027,  model checking: 0.000118):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= True
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_bide_0, _bide_1)  ;  _kua -> s(z)  ;  _lua -> s(_dide_0)  ;  _mua -> s(s(_side_0))  ;  l -> econs(_fide_0, _fide_1)  ;  n -> z
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> econs(_hide_0, _hide_1)  ;  u -> z  ;  x3 -> econs(_jide_0, _jide_1)
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(_kide_0)  ;  u -> s(_lide_0)  ;  x2 -> z
}


-------------------------------------------
Step 3, which took 0.021262 s (model generation: 0.021117,  model checking: 0.000145):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= True
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
Yes: {
u -> s(_rjde_0)
}

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(_hjde_0)  ;  _mua -> s(_ijde_0)  ;  l -> econs(_jjde_0, _jjde_1)  ;  n -> s(_kjde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 4, which took 0.033444 s (model generation: 0.033224,  model checking: 0.000220):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= True
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_yjde_0, _yjde_1)  ;  _kua -> s(_zjde_0)  ;  _lua -> s(_akde_0)  ;  _mua -> z  ;  l -> econs(_ckde_0, _ckde_1)  ;  n -> s(_dkde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 5, which took 0.057766 s (model generation: 0.057529,  model checking: 0.000237):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= True
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(_pmde_0))  ;  _mua -> s(z)  ;  l -> econs(_vlde_0, _vlde_1)  ;  n -> s(_wlde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(s(_smde_0))  ;  u -> s(s(_rmde_0))  ;  x2 -> z
}


-------------------------------------------
Step 6, which took 0.083767 s (model generation: 0.083436,  model checking: 0.000331):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= True
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(z))  ;  _mua -> s(z)  ;  l -> econs(_jnde_0, econs(_zode_0, enil))  ;  n -> s(_knde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 7, which took 0.076221 s (model generation: 0.075804,  model checking: 0.000417):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_gpde_0, _gpde_1)  ;  _kua -> s(z)  ;  _lua -> s(z)  ;  _mua -> z  ;  l -> econs(_kpde_0, econs(_arde_0, _arde_1))  ;  n -> s(_lpde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua)  :
Yes: {
_aua -> s(z)  ;  ll -> econs(_lqde_0, _lqde_1)
}

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 8, which took 0.181164 s (model generation: 0.180606,  model checking: 0.000558):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), 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 <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_3(econs(x_0_0, x_0_1)) <= True
  _r_4(enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_hrde_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(z))  ;  _mua -> z  ;  l -> econs(_lrde_0, econs(_ltde_0, enil))  ;  n -> s(_mrde_0)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> enil  ;  u -> s(_jsde_0)  ;  x3 -> econs(_ksde_0, enil)
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 9, which took 0.202101 s (model generation: 0.201656,  model checking: 0.000445):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), 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 <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_3(z, econs(x_1_0, x_1_1)) <= True
  _r_4(s(x_0_0), econs(x_1_0, x_1_1)) <= True
  _r_4(z, enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_otde_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(z))  ;  _mua -> s(s(_gwde_0))  ;  l -> econs(_stde_0, econs(_jwde_0, enil))  ;  n -> s(z)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> enil  ;  u -> s(_wude_0)  ;  x3 -> enil
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> z  ;  u -> z  ;  x2 -> s(_qvde_0)
}


-------------------------------------------
Step 10, which took 0.219210 s (model generation: 0.218377,  model checking: 0.000833):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), 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 <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_1(s(x_0_0), econs(x_1_0, x_1_1)) <= True
  _r_1(s(x_0_0), enil) <= True
  _r_1(z, enil) <= True
  _r_2(z, econs(x_1_0, x_1_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_1(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_uxde_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(z))  ;  _mua -> s(s(_tbee_0))  ;  l -> econs(_yxde_0, econs(_jbee_0, enil))  ;  n -> z
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> econs(_ayde_0, _ayde_1)  ;  u -> s(z)  ;  x3 -> econs(_cyde_0, econs(_dbee_0, _dbee_1))
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> z  ;  u -> s(z)  ;  x2 -> s(_tzde_0)
}


-------------------------------------------
Step 11, which took 0.330562 s (model generation: 0.329543,  model checking: 0.001019):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(s(x_0_0)) <= True
  _r_3(econs(x_0_0, x_0_1)) <= True
  _r_4(enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_2(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
Yes: {
l -> econs(_acee_0, econs(_nhee_0, _nhee_1))
}

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(z))  ;  _mua -> s(z)  ;  l -> econs(_jdee_0, econs(_ciee_0, enil))  ;  n -> s(s(_shee_0))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(s(z))  ;  u -> s(z)  ;  x2 -> s(_hfee_0)
}


-------------------------------------------
Step 12, which took 0.414359 s (model generation: 0.412970,  model checking: 0.001389):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(s(x_0_0)) <= True
  _r_3(enil) <= True
  _r_4(econs(x_0_0, x_0_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_2(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_ziee_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(z))  ;  _mua -> z  ;  l -> econs(_djee_0, econs(_qoee_0, enil))  ;  n -> s(s(_ioee_0))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 13, which took 0.388685 s (model generation: 0.386449,  model checking: 0.002236):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_1(s(x_0_0)) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_2(z) <= True
  _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
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_0) /\ _r_4(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_1(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(z)  ;  _mua -> s(s(_zdfe_0))  ;  l -> econs(_ksee_0, enil)  ;  n -> s(s(_ydfe_0))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(z)  ;  u -> s(s(_zdfe_0))  ;  x2 -> s(z)
}


-------------------------------------------
Step 14, which took 0.432513 s (model generation: 0.425573,  model checking: 0.006940):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_1(s(x_0_0)) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_2(z) <= True
  _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
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_0) /\ _r_4(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_1(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(z))  ;  _mua -> s(z)  ;  l -> econs(_rife_0, econs(_ymge_0, enil))  ;  n -> s(s(s(_olge_0)))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 15, which took 0.441883 s (model generation: 0.436560,  model checking: 0.005323):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _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
  _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
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_0) /\ _r_3(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_4(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_1(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_1)
  drop_elt(z, 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
}
]


;
minus ->
[
minus : <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
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_1_0) /\ _r_1(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_0_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(z)  ;  _mua -> s(z)  ;  l -> econs(_tqge_0, enil)  ;  n -> s(s(z))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> enil  ;  u -> s(s(z))  ;  x3 -> econs(_vuge_0, enil)
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> z  ;  u -> s(z)  ;  x2 -> s(s(z))
}


-------------------------------------------
Step 16, which took 1.282197 s (model generation: 1.280104,  model checking: 0.002093):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1)
  _r_2(z, econs(x_1_0, x_1_1)) <= True
  _r_3(s(x_0_0), econs(x_1_0, x_1_1)) <= True
  _r_3(s(x_0_0), enil) <= True
  _r_3(z, enil) <= True
  _r_4(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_4(enil, enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1, x_2_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_mwhe_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(s(z)))  ;  _mua -> z  ;  l -> econs(_qwhe_0, econs(_reie_0, econs(_xeie_0, enil)))  ;  n -> s(s(z))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 17, which took 1.598417 s (model generation: 1.595868,  model checking: 0.002549):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, econs(a, enil)), econs(a, enil))
False <= length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ minus(s(s(s(z))), s(s(z)), z)
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  _r_4(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_4(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_5(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_2(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
Yes: {
u -> s(s(_nuie_0))
}

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_wgie_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(z)  ;  _mua -> z  ;  l -> econs(_ahie_0, enil)  ;  n -> s(s(_muie_0))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
Yes: {
_vta -> econs(_ikie_0, _ikie_1)  ;  u -> s(s(_fwie_0))  ;  x3 -> econs(_kkie_0, enil)
}

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(s(_wvie_0))  ;  u -> s(s(z))  ;  x2 -> s(s(_awie_0))
}


-------------------------------------------
Step 18, which took 1.741877 s (model generation: 1.738553,  model checking: 0.003324):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, econs(a, enil)), econs(a, enil))
False <= length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) /\ minus(s(s(s(z))), s(s(z)), z)
False <= length_elt(econs(a, econs(a, enil)), s(z))
False <= length_elt(econs(a, enil), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1)
  _r_2(z, econs(x_1_0, x_1_1)) <= True
  _r_3(s(x_0_0)) <= True
  _r_4(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1)
  drop_elt(z, enil, enil) <= True
}
]


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


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
Yes: {
l -> econs(_gwie_0, econs(_eoje_0, econs(_koje_0, _koje_1)))
}

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(z))  ;  _mua -> s(s(_toje_0))  ;  l -> econs(_fcje_0, econs(_hpje_0, enil))  ;  n -> s(s(s(_voje_0)))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 19, which took 10.840602 s (model generation: 10.839909,  model checking: 0.000693):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_4(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_4(x_0_0, x_1_1)
  _r_4(z, econs(x_1_0, x_1_1)) <= True
  _r_5(s(x_0_0), econs(x_1_0, x_1_1)) <= True
  _r_5(s(x_0_0), enil) <= True
  _r_5(z, enil) <= True
  _r_6(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_6(enil, enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_5(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_6(x_1_1, x_2_1)
  drop_elt(z, 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
}
]


;
minus ->
[
minus : <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)) <= _r_2(x_0_0, x_1_0)
  _r_2(s(x_0_0), z) <= True
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(z, s(x_1_0)) <= True
  _r_3(z, z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> enil  ;  _kua -> z  ;  _lua -> s(s(s(z)))  ;  _mua -> s(z)  ;  l -> econs(_crje_0, econs(_otje_0, econs(_euje_0, enil)))  ;  n -> s(s(z))
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> s(s(s(z)))  ;  u -> s(s(z))  ;  x2 -> z
}


-------------------------------------------
Step 20, which took 15.642623 s (model generation: 15.641834,  model checking: 0.000789):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), enil)
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_3(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_1)
  _r_3(z, econs(x_1_0, x_1_1)) <= True
  _r_4(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_4(x_0_0, x_1_1)
  _r_4(s(x_0_0), enil) <= True
  _r_4(z, enil) <= True
  _r_5(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_5(enil, enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_4(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1, x_2_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_xvje_0, econs(_ozje_0, enil))  ;  _kua -> s(s(z))  ;  _lua -> s(s(z))  ;  _mua -> s(z)  ;  l -> econs(_bwje_0, econs(_nzje_0, enil))  ;  n -> z
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
No: ()


-------------------------------------------
Step 21, which took 8.685658 s (model generation: 8.684561,  model checking: 0.001097):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), enil)
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_1(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  _r_1(z, econs(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), econs(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1)
  _r_2(s(x_0_0), enil) <= True
  _r_2(z, enil) <= True
  _r_3(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_3(enil, enil) <= True
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_2(x_0_0, x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
Yes: {
u -> s(s(s(_sgke_0)))
}

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_xake_0, enil)  ;  _kua -> s(z)  ;  _lua -> s(s(s(z)))  ;  _mua -> s(s(_mhke_0))  ;  l -> econs(_bbke_0, econs(_yhke_0, econs(_kike_0, enil)))  ;  n -> s(z)
}

drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta)  :
No: ()

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

minus(s(u), s(x2), _eua) <= minus(u, x2, _eua)  :
Yes: {
_eua -> z  ;  u -> s(z)  ;  x2 -> s(s(s(_sgke_0)))
}


-------------------------------------------
Step 22, which took 17.127740 s (model generation: 17.124912,  model checking: 0.002828):

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), enil)
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, econs(a, enil))), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
minus(s(s(z)), s(s(s(s(z)))), z) <= minus(s(z), s(s(s(z))), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_6(x_0_1)
  _r_3(s(x_0_0)) <= True
  _r_4(z) <= True
  _r_5(enil) <= True
  _r_6(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_5(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1)
  drop_elt(z, 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
}
]


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



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




Answer of teacher:

drop_elt(s(u), enil, enil) <= True  :
No: ()

drop_elt(z, l, l) <= True  :
No: ()

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

minus(s(u), z, s(u)) <= True  :
No: ()

minus(z, y, z) <= True  :
No: ()

eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua)  :
Yes: {
_jua -> econs(_lkke_0, econs(_fale_0, enil))  ;  _kua -> s(s(z))  ;  _lua -> s(s(z))  ;  _mua -> s(z)  ;  l -> econs(_pkke_0, econs(_lale_0, enil))  ;  n -> s(z)
}

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


Total time: 60.849093
Learner time: 59.800964
Teacher time: 0.033761
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
drop_elt(s(u), enil, enil) <= True -> 0
drop_elt(z, l, l) <= True -> 0
length_elt(enil, z) <= True -> 0
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_kua, _mua) <= drop_elt(n, l, _jua) /\ length_elt(_jua, _kua) /\ length_elt(l, _lua) /\ minus(_lua, n, _mua) -> 0
drop_elt(s(u), econs(x2, x3), _vta) <= drop_elt(u, x3, _vta) -> 0
length_elt(econs(x, ll), s(_aua)) <= length_elt(ll, _aua) -> 0
minus(s(u), s(x2), _eua) <= minus(u, x2, _eua) -> 0
}

Accumulated learning constraints:
{
drop_elt(s(s(s(z))), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), econs(a, enil)) <= True
drop_elt(s(s(z)), econs(a, econs(a, enil)), enil) <= True
drop_elt(s(s(z)), econs(a, enil), enil) <= True
drop_elt(s(z), econs(a, econs(a, enil)), econs(a, enil)) <= True
drop_elt(s(z), econs(a, enil), enil) <= True
drop_elt(s(z), enil, enil) <= True
drop_elt(z, econs(a, econs(a, econs(a, enil))), econs(a, econs(a, econs(a, enil)))) <= True
drop_elt(z, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True
drop_elt(z, econs(a, enil), econs(a, enil)) <= True
drop_elt(z, enil, enil) <= True
length_elt(econs(a, econs(a, econs(a, enil))), s(s(s(z)))) <= 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
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(z)), s(z)) <= True
minus(s(s(s(z))), s(z), s(s(z))) <= True
minus(s(s(s(z))), z, s(s(s(z)))) <= True
minus(s(s(z)), s(s(s(z))), z) <= True
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(s(z))) <= True
minus(s(z), s(s(z)), z) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= drop_elt(s(s(z)), econs(a, econs(a, econs(a, enil))), enil)
False <= drop_elt(s(s(z)), econs(a, econs(a, enil)), econs(a, enil))
False <= drop_elt(s(s(z)), econs(a, enil), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, econs(a, enil))), econs(a, enil))
False <= drop_elt(s(z), econs(a, econs(a, enil)), econs(a, econs(a, enil)))
False <= drop_elt(s(z), econs(a, econs(a, enil)), enil)
False <= drop_elt(s(z), econs(a, enil), econs(a, enil))
False <= drop_elt(z, econs(a, 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 <= minus(s(s(s(z))), s(s(z)), z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(z))) <= minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
minus(s(s(z)), s(s(s(s(z)))), z) <= minus(s(z), s(s(s(z))), z)
False <= minus(s(z), s(s(z)), s(s(z)))
False <= minus(s(z), s(s(z)), s(z))
minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z)))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

drop_elt ->
[
drop_elt : <nat * elist * elist>
{
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_6(x_0_1)
  _r_3(s(x_0_0)) <= True
  _r_4(z) <= True
  _r_5(enil) <= True
  _r_6(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_3(x_0_0) /\ _r_6(x_1_1)
  drop_elt(s(x_0_0), econs(x_1_0, x_1_1), enil) <= _r_5(x_1_1)
  drop_elt(s(x_0_0), enil, enil) <= True
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1)
  drop_elt(z, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1)
  drop_elt(z, 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
}
]


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



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