Solving ../../benchmarks/smtlib/true/tree_shallower_rec_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}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{
leq(z, n2) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(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)
}
)
(shallower, P:
{
shallower(leaf, n) <= True
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))
shallower(t1, m) <= shallower(node(e, t1, t2), s(m))
False <= shallower(node(e, t1, t2), z)
}
)
}

properties:
{
shallower(t1, n) <= shallower(node(e, t1, t2), s(n))
shallower(t2, n) <= shallower(node(e, t1, t2), s(n))
}


over-approximation: {le, leq}
under-approximation: {le, leq}

Clause system for inference is:

{
shallower(leaf, n) <= True -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, n) <= shallower(node(e, t1, t2), s(n)) -> 0
shallower(t2, n) <= shallower(node(e, t1, t2), s(n)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}


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

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


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


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



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

Clauses:
{
shallower(leaf, n) <= True -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, n) <= shallower(node(e, t1, t2), s(n)) -> 0
shallower(t2, n) <= shallower(node(e, t1, t2), s(n)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


;
shallower ->
[
shallower : <etree * nat>
{
  
}
]



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




Answer of teacher:

shallower(leaf, n) <= True  :
Yes: {
n -> z
}

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

shallower(t2, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 1, which took 0.006649 s (model generation: 0.006565,  model checking: 0.000084):

Clauses:
{
shallower(leaf, n) <= True -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, n) <= shallower(node(e, t1, t2), s(n)) -> 0
shallower(t2, n) <= shallower(node(e, t1, t2), s(n)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

shallower(leaf, n) <= True  :
Yes: {
n -> s(_krxpw_0)
}

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
Yes: {
m -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

shallower(t2, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 2, which took 0.007305 s (model generation: 0.007219,  model checking: 0.000086):

Clauses:
{
shallower(leaf, n) <= True -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, n) <= shallower(node(e, t1, t2), s(n)) -> 0
shallower(t2, n) <= shallower(node(e, t1, t2), s(n)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

shallower(leaf, n) <= True  :
No: ()

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> leaf  ;  t2 -> node(_qrxpw_0, _qrxpw_1, _qrxpw_2)
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> node(_srxpw_0, _srxpw_1, _srxpw_2)
}

shallower(t1, n) <= shallower(node(e, t1, t2), s(n))  :
Yes: {
n -> z  ;  t1 -> node(_urxpw_0, _urxpw_1, _urxpw_2)
}

shallower(t2, n) <= shallower(node(e, t1, t2), s(n))  :
Yes: {
n -> z  ;  t2 -> node(_wrxpw_0, _wrxpw_1, _wrxpw_2)
}

False <= shallower(node(e, t1, t2), z)  :
No: ()


-------------------------------------------
Step 3, which took 0.007539 s (model generation: 0.007460,  model checking: 0.000079):

Clauses:
{
shallower(leaf, n) <= True -> 0
le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0
le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m) -> 0
shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
shallower(t1, n) <= shallower(node(e, t1, t2), s(n)) -> 0
shallower(t2, n) <= shallower(node(e, t1, t2), s(n)) -> 0
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

shallower(leaf, n) <= True  :
No: ()

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

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

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

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

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
No: ()

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
No: ()

shallower(t1, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

shallower(t2, n) <= shallower(node(e, t1, t2), s(n))  :
No: ()

False <= shallower(node(e, t1, t2), z)  :
Yes: {

}


Total time: 0.176176
Learner time: 0.028157
Teacher time: 0.000323
Reasons for stopping: Yes: |_
name: None

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


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


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



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