Solving ../../benchmarks/smtlib/true/isaplanner_prop13.smt2...

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



Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(drop, F:
{
drop(s(u), nil, nil) <= True
drop(z, l, l) <= True
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)
}
eq_eltlist(_vy, _wy) <= drop(_ty, _uy, _vy) /\ drop(_ty, _uy, _wy)
)
}

properties:
{
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)
}


over-approximation: {drop}
under-approximation: {}

Clause system for inference is:

{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}


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

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(s(z))), cons(b, cons(a, cons(a, nil))), cons(b, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, cons(a, nil)))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(a, nil), cons(b, nil))
drop(s(s(z)), cons(a, cons(b, cons(a, cons(a, nil)))), cons(b, cons(a, nil))) <= drop(s(z), cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil)))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
drop(s(z), cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= drop(z, cons(b, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(z, nil) <= True
  _r_2(cons(x_0_0, x_0_1), a) <= True
  _r_2(cons(x_0_0, x_0_1), b) <= _r_5(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(nil) <= True
  _r_5(b) <= True
  _r_6(a) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_1_1, x_2_0) /\ _r_4(x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_2_0) /\ _r_6(x_1_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0)
  drop(z, nil, nil) <= True
}
]



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006319 s (model generation: 0.006273,  model checking: 0.000046):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
Yes: {

}

drop(z, l, l) <= True  :
Yes: {
l -> nil
}

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
No: ()

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
No: ()


-------------------------------------------
Step 1, which took 0.006997 s (model generation: 0.006938,  model checking: 0.000059):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(z), nil, nil) <= True
drop(z, nil, nil) <= True
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  drop(s(x_0_0), nil, nil) <= True
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

drop(z, l, l) <= True  :
Yes: {
l -> cons(_bqoe_0, _bqoe_1)
}

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
No: ()

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> nil  ;  u -> z  ;  x3 -> nil
}


-------------------------------------------
Step 2, which took 0.010104 s (model generation: 0.009894,  model checking: 0.000210):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> nil  ;  _yy -> cons(_jqoe_0, _jqoe_1)  ;  l1 -> cons(_kqoe_0, _kqoe_1)  ;  n -> z
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(_mqoe_0, _mqoe_1)  ;  u -> z  ;  x3 -> cons(_oqoe_0, _oqoe_1)
}


-------------------------------------------
Step 3, which took 0.014028 s (model generation: 0.013893,  model checking: 0.000135):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(z), cons(a, cons(a, nil)), nil)
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(nil) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(_vroe_0, _vroe_1)  ;  _yy -> nil  ;  l1 -> nil  ;  n -> z
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> nil  ;  u -> s(_asoe_0)  ;  x3 -> cons(_bsoe_0, nil)
}


-------------------------------------------
Step 4, which took 0.028140 s (model generation: 0.027906,  model checking: 0.000234):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(z, cons(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_2(z, nil) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, _dtoe_1)  ;  _yy -> cons(a, _etoe_1)  ;  l1 -> cons(_ftoe_0, _ftoe_1)  ;  n -> z
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> nil  ;  u -> s(_duoe_0)  ;  x3 -> nil
}


-------------------------------------------
Step 5, which took 0.029124 s (model generation: 0.028926,  model checking: 0.000198):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(s(x_0_0), nil) <= True
  _r_1(z, nil) <= True
  _r_2(cons(x_0_0, x_0_1), a) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(a, nil)  ;  _yy -> cons(_lvoe_0, cons(_uwoe_0, _uwoe_1))  ;  l1 -> cons(_mvoe_0, _mvoe_1)  ;  n -> z
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(b, _fwoe_1)  ;  u -> z  ;  x3 -> cons(_hwoe_0, _hwoe_1)
}


-------------------------------------------
Step 6, which took 0.103902 s (model generation: 0.103643,  model checking: 0.000259):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(s(x_0_0), nil) <= True
  _r_1(z, nil) <= True
  _r_2(nil, a) <= True
  _r_3(cons(x_0_0, x_0_1), a) <= True
  _r_4(nil) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_2_1)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

drop(z, l, l) <= True  :
Yes: {
l -> cons(b, nil)
}

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(a, _jxoe_1)  ;  _yy -> nil  ;  l1 -> cons(_lxoe_0, nil)  ;  n -> s(z)
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
No: ()


-------------------------------------------
Step 7, which took 0.115080 s (model generation: 0.114623,  model checking: 0.000457):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(s(x_0_0), nil) <= True
  _r_1(z, nil) <= True
  _r_2(z, cons(x_1_0, x_1_1)) <= True
  _r_3(a, a) <= True
  _r_3(b, b) <= True
  _r_4(nil) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1) /\ _r_3(x_1_0, x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ _r_4(x_2_1)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

drop(z, l, l) <= True  :
Yes: {
l -> cons(_vzoe_0, cons(_bcpe_0, _bcpe_1))
}

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, cons(_cdpe_0, _cdpe_1))  ;  _yy -> cons(b, nil)  ;  l1 -> cons(b, _wape_1)  ;  n -> z  ;  x -> b
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(b, nil)  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(b, _xbpe_1)
}


-------------------------------------------
Step 8, which took 0.489553 s (model generation: 0.488885,  model checking: 0.000668):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(z, nil) <= True
  _r_2(cons(x_0_0, x_0_1), a) <= True
  _r_2(cons(x_0_0, x_0_1), b) <= _r_5(x_0_0)
  _r_3(a, a) <= True
  _r_3(b, b) <= True
  _r_4(nil) <= True
  _r_5(b) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_1_1, x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_0, x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ _r_4(x_2_1)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

drop(z, l, l) <= True  :
Yes: {
l -> cons(b, cons(a, _dhpe_1))
}

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(a, cons(_chpe_0, _chpe_1))  ;  _yy -> nil  ;  l1 -> cons(_depe_0, nil)  ;  n -> s(_eepe_0)
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(b, nil)  ;  u -> s(z)  ;  x3 -> cons(a, cons(b, _xhpe_1))
}


-------------------------------------------
Step 9, which took 1.280792 s (model generation: 1.280120,  model checking: 0.000672):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1), b) <= True
  _r_1(z, cons(x_1_0, x_1_1), a) <= True
  _r_1(z, cons(x_1_0, x_1_1), b) <= _r_5(x_1_0)
  _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), nil) <= True
  _r_2(z, nil) <= True
  _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_3(nil, nil) <= True
  _r_4(a, a) <= True
  _r_4(b, b) <= True
  _r_5(b) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1, x_2_0) /\ _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1, x_2_0) /\ _r_2(x_0_0, x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, _qjpe_1)  ;  _yy -> nil  ;  l1 -> cons(_sjpe_0, nil)  ;  n -> s(z)
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(a, nil)  ;  u -> s(z)  ;  x3 -> cons(_nlpe_0, cons(_dnpe_0, _dnpe_1))
}


-------------------------------------------
Step 10, which took 1.757645 s (model generation: 1.754459,  model checking: 0.003186):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  _r_1(s(x_0_0), nil) <= True
  _r_1(z, cons(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), nil) <= True
  _r_2(z, nil) <= True
  _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_3(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0)
  _r_3(nil, nil) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_5(x_1_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_2_1) /\ _r_3(x_1_1, x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_2_1) /\ _r_5(x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1) /\ _r_4(x_1_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1) /\ _r_5(x_2_0)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, cons(_piqe_0, _piqe_1))  ;  _yy -> cons(a, nil)  ;  l1 -> cons(_ntpe_0, nil)  ;  n -> z  ;  x -> a
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(b, cons(_fjqe_0, _fjqe_1))  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, cons(_gjqe_0, _gjqe_1))
}


-------------------------------------------
Step 11, which took 30.477921 s (model generation: 30.476311,  model checking: 0.001610):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, cons(a, nil)))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_1_1)
  _r_1(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1)
  _r_1(z, cons(x_1_0, x_1_1), nil) <= True
  _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_2(s(x_0_0), nil) <= True
  _r_2(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0)
  _r_2(z, nil) <= True
  _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_3(nil, nil) <= True
  _r_4(a, a) <= True
  _r_4(b, b) <= True
  _r_5(cons(x_0_0, x_0_1)) <= True
  _r_6(b) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1, x_2_1) /\ _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1, x_2_1) /\ _r_2(x_0_0, x_1_1) /\ _r_3(x_1_1, x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0, x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, nil)  ;  _yy -> nil  ;  l1 -> cons(_inqe_0, cons(_vvqe_0, _vvqe_1))  ;  n -> s(s(_uvqe_0))  ;  x -> b
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(b, cons(_ruqe_0, _ruqe_1))  ;  u -> s(z)  ;  x3 -> cons(b, cons(_quqe_0, cons(_nvqe_0, _nvqe_1)))
}


-------------------------------------------
Step 12, which took 16.214675 s (model generation: 16.211134,  model checking: 0.003541):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(s(z))), cons(b, cons(a, cons(a, nil))), cons(b, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, cons(a, nil)))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
drop(s(s(z)), cons(a, cons(b, cons(a, cons(a, nil)))), cons(b, cons(a, nil))) <= drop(s(z), cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil)))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(z, nil) <= True
  _r_2(cons(x_0_0, x_0_1), a) <= True
  _r_2(cons(x_0_0, x_0_1), b) <= _r_5(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(nil) <= True
  _r_5(b) <= True
  _r_6(a) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_1_1, x_2_0) /\ _r_4(x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_2_0) /\ _r_6(x_1_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0)
  drop(z, nil, nil) <= True
}
]



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




Answer of teacher:

drop(s(u), nil, nil) <= True  :
No: ()

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

eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy)  :
Yes: {
_xy -> cons(b, _kfre_1)  ;  _yy -> nil  ;  l1 -> nil  ;  n -> z  ;  x -> a
}

drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy)  :
Yes: {
_sy -> cons(_orre_0, cons(_asre_0, nil))  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, nil)
}


Total time: 59.681147
Learner time: 50.523005
Teacher time: 0.011275
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
eq_eltlist(_xy, _yy) <= drop(n, l1, _yy) /\ drop(s(n), cons(x, l1), _xy) -> 0
drop(s(u), cons(x2, x3), _sy) <= drop(u, x3, _sy) -> 0
}

Accumulated learning constraints:
{
drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True
drop(s(s(z)), cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True
drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True
drop(s(s(z)), cons(a, nil), nil) <= True
drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True
drop(s(z), cons(a, cons(b, nil)), cons(b, nil)) <= True
drop(s(z), cons(a, nil), nil) <= True
drop(s(z), cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True
drop(s(z), nil, nil) <= True
drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True
drop(z, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(s(s(s(z))), cons(b, cons(a, cons(a, nil))), cons(b, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, cons(a, nil)))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil))
False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, cons(a, nil)))
False <= drop(s(z), cons(a, cons(a, nil)), cons(b, nil))
False <= drop(s(z), cons(a, cons(a, nil)), nil)
False <= drop(s(z), cons(a, nil), cons(a, nil))
False <= drop(s(z), cons(a, nil), cons(b, nil))
drop(s(s(z)), cons(a, cons(b, cons(a, cons(a, nil)))), cons(b, cons(a, nil))) <= drop(s(z), cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil)))
False <= drop(s(z), cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(a, cons(a, nil)))
False <= drop(z, cons(a, nil), cons(b, nil))
drop(s(z), cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= drop(z, cons(b, nil), cons(a, cons(a, nil)))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  _r_1(z, nil) <= True
  _r_2(cons(x_0_0, x_0_1), a) <= True
  _r_2(cons(x_0_0, x_0_1), b) <= _r_5(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(nil) <= True
  _r_5(b) <= True
  _r_6(a) <= True
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_1_1, x_2_0) /\ _r_4(x_2_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_2_0) /\ _r_6(x_1_0)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1)
  drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1)
  drop(s(x_0_0), nil, nil) <= True
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0)
  drop(z, nil, nil) <= True
}
]



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