Solving ../../benchmarks/smtlib/false/nat_double_is_le.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(_geb))) <= double(nn, _geb)
}
eq_nat(_ieb, _jeb) <= double(_heb, _ieb) /\ double(_heb, _jeb)
)
(le, P:
{
le(z, s(nn2)) <= True
le(s(nn1), s(nn2)) <= le(nn1, nn2)
le(nn1, nn2) <= le(s(nn1), s(nn2))
False <= le(s(nn1), z)
False <= le(z, z)
}
)
}

properties:
{
le(n, _keb) <= double(n, _keb)
}


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

Clause system for inference is:

{
double(z, z) <= True -> 0
le(n, _keb) <= double(n, _keb) -> 0
double(s(nn), s(s(_geb))) <= double(nn, _geb) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
}


Solving took 0.039918 seconds.
No: Contradictory set of ground constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
le(z, z) <= True
le(s(z), s(z)) <= double(s(z), s(z))
False <= le(z, z)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005980 s (model generation: 0.005932,  model checking: 0.000048):

Clauses:
{
double(z, z) <= True -> 0
le(n, _keb) <= double(n, _keb) -> 0
double(s(nn), s(s(_geb))) <= double(nn, _geb) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
le ->
[
le : <nat * nat>
{
  
}
]



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




Answer of teacher:

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

}

le(n, _keb) <= double(n, _keb)  :
No: ()

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

le(s(nn1), s(nn2)) <= le(nn1, nn2)  :
No: ()

le(nn1, nn2) <= le(s(nn1), s(nn2))  :
No: ()

False <= le(s(nn1), z)  :
No: ()

False <= le(z, z)  :
No: ()


-------------------------------------------
Step 1, which took 0.006261 s (model generation: 0.006209,  model checking: 0.000052):

Clauses:
{
double(z, z) <= True -> 0
le(n, _keb) <= double(n, _keb) -> 0
double(s(nn), s(s(_geb))) <= double(nn, _geb) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
}

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

Current best model:
|_
name: None

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


;
le ->
[
le : <nat * nat>
{
  
}
]



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




Answer of teacher:

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

le(n, _keb) <= double(n, _keb)  :
Yes: {
_keb -> z  ;  n -> z
}

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

le(s(nn1), s(nn2)) <= le(nn1, nn2)  :
No: ()

le(nn1, nn2) <= le(s(nn1), s(nn2))  :
No: ()

False <= le(s(nn1), z)  :
No: ()

False <= le(z, z)  :
No: ()


-------------------------------------------
Step 2, which took 0.007211 s (model generation: 0.007134,  model checking: 0.000077):

Clauses:
{
double(z, z) <= True -> 0
le(n, _keb) <= double(n, _keb) -> 0
double(s(nn), s(s(_geb))) <= double(nn, _geb) -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
False <= le(s(nn1), z) -> 0
False <= le(z, z) -> 0
}

Accumulated learning constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
le(z, 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
}
]


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



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




Answer of teacher:

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

le(n, _keb) <= double(n, _keb)  :
Yes: {
_keb -> s(_pdpqw_0)  ;  n -> s(_qdpqw_0)
}

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

le(s(nn1), s(nn2)) <= le(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

le(nn1, nn2) <= le(s(nn1), s(nn2))  :
No: ()

False <= le(s(nn1), z)  :
No: ()

False <= le(z, z)  :
Yes: {

}


Total time: 0.039918
Learner time: 0.019275
Teacher time: 0.000177
Reasons for stopping: No: Contradictory set of ground constraints:
{
double(s(z), s(s(z))) <= True
double(z, z) <= True
le(z, z) <= True
le(s(z), s(z)) <= double(s(z), s(z))
False <= le(z, z)
}