Solving ../../benchmarks/smtlib/true/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), _uua) <= drop(u, x3, _uua)
}
eq_eltlist(_xua, _yua) <= drop(_vua, _wua, _xua) /\ drop(_vua, _wua, _yua)
)
}

properties:
{
eq_eltlist(_zua, xs) <= drop(z, xs, _zua)
}


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), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 0
}


Solving took 0.164176 seconds.
Yes: |_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_0, x_1_0)
  _r_1(nil, nil) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= 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) <= 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)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_0, x_2_0)
  drop(z, nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007625 s (model generation: 0.007582,  model checking: 0.000043):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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), _uua) <= drop(u, x3, _uua)  :
No: ()

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
No: ()


-------------------------------------------
Step 1, which took 0.006594 s (model generation: 0.006514,  model checking: 0.000080):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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(_hloe_0, _hloe_1)
}

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

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
No: ()


-------------------------------------------
Step 2, which took 0.008038 s (model generation: 0.007967,  model checking: 0.000071):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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: ()

drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua)  :
Yes: {
_uua -> cons(_oloe_0, _oloe_1)  ;  u -> z  ;  x3 -> cons(_qloe_0, _qloe_1)
}

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
Yes: {
_zua -> cons(b, _rloe_1)  ;  xs -> cons(a, _sloe_1)
}


-------------------------------------------
Step 3, which took 0.014501 s (model generation: 0.014205,  model checking: 0.000296):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(a) <= 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) <= 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)) <= _r_1(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  :
Yes: {
l -> cons(b, _zloe_1)
}

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

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
Yes: {
_zua -> cons(a, nil)  ;  xs -> cons(_dmoe_0, cons(_nmoe_0, _nmoe_1))
}


-------------------------------------------
Step 4, which took 0.026826 s (model generation: 0.026700,  model checking: 0.000126):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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, cons(b, nil), cons(b, nil)) <= True
drop(z, nil, nil) <= True
False <= drop(z, cons(a, cons(a, nil)), cons(a, nil))
False <= drop(z, cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(nil, a) <= True
  _r_2(b) <= 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) <= 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)) <= _r_1(x_1_1, x_2_0)
  drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(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  :
Yes: {
l -> cons(a, cons(_xmoe_0, _xmoe_1))
}

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

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
Yes: {
_zua -> cons(_vmoe_0, nil)  ;  xs -> cons(b, cons(_hnoe_0, _hnoe_1))
}


-------------------------------------------
Step 5, which took 0.032094 s (model generation: 0.031936,  model checking: 0.000158):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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, 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(z, cons(a, cons(a, nil)), cons(a, nil))
False <= drop(z, cons(a, nil), cons(b, nil))
False <= drop(z, cons(b, cons(a, nil)), cons(a, nil))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(nil, nil) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= 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) <= 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)) <= _r_1(x_1_1, x_2_1) /\ _r_2(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: ()

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

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
Yes: {
_zua -> cons(b, cons(b, _xnoe_1))  ;  xs -> cons(b, cons(a, _wnoe_1))
}


-------------------------------------------
Step 6, which took 0.033509 s (model generation: 0.033346,  model checking: 0.000163):

Clauses:
{
drop(s(u), nil, nil) <= True -> 0
drop(z, l, l) <= True -> 0
drop(s(u), cons(x2, x3), _uua) <= drop(u, x3, _uua) -> 0
eq_eltlist(_zua, xs) <= drop(z, xs, _zua) -> 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, 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(z, cons(a, cons(a, nil)), cons(a, nil))
False <= drop(z, cons(a, nil), cons(b, nil))
False <= drop(z, cons(b, cons(a, nil)), cons(a, nil))
False <= drop(z, cons(b, cons(a, nil)), cons(b, cons(b, nil)))
}

Current best model:
|_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0)
  _r_1(nil, nil) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= 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) <= 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)) <= _r_1(x_1_1, x_2_1) /\ _r_2(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: ()

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

eq_eltlist(_zua, xs) <= drop(z, xs, _zua)  :
Yes: {
_zua -> cons(b, cons(b, nil))  ;  xs -> cons(b, cons(b, cons(_epoe_0, _epoe_1)))
}


Total time: 0.164176
Learner time: 0.128249
Teacher time: 0.000937
Reasons for stopping: Yes: |_
name: None

drop ->
[
drop : <nat * eltlist * eltlist>
{
  _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_0, x_1_0)
  _r_1(nil, nil) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= 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) <= 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)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_0, x_2_0)
  drop(z, nil, nil) <= True
}
]



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