Solving ../../benchmarks/smtlib/true/member_equal_nat.smt2...

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



Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(memberl, P:
{
memberl(h1, cons(h1, t1)) <= True
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))
False <= memberl(e, nil)
}
)
}

properties:
{
memberl(i, l2) <= memberl(i, l2)
}


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

Clause system for inference is:

{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}


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

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

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



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005842 s (model generation: 0.005806,  model checking: 0.000036):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> z
}

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
No: ()

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 1, which took 0.005913 s (model generation: 0.005871,  model checking: 0.000042):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

Accumulated learning constraints:
{
memberl(z, cons(z, nil)) <= True
}

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  memberl(z, cons(x_1_0, x_1_1)) <= True
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> s(_joey_0)
}

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> z  ;  h1 -> s(_loey_0)  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 2, which took 0.008621 s (model generation: 0.008572,  model checking: 0.000049):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(_qoey_0)  ;  h1 -> z  ;  t1 -> nil
}

False <= memberl(e, nil)  :
Yes: {
e -> z
}

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 3, which took 0.022171 s (model generation: 0.021971,  model checking: 0.000200):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= True
  memberl(s(x_0_0), nil) <= True
  memberl(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> z  ;  h1 -> s(_woey_0)  ;  t1 -> cons(z, _xoey_1)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
No: ()

False <= memberl(e, nil)  :
Yes: {
e -> s(_epey_0)
}

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 4, which took 0.029960 s (model generation: 0.029586,  model checking: 0.000374):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(_opey_0)  ;  h1 -> z  ;  t1 -> cons(s(_crey_0), _qpey_1)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(_irey_0))  ;  h1 -> s(z)  ;  t1 -> cons(z, _zpey_1)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 5, which took 0.031474 s (model generation: 0.030803,  model checking: 0.000671):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(_tuey_0))  ;  h1 -> z  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 6, which took 0.036358 s (model generation: 0.035517,  model checking: 0.000841):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(z, s(x_1_0)) <= True
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> s(s(_kyey_0))  ;  t1 -> nil
}

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(_lzey_0))  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(_oyey_0, _oyey_1))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(z)  ;  h1 -> s(s(_wyey_0))  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 7, which took 0.064766 s (model generation: 0.063923,  model checking: 0.000843):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(z) <= True
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
  memberl(s(x_0_0), nil) <= _r_3(x_0_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> s(s(s(_kdfy_0)))  ;  t1 -> nil
}

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(s(_fdfy_0)))  ;  h1 -> s(z)  ;  t1 -> nil
}

False <= memberl(e, nil)  :
Yes: {
e -> s(s(z))
}

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 8, which took 0.079360 s (model generation: 0.078487,  model checking: 0.000873):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= _r_3(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(s(z)), _mffy_1)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> z  ;  h1 -> s(_khfy_0)  ;  t1 -> cons(s(_ojfy_0), nil)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 9, which took 0.209835 s (model generation: 0.208070,  model checking: 0.001765):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= _r_4(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_4(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= memberl(x_0_0, x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> z  ;  h1 -> s(_dlfy_0)  ;  t1 -> cons(s(_oofy_0), cons(z, _apfy_1))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, nil)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 10, which took 0.546986 s (model generation: 0.546028,  model checking: 0.000958):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= _r_4(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, cons(s(_kagy_0), _jzfy_1))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(_jcgy_0)), cons(z, _zagy_1))
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 11, which took 0.736292 s (model generation: 0.732606,  model checking: 0.003686):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= _r_4(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_5(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
No: ()

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(z), nil)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 12, which took 0.920639 s (model generation: 0.896800,  model checking: 0.023839):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= _r_4(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_4(s(x_0_0)) <= _r_5(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_5(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_5(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(z), cons(s(z), nil))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> z  ;  h1 -> s(s(_fziy_0))  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 13, which took 1.057356 s (model generation: 1.015290,  model checking: 0.042066):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_3(s(x_0_0)) <= _r_5(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_5(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_0)
  memberl(s(x_0_0), nil) <= _r_3(x_0_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> s(s(s(s(_lkoy_0))))  ;  t1 -> nil
}

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(s(s(_lkoy_0))))  ;  h1 -> z  ;  t1 -> cons(s(z), cons(s(z), _vjoy_1))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> z  ;  h1 -> s(_trny_0)  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
}

False <= memberl(e, nil)  :
Yes: {
e -> s(s(s(z)))
}

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 14, which took 2.256828 s (model generation: 2.100082,  model checking: 0.156746):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0)
  _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_3(s(x_0_0)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_5(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(z))  ;  h1 -> s(z)  ;  t1 -> cons(s(s(z)), nil)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), nil)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 15, which took 7.198321 s (model generation: 6.725670,  model checking: 0.472651):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _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_6(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_6(x_1_0)
  _r_2(nil) <= True
  _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1)
  _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1)
  _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_5(s(x_0_0)) <= True
  _r_6(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ memberl(x_0_0, x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> s(_hwyy_0)  ;  t1 -> cons(z, nil)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(z))  ;  h1 -> s(z)  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 16, which took 6.067369 s (model generation: 6.018637,  model checking: 0.048732):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_6(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1)
  _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= _r_5(x_0_0)
  _r_5(s(x_0_0)) <= _r_6(x_0_0)
  _r_6(z) <= True
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_6(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_6(x_0_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, cons(z, cons(s(z), _hbyz_1)))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(z))  ;  h1 -> s(s(s(s(z))))  ;  t1 -> cons(z, nil)
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 17, which took 10.240808 s (model generation: 10.208941,  model checking: 0.031867):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

memberl ->
[
memberl : <nat * natlist>
{
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_5(x_1_0)
  _r_1(s(x_0_0), nil) <= _r_5(x_0_0)
  _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1)
  _r_1(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0)
  _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_3(cons(x_0_0, x_0_1)) <= True
  _r_4(s(x_0_0)) <= _r_5(x_0_0)
  _r_4(z) <= True
  _r_5(s(x_0_0)) <= _r_6(x_0_0)
  _r_6(s(x_0_0)) <= _r_4(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0)
  memberl(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_6(x_0_0)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  memberl(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(s(s(z))))  ;  h1 -> z  ;  t1 -> cons(z, nil)
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(s(z)))  ;  h1 -> z  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


-------------------------------------------
Step 18, which took 9.813103 s (model generation: 9.724446,  model checking: 0.088657):

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

memberl(h1, cons(h1, t1)) <= True  :
No: ()

eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1)  :
Yes: {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(s(s(z))), cons(z, nil))
}

eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1))  :
Yes: {
e -> s(s(z))  ;  h1 -> s(s(s(z)))  ;  t1 -> nil
}

False <= memberl(e, nil)  :
No: ()

memberl(i, l2) <= memberl(i, l2)  :
No: ()


Total time: 59.524760
Learner time: 38.457106
Teacher time: 0.874896
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
memberl(h1, cons(h1, t1)) <= True -> 0
eq_nat(e, h1) \/ memberl(e, cons(h1, t1)) <= memberl(e, t1) -> 0
eq_nat(e, h1) \/ memberl(e, t1) <= memberl(e, cons(h1, t1)) -> 0
False <= memberl(e, nil) -> 0
memberl(i, l2) <= memberl(i, l2) -> 0
}

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

Current best model:
|_
name: None

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



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