Solving ../../benchmarks/smtlib/true/tree_height_node_leq.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)
}
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa)
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa)
}
eq_nat(_ab, _bb) <= height(_za, _ab) /\ height(_za, _bb)
)
}

properties:
{
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb)
}


over-approximation: {height}
under-approximation: {}

Clause system for inference is:

{
height(leaf, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa) -> 0
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa) -> 0
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}


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

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


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



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

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa) -> 0
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa) -> 0
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

}

leq_nat(z, n2) <= True  :
Yes: {
n2 -> z
}

height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa)  :
No: ()

height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa)  :
No: ()

leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb)  :
No: ()

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

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

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


-------------------------------------------
Step 1, which took 0.006368 s (model generation: 0.006290,  model checking: 0.000078):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa) -> 0
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa) -> 0
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

leq_nat(z, n2) <= True  :
Yes: {
n2 -> s(_nxyaw_0)
}

height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa)  :
No: ()

height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa)  :
Yes: {
_va -> z  ;  _wa -> z  ;  _xa -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb)  :
No: ()

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

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

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


-------------------------------------------
Step 2, which took 0.008320 s (model generation: 0.008239,  model checking: 0.000081):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa) -> 0
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa) -> 0
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa)  :
No: ()

height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa)  :
No: ()

leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb)  :
No: ()

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

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

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


-------------------------------------------
Step 3, which took 0.009842 s (model generation: 0.009782,  model checking: 0.000060):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa) -> 0
height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa) -> 0
leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

leq_nat(z, n2) <= True  :
No: ()

height(node(e, t1, t2), s(_ya)) \/ leq_nat(_va, _wa) <= height(t1, _va) /\ height(t1, _ya) /\ height(t2, _wa)  :
No: ()

height(node(e, t1, t2), s(_xa)) <= height(t1, _va) /\ height(t2, _wa) /\ height(t2, _xa) /\ leq_nat(_va, _wa)  :
No: ()

leq_nat(s(z), _cb) <= height(node(e, t1, t2), _cb)  :
No: ()

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

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

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

}


Total time: 0.042901
Learner time: 0.031204
Teacher time: 0.000293
Reasons for stopping: Yes: |_
name: None

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


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



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