Solving ../../benchmarks/smtlib/true/nat_double_is_zero.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(_ora))) <= double(nn, _ora)
}
eq_nat(_qra, _rra) <= double(_pra, _qra) /\ double(_pra, _rra)
)
(is_zero, P:
{
eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n)
is_zero(n) <= double(n, z)
}
)
}

properties:
{
is_zero(z) <= True
}


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

Clause system for inference is:

{
double(z, z) <= True -> 0
is_zero(z) <= True -> 0
eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n) -> 0
double(s(nn), s(s(_ora))) <= double(nn, _ora) -> 0
}


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

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


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



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

Clauses:
{
double(z, z) <= True -> 0
is_zero(z) <= True -> 0
eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n) -> 0
double(s(nn), s(s(_ora))) <= double(nn, _ora) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

}

is_zero(z) <= True  :
Yes: {

}

eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006387 s (model generation: 0.006339,  model checking: 0.000048):

Clauses:
{
double(z, z) <= True -> 0
is_zero(z) <= True -> 0
eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n) -> 0
double(s(nn), s(s(_ora))) <= double(nn, _ora) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

is_zero(z) <= True  :
No: ()

eq_nat(_sra, z) <= double(n, _sra) /\ is_zero(n)  :
No: ()

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


Total time: 0.020337
Learner time: 0.013093
Teacher time: 0.000094
Reasons for stopping: Yes: |_
name: None

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


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



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