Solving ../../benchmarks/smtlib/true/nat_double_is_zero_ite.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(_st))) <= double(nn, _st)
}
eq_nat(_ut, _vt) <= double(_tt, _ut) /\ double(_tt, _vt)
)
(is_zero, P:
{
eq_nat(_wt, z) <= double(n, _wt) /\ 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(_wt, z) <= double(n, _wt) /\ is_zero(n) -> 0
double(s(nn), s(s(_st))) <= double(nn, _st) -> 0
}


Solving took 0.020786 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.005921 s (model generation: 0.005882,  model checking: 0.000039):

Clauses:
{
double(z, z) <= True -> 0
is_zero(z) <= True -> 0
eq_nat(_wt, z) <= double(n, _wt) /\ is_zero(n) -> 0
double(s(nn), s(s(_st))) <= double(nn, _st) -> 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(_wt, z) <= double(n, _wt) /\ is_zero(n)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.006683 s (model generation: 0.006631,  model checking: 0.000052):

Clauses:
{
double(z, z) <= True -> 0
is_zero(z) <= True -> 0
eq_nat(_wt, z) <= double(n, _wt) /\ is_zero(n) -> 0
double(s(nn), s(s(_st))) <= double(nn, _st) -> 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(_wt, z) <= double(n, _wt) /\ is_zero(n)  :
No: ()

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


Total time: 0.020786
Learner time: 0.012513
Teacher time: 0.000091
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}
_|