Solving ../../benchmarks/smtlib/true/isaplanner_prop16.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:
{
(last, F:
{
last(cons(y, nil), y) <= True
last(nil, z) <= True
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)
}
eq_nat(_xd, _yd) <= last(_wd, _xd) /\ last(_wd, _yd)
)
}

properties:
{
eq_nat(_zd, x) <= last(cons(x, nil), _zd)
}


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

Clause system for inference is:

{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}


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

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



--
Equality automata are defined for: {nat, natlist}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006485 s (model generation: 0.006428,  model checking: 0.000057):

Clauses:
{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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



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




Answer of teacher:

last(cons(y, nil), y) <= True  :
Yes: {
y -> z
}

last(nil, z) <= True  :
Yes: {

}

eq_nat(_zd, x) <= last(cons(x, nil), _zd)  :
No: ()

last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)  :
No: ()


-------------------------------------------
Step 1, which took 0.006744 s (model generation: 0.006696,  model checking: 0.000048):

Clauses:
{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}

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

Current best model:
|_
name: None

last ->
[
last : <natlist * nat>
{
  last(cons(x_0_0, x_0_1), z) <= True
  last(nil, z) <= True
}
]



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




Answer of teacher:

last(cons(y, nil), y) <= True  :
Yes: {
y -> s(_oese_0)
}

last(nil, z) <= True  :
No: ()

eq_nat(_zd, x) <= last(cons(x, nil), _zd)  :
Yes: {
_zd -> z  ;  x -> s(_qese_0)
}

last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)  :
No: ()


-------------------------------------------
Step 2, which took 0.009546 s (model generation: 0.009446,  model checking: 0.000100):

Clauses:
{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

last(cons(y, nil), y) <= True  :
No: ()

last(nil, z) <= True  :
No: ()

eq_nat(_zd, x) <= last(cons(x, nil), _zd)  :
Yes: {
_zd -> s(_uese_0)  ;  x -> z
}

last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)  :
Yes: {
_vd -> z  ;  x2 -> z  ;  y -> s(_zese_0)
}


-------------------------------------------
Step 3, which took 0.021266 s (model generation: 0.021069,  model checking: 0.000197):

Clauses:
{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

last(cons(y, nil), y) <= True  :
No: ()

last(nil, z) <= True  :
No: ()

eq_nat(_zd, x) <= last(cons(x, nil), _zd)  :
Yes: {
_zd -> s(s(_tfse_0))  ;  x -> s(z)
}

last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)  :
Yes: {
_vd -> s(_lfse_0)  ;  x2 -> s(_ofse_0)  ;  y -> z
}


-------------------------------------------
Step 4, which took 0.031853 s (model generation: 0.031377,  model checking: 0.000476):

Clauses:
{
last(cons(y, nil), y) <= True -> 0
last(nil, z) <= True -> 0
eq_nat(_zd, x) <= last(cons(x, nil), _zd) -> 0
last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

last(cons(y, nil), y) <= True  :
Yes: {
y -> s(s(_ogse_0))
}

last(nil, z) <= True  :
No: ()

eq_nat(_zd, x) <= last(cons(x, nil), _zd)  :
Yes: {
_zd -> s(z)  ;  x -> s(s(_chse_0))
}

last(cons(y, cons(x2, x3)), _vd) <= last(cons(x2, x3), _vd)  :
No: ()


Total time: 0.118634
Learner time: 0.075016
Teacher time: 0.000878
Reasons for stopping: Yes: |_
name: None

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



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