Solving ../../benchmarks/smtlib/false/isaplanner_prop11.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), _ukb) <= drop(u, x3, _ukb)
}
eq_eltlist(_xkb, _ykb) <= drop(_vkb, _wkb, _xkb) /\ drop(_vkb, _wkb, _ykb)
)
}

properties:
{
False <= drop(z, _zkb, _zkb)
}


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

Clause system for inference is:

{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _ukb) <= drop(u, x3, _ukb) -> 0
False <= drop(z, _zkb, _zkb) -> 0
}


Solving took 0.039451 seconds.
No: Contradictory set of ground constraints:
{
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(z, nil, nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005790 s (model generation: 0.005741,  model checking: 0.000049):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _ukb) <= drop(u, x3, _ukb) -> 0
False <= drop(z, _zkb, _zkb) -> 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
}

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

False <= drop(z, _zkb, _zkb)  :
No: ()


-------------------------------------------
Step 1, which took 0.006814 s (model generation: 0.006755,  model checking: 0.000059):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _ukb) <= drop(u, x3, _ukb) -> 0
False <= drop(z, _zkb, _zkb) -> 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(_tuoqw_0, _tuoqw_1)
}

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

False <= drop(z, _zkb, _zkb)  :
Yes: {
_zkb -> nil
}


Total time: 0.039451
Learner time: 0.012496
Teacher time: 0.000108
Reasons for stopping: No: Contradictory set of ground constraints:
{
drop(s(z), nil, nil) <= True
drop(z, cons(a, nil), cons(a, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(z, nil, nil)
}