Solving ../../benchmarks/smtlib/true/tree_heightRB_node_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: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(le_nat, P:
{
le_nat(z, s(nn2)) <= True
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))
False <= le_nat(s(nn1), z)
False <= le_nat(z, z)
}
)
(height_rb, F:
{
height_rb(leaf, z) <= True
height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma)
}
eq_nat(_zma, _ana) <= height_rb(_yma, _ana) /\ height_rb(_yma, _zma)
)
}

properties:
{
eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna)
}


over-approximation: {height_rb, le_nat, leq_nat}
under-approximation: {le_nat, leq_nat}

Clause system for inference is:

{
height_rb(leaf, z) <= True -> 0
eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna) -> 0
height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}


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

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height_rb(x_0_2, x_1_0)
}
]


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


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



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

Clauses:
{
height_rb(leaf, z) <= True -> 0
eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna) -> 0
height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  
}
]


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


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



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




Answer of teacher:

height_rb(leaf, z) <= True  :
Yes: {

}

eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna)  :
No: ()

height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma)  :
No: ()

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

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

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

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


-------------------------------------------
Step 1, which took 0.006178 s (model generation: 0.006127,  model checking: 0.000051):

Clauses:
{
height_rb(leaf, z) <= True -> 0
eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna) -> 0
height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

height_rb(leaf, z) <= True  :
No: ()

eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna)  :
No: ()

height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma)  :
Yes: {
_xma -> z  ;  t2 -> leaf
}

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

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

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

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


-------------------------------------------
Step 2, which took 0.009452 s (model generation: 0.009330,  model checking: 0.000122):

Clauses:
{
height_rb(leaf, z) <= True -> 0
eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna) -> 0
height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
}

Accumulated learning constraints:
{
height_rb(leaf, z) <= True
height_rb(node(a, leaf, leaf), s(z)) <= True
}

Current best model:
|_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


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


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



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




Answer of teacher:

height_rb(leaf, z) <= True  :
No: ()

eq_nat(_bna, s(_cna)) <= height_rb(t2, _cna) /\ height_rb(node(e, t1, t2), _bna)  :
Yes: {
_bna -> s(z)  ;  _cna -> s(_nclhp_0)  ;  t2 -> node(_oclhp_0, _oclhp_1, _oclhp_2)
}

height_rb(node(e, t1, t2), s(_xma)) <= height_rb(t2, _xma)  :
No: ()

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

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

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

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


Total time: 0.032943
Learner time: 0.021487
Teacher time: 0.000219
Reasons for stopping: Yes: |_
name: None

height_rb ->
[
height_rb : <etree * nat>
{
  height_rb(leaf, z) <= True
  height_rb(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height_rb(x_0_2, x_1_0)
}
]


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


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



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