Solving ../../benchmarks/smtlib/false/member_cons.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)
}
)
(not_null, P:
{
not_null(cons(x, ll)) <= True
False <= not_null(nil)
}
)
}

properties:
{
memberl(i1, l) <= memberl(i1, cons(i2, l))
}


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

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(i1, l) <= memberl(i1, cons(i2, l)) -> 0
}


Solving took 0.047230 seconds.
No: Contradictory set of ground constraints:
{
memberl(s(z), cons(s(z), nil)) <= True
memberl(z, cons(z, nil)) <= True
memberl(z, nil) <= True
memberl(s(z), nil) <= memberl(s(z), cons(z, nil))
False <= memberl(z, nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006255 s (model generation: 0.006199,  model checking: 0.000056):

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(i1, l) <= memberl(i1, cons(i2, l)) -> 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(i1, l) <= memberl(i1, cons(i2, l))  :
No: ()


-------------------------------------------
Step 1, which took 0.006456 s (model generation: 0.006402,  model checking: 0.000054):

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(i1, l) <= memberl(i1, cons(i2, l)) -> 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(_sbpqw_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(_ubpqw_0)  ;  t1 -> nil
}

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

memberl(i1, l) <= memberl(i1, cons(i2, l))  :
Yes: {
i1 -> z  ;  l -> nil
}


-------------------------------------------
Step 2, which took 0.006540 s (model generation: 0.006480,  model checking: 0.000060):

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(i1, l) <= memberl(i1, cons(i2, l)) -> 0
}

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

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(_bcpqw_0)  ;  h1 -> z  ;  t1 -> nil
}

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

memberl(i1, l) <= memberl(i1, cons(i2, l))  :
Yes: {
i1 -> s(_fcpqw_0)  ;  l -> nil
}


Total time: 0.047230
Learner time: 0.019081
Teacher time: 0.000170
Reasons for stopping: No: Contradictory set of ground constraints:
{
memberl(s(z), cons(s(z), nil)) <= True
memberl(z, cons(z, nil)) <= True
memberl(z, nil) <= True
memberl(s(z), nil) <= memberl(s(z), cons(z, nil))
False <= memberl(z, nil)
}