Solving ../../benchmarks/smtlib/true/tree_shallower_rec_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}  ;  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)
}
)
(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(t, n2) <= leq(n1, n2) /\ shallower(t, n1)
}


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

Clause system for inference is:

{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}


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

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


;
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.006395 s (model generation: 0.006330,  model checking: 0.000065):

Clauses:
{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1)  :
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: ()

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


-------------------------------------------
Step 1, which took 0.006361 s (model generation: 0.006290,  model checking: 0.000071):

Clauses:
{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

leq(z, n2) <= True  :
Yes: {
n2 -> s(_rfspw_0)
}

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

shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1)  :
No: ()

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

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: ()

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


-------------------------------------------
Step 2, which took 0.009114 s (model generation: 0.008099,  model checking: 0.001015):

Clauses:
{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


;
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:

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

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

shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1)  :
No: ()

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

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

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(_cgspw_0, _cgspw_1, _cgspw_2)
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> node(_egspw_0, _egspw_1, _egspw_2)
}

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


-------------------------------------------
Step 3, which took 0.015484 s (model generation: 0.015374,  model checking: 0.000110):

Clauses:
{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
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

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


;
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:

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

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

shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1)  :
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: ()

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

}


-------------------------------------------
Step 4, which took 0.165787 s (model generation: 0.009867,  model checking: 0.155920):

Clauses:
{
leq(z, n2) <= True -> 0
shallower(leaf, n) <= True -> 0
shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1) -> 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
False <= shallower(node(e, t1, t2), z) -> 0
}

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

Current best model:
|_
name: None

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


;
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}
_|




Answer of teacher:

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

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

shallower(t, n2) <= leq(n1, n2) /\ shallower(t, n1)  :
Yes: {
n1 -> s(z)  ;  n2 -> z  ;  t -> node(_ngspw_0, leaf, leaf)
}

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: ()

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


Total time: 0.291415
Learner time: 0.045960
Teacher time: 0.157181
Reasons for stopping: Yes: |_
name: None

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


;
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}
_|