Solving ../../benchmarks/smtlib/false/timbuk_deleteBUG.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}
}
definition:
{
(delete, F:
{
delete(x, nil, nil) <= True
delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb)
eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb)
}
eq_eltlist(_vhb, _whb) <= delete(_thb, _uhb, _vhb) /\ delete(_thb, _uhb, _whb)
)
(mem, P:
{
mem(h, cons(h, t)) <= True
eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t)
eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t))
False <= mem(e, nil)
}
)
}

properties:
{
mem(i, _xhb) <= delete(i, l, _xhb)
}


over-approximation: {delete}
under-approximation: {mem}

Clause system for inference is:

{
delete(x, nil, nil) <= True -> 0
delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb) -> 0
mem(i, _xhb) <= delete(i, l, _xhb) -> 0
eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb) -> 0
eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0
eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0
False <= mem(e, nil) -> 0
}


Solving took 0.058275 seconds.
No: Contradictory set of ground constraints:
{
delete(a, cons(a, nil), nil) <= True
delete(a, cons(b, nil), cons(b, nil)) <= True
delete(a, nil, nil) <= True
delete(b, cons(a, nil), cons(a, nil)) <= True
delete(b, cons(b, nil), nil) <= True
delete(b, nil, nil) <= True
mem(a, nil) <= True
mem(b, nil) <= True
False <= mem(b, nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005374 s (model generation: 0.005312,  model checking: 0.000062):

Clauses:
{
delete(x, nil, nil) <= True -> 0
delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb) -> 0
mem(i, _xhb) <= delete(i, l, _xhb) -> 0
eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb) -> 0
eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0
eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0
False <= mem(e, nil) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

delete ->
[
delete : <elt * eltlist * eltlist>
{
  
}
]


;
mem ->
[
mem : <elt * eltlist>
{
  
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
Yes: {
x -> b
}

delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb)  :
No: ()

mem(i, _xhb) <= delete(i, l, _xhb)  :
No: ()

eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb)  :
No: ()

eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t)  :
No: ()

eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t))  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006330 s (model generation: 0.006188,  model checking: 0.000142):

Clauses:
{
delete(x, nil, nil) <= True -> 0
delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb) -> 0
mem(i, _xhb) <= delete(i, l, _xhb) -> 0
eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb) -> 0
eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0
eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0
False <= mem(e, nil) -> 0
}

Accumulated learning constraints:
{
delete(b, nil, nil) <= True
}

Current best model:
|_
name: None

delete ->
[
delete : <elt * eltlist * eltlist>
{
  delete(b, nil, nil) <= True
}
]


;
mem ->
[
mem : <elt * eltlist>
{
  
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
Yes: {
x -> a
}

delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb)  :
Yes: {
_rhb -> nil  ;  h -> b  ;  t -> nil
}

mem(i, _xhb) <= delete(i, l, _xhb)  :
Yes: {
_xhb -> nil  ;  i -> b  ;  l -> nil
}

eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb)  :
Yes: {
_shb -> nil  ;  h -> a  ;  t -> nil  ;  x -> b
}

eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t)  :
No: ()

eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t))  :
No: ()

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


-------------------------------------------
Step 2, which took 0.008419 s (model generation: 0.007378,  model checking: 0.001041):

Clauses:
{
delete(x, nil, nil) <= True -> 0
delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb) -> 0
mem(i, _xhb) <= delete(i, l, _xhb) -> 0
eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb) -> 0
eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0
eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0
False <= mem(e, nil) -> 0
}

Accumulated learning constraints:
{
delete(a, nil, nil) <= True
delete(b, cons(a, nil), cons(a, nil)) <= True
delete(b, cons(b, nil), nil) <= True
delete(b, nil, nil) <= True
mem(b, nil) <= True
}

Current best model:
|_
name: None

delete ->
[
delete : <elt * eltlist * eltlist>
{
  delete(a, nil, nil) <= True
  delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  delete(b, cons(x_1_0, x_1_1), nil) <= True
  delete(b, nil, nil) <= True
}
]


;
mem ->
[
mem : <elt * eltlist>
{
  mem(b, nil) <= True
}
]



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




Answer of teacher:

delete(x, nil, nil) <= True  :
No: ()

delete(h, cons(h, t), _rhb) <= delete(h, t, _rhb)  :
Yes: {
_rhb -> nil  ;  h -> a  ;  t -> nil
}

mem(i, _xhb) <= delete(i, l, _xhb)  :
Yes: {
_xhb -> nil  ;  i -> a  ;  l -> nil
}

eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _shb)) <= delete(x, t, _shb)  :
Yes: {
_shb -> nil  ;  h -> b  ;  t -> nil  ;  x -> a
}

eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t)  :
Yes: {
e -> b  ;  h -> a  ;  t -> nil
}

eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t))  :
No: ()

False <= mem(e, nil)  :
Yes: {
e -> b
}


Total time: 0.058275
Learner time: 0.018878
Teacher time: 0.001245
Reasons for stopping: No: Contradictory set of ground constraints:
{
delete(a, cons(a, nil), nil) <= True
delete(a, cons(b, nil), cons(b, nil)) <= True
delete(a, nil, nil) <= True
delete(b, cons(a, nil), cons(a, nil)) <= True
delete(b, cons(b, nil), nil) <= True
delete(b, nil, nil) <= True
mem(a, nil) <= True
mem(b, nil) <= True
False <= mem(b, nil)
}