Solving ../../benchmarks/smtlib/true/nat_double_is_even.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}
}
definition:
{
(double, F:
{
double(z, z) <= True
double(s(nn), s(s(_tj))) <= double(nn, _tj)
}
eq_nat(_vj, _wj) <= double(_uj, _vj) /\ double(_uj, _wj)
)
(is_even, P:
{
is_even(z) <= True
is_even(s(s(n3))) <= is_even(n3)
is_even(n3) <= is_even(s(s(n3)))
False <= is_even(s(z))
}
)
}

properties:
{
is_even(_xj) <= double(n, _xj)
}


over-approximation: {double}
under-approximation: {is_even}

Clause system for inference is:

{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}


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

double ->
[
double : <nat * nat>
{
  _r_1(s(x_0_0)) <= is_even(x_0_0)
  double(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0)
  double(z, z) <= True
  is_even(s(x_0_0)) <= _r_1(x_0_0)
  is_even(z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  _r_1(s(x_0_0)) <= is_even(x_0_0)
  is_even(s(x_0_0)) <= _r_1(x_0_0)
  is_even(z) <= True
}
]



--
Equality automata are defined for: {nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006759 s (model generation: 0.006718,  model checking: 0.000041):

Clauses:
{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

double ->
[
double : <nat * nat>
{
  
}
]


;
is_even ->
[
is_even : <nat>
{
  
}
]



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




Answer of teacher:

double(z, z) <= True  :
Yes: {

}

is_even(_xj) <= double(n, _xj)  :
No: ()

double(s(nn), s(s(_tj))) <= double(nn, _tj)  :
No: ()

is_even(s(s(n3))) <= is_even(n3)  :
No: ()

is_even(n3) <= is_even(s(s(n3)))  :
No: ()

False <= is_even(s(z))  :
No: ()


-------------------------------------------
Step 1, which took 0.010432 s (model generation: 0.010398,  model checking: 0.000034):

Clauses:
{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}

Accumulated learning constraints:
{
double(z, z) <= True
}

Current best model:
|_
name: None

double ->
[
double : <nat * nat>
{
  double(z, z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  
}
]



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




Answer of teacher:

double(z, z) <= True  :
No: ()

is_even(_xj) <= double(n, _xj)  :
Yes: {
_xj -> z  ;  n -> z
}

double(s(nn), s(s(_tj))) <= double(nn, _tj)  :
Yes: {
_tj -> z  ;  nn -> z
}

is_even(s(s(n3))) <= is_even(n3)  :
No: ()

is_even(n3) <= is_even(s(s(n3)))  :
No: ()

False <= is_even(s(z))  :
No: ()


-------------------------------------------
Step 2, which took 0.015317 s (model generation: 0.015230,  model checking: 0.000087):

Clauses:
{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}

Accumulated learning constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
is_even(z) <= True
}

Current best model:
|_
name: None

double ->
[
double : <nat * nat>
{
  double(s(x_0_0), s(x_1_0)) <= True
  double(z, z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  is_even(z) <= True
}
]



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




Answer of teacher:

double(z, z) <= True  :
No: ()

is_even(_xj) <= double(n, _xj)  :
Yes: {
_xj -> s(_ompaa_0)  ;  n -> s(_pmpaa_0)
}

double(s(nn), s(s(_tj))) <= double(nn, _tj)  :
No: ()

is_even(s(s(n3))) <= is_even(n3)  :
Yes: {
n3 -> z
}

is_even(n3) <= is_even(s(s(n3)))  :
No: ()

False <= is_even(s(z))  :
No: ()


-------------------------------------------
Step 3, which took 0.013844 s (model generation: 0.013774,  model checking: 0.000070):

Clauses:
{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}

Accumulated learning constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
is_even(s(s(z))) <= True
is_even(z) <= True
is_even(s(z)) <= double(s(z), s(z))
}

Current best model:
|_
name: None

double ->
[
double : <nat * nat>
{
  double(s(x_0_0), s(x_1_0)) <= True
  double(z, z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  is_even(s(x_0_0)) <= True
  is_even(z) <= True
}
]



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




Answer of teacher:

double(z, z) <= True  :
No: ()

is_even(_xj) <= double(n, _xj)  :
No: ()

double(s(nn), s(s(_tj))) <= double(nn, _tj)  :
No: ()

is_even(s(s(n3))) <= is_even(n3)  :
No: ()

is_even(n3) <= is_even(s(s(n3)))  :
No: ()

False <= is_even(s(z))  :
Yes: {

}


-------------------------------------------
Step 4, which took 0.016149 s (model generation: 0.015886,  model checking: 0.000263):

Clauses:
{
double(z, z) <= True -> 0
is_even(_xj) <= double(n, _xj) -> 0
double(s(nn), s(s(_tj))) <= double(nn, _tj) -> 0
is_even(s(s(n3))) <= is_even(n3) -> 0
is_even(n3) <= is_even(s(s(n3))) -> 0
False <= is_even(s(z)) -> 0
}

Accumulated learning constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
is_even(s(s(z))) <= True
is_even(z) <= True
False <= double(s(z), s(z))
False <= is_even(s(z))
}

Current best model:
|_
name: None

double ->
[
double : <nat * nat>
{
  _r_1(s(x_0_0)) <= True
  double(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0)
  double(z, z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  _r_1(s(x_0_0)) <= True
  is_even(s(x_0_0)) <= _r_1(x_0_0)
  is_even(z) <= True
}
]



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




Answer of teacher:

double(z, z) <= True  :
No: ()

is_even(_xj) <= double(n, _xj)  :
No: ()

double(s(nn), s(s(_tj))) <= double(nn, _tj)  :
No: ()

is_even(s(s(n3))) <= is_even(n3)  :
No: ()

is_even(n3) <= is_even(s(s(n3)))  :
Yes: {
n3 -> s(z)
}

False <= is_even(s(z))  :
No: ()


Total time: 0.077288
Learner time: 0.062006
Teacher time: 0.000495
Reasons for stopping: Yes: |_
name: None

double ->
[
double : <nat * nat>
{
  _r_1(s(x_0_0)) <= is_even(x_0_0)
  double(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0)
  double(z, z) <= True
  is_even(s(x_0_0)) <= _r_1(x_0_0)
  is_even(z) <= True
}
]


;
is_even ->
[
is_even : <nat>
{
  _r_1(s(x_0_0)) <= is_even(x_0_0)
  is_even(s(x_0_0)) <= _r_1(x_0_0)
  is_even(z) <= True
}
]



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