Solving ../../benchmarks/smtlib/true/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(_ex))) <= double(nn, _ex)
}
eq_nat(_gx, _hx) <= double(_fx, _gx) /\ double(_fx, _hx)
)
(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, _ix) <= double(n, _ix) /\ le(z, n)
}


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

Clause system for inference is:

{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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.042769 seconds.
Yes: |_
name: None

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


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



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

Clauses:
{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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(z, s(nn2)) <= True  :
Yes: {

}

le(n, _ix) <= double(n, _ix) /\ le(z, n)  :
No: ()

double(s(nn), s(s(_ex))) <= double(nn, _ex)  :
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.006793 s (model generation: 0.006726,  model checking: 0.000067):

Clauses:
{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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
le(z, s(z)) <= True
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

le(z, s(nn2)) <= True  :
No: ()

le(n, _ix) <= double(n, _ix) /\ le(z, n)  :
No: ()

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

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

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.006972 s (model generation: 0.006907,  model checking: 0.000065):

Clauses:
{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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(s(z), s(s(z))) <= True
le(z, s(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(s(x_0_0), s(x_1_0)) <= True
  le(z, s(x_1_0)) <= True
}
]



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




Answer of teacher:

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

le(z, s(nn2)) <= True  :
No: ()

le(n, _ix) <= double(n, _ix) /\ le(z, n)  :
No: ()

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

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

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

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

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


-------------------------------------------
Step 3, which took 0.006649 s (model generation: 0.006603,  model checking: 0.000046):

Clauses:
{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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(s(z), s(s(z))) <= True
le(z, s(z)) <= True
le(z, z) <= le(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
}
]


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



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




Answer of teacher:

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

le(z, s(nn2)) <= True  :
No: ()

le(n, _ix) <= double(n, _ix) /\ le(z, n)  :
No: ()

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

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

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

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

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

}


-------------------------------------------
Step 4, which took 0.008765 s (model generation: 0.008632,  model checking: 0.000133):

Clauses:
{
double(z, z) <= True -> 0
le(z, s(nn2)) <= True -> 0
le(n, _ix) <= double(n, _ix) /\ le(z, n) -> 0
double(s(nn), s(s(_ex))) <= double(nn, _ex) -> 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(s(z), s(s(z))) <= True
le(z, s(z)) <= True
le(s(z), z) <= le(s(s(z)), s(z))
False <= le(s(z), s(z))
False <= le(z, z)
}

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(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0)
  le(s(x_0_0), z) <= True
  le(z, s(x_1_0)) <= True
}
]



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




Answer of teacher:

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

le(z, s(nn2)) <= True  :
No: ()

le(n, _ix) <= double(n, _ix) /\ le(z, n)  :
Yes: {
_ix -> s(z)  ;  n -> s(z)
}

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

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

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

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

}

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


Total time: 0.042769
Learner time: 0.034761
Teacher time: 0.000375
Reasons for stopping: Yes: |_
name: None

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


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



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