Solving ../../benchmarks/smtlib/true/tree_shallow_taller_subtree.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)
}
)
(subtree, P:
{
subtree(leaf, t) <= True
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
False <= subtree(node(ea, ta1, ta2), leaf)
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
}
)
(max, F:
{
le_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= le_nat(n, m)
}
eq_nat(_ma, _na) <= max(_ka, _la, _ma) /\ max(_ka, _la, _na)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)
}
eq_nat(_ta, _ua) <= height(_sa, _ta) /\ height(_sa, _ua)
)
(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)
}
)
(taller, P:
{
taller(leaf, z) <= True
taller(node(e, t1, t2), z) <= True
taller(node(e, t1, t2), s(m)) <= taller(t1, m)
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m)
False <= taller(leaf, s(m))
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m))
}
)
}

properties:
{
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)
}


over-approximation: {height, le_nat, max, shallower, subtree, taller}
under-approximation: {height, le_nat, leq_nat, max}

Clause system for inference is:

{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}


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

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


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


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


;
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)
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
}
]


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



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

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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


;
subtree ->
[
subtree : <etree * etree>
{
  
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
Yes: {
t -> node(_ipbpw_0, _ipbpw_1, _ipbpw_2)
}

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

}

taller(node(e, t1, t2), z) <= True  :
Yes: {

}

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

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

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


-------------------------------------------
Step 1, which took 0.007108 s (model generation: 0.006958,  model checking: 0.000150):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


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


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


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


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, z) <= True
  taller(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  :
Yes: {
n -> s(_jpbpw_0)
}

subtree(leaf, t) <= True  :
Yes: {
t -> leaf
}

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_qpbpw_0, _qpbpw_1, _qpbpw_2)  ;  tb2 -> node(_rpbpw_0, _rpbpw_1, _rpbpw_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> node(_vpbpw_0, _vpbpw_1, _vpbpw_2)
}

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

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


-------------------------------------------
Step 2, which took 0.009274 s (model generation: 0.009058,  model checking: 0.000216):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


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


;
leq_nat ->
[
leq_nat : <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
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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(_ypbpw_0, _ypbpw_1, _ypbpw_2)
}

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> z  ;  n2 -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> node(_mqbpw_0, _mqbpw_1, _mqbpw_2)
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_vqbpw_0, _vqbpw_1, _vqbpw_2)  ;  ta2 -> node(_wqbpw_0, _wqbpw_1, _wqbpw_2)  ;  tb1 -> node(_xqbpw_0, _xqbpw_1, _xqbpw_2)  ;  tb2 -> leaf
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_zqbpw_0, _zqbpw_1, _zqbpw_2)  ;  tb1 -> leaf
}

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

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

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


-------------------------------------------
Step 3, which took 0.011401 s (model generation: 0.011133,  model checking: 0.000268):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, 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))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
taller(leaf, s(z)) <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


;
leq_nat ->
[
leq_nat : <nat * nat>
{
  leq_nat(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
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, s(x_1_0)) <= True
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

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

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> z  ;  n2 -> s(_zsbpw_0)  ;  t1 -> node(_atbpw_0, _atbpw_1, _atbpw_2)  ;  t2 -> node(_btbpw_0, _btbpw_1, _btbpw_2)
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

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

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


-------------------------------------------
Step 4, which took 0.011474 s (model generation: 0.011325,  model checking: 0.000149):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(z, s(z)) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), 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))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
taller(leaf, s(z)) <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


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


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, s(x_1_0)) <= True
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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))  :
Yes: {
nn1 -> s(_ctbpw_0)  ;  nn2 -> z
}

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> s(_qtbpw_0)  ;  n2 -> z  ;  t1 -> node(_stbpw_0, _stbpw_1, _stbpw_2)  ;  t2 -> node(_ttbpw_0, _ttbpw_1, _ttbpw_2)
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

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

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


-------------------------------------------
Step 5, which took 0.012332 s (model generation: 0.012149,  model checking: 0.000183):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z))
leq_nat(s(z), z) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), s(z))
leq_nat(z, s(z)) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), 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))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
taller(leaf, s(z)) <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


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


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, s(x_1_0)) <= True
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

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

}

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

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

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

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


-------------------------------------------
Step 6, which took 0.118254 s (model generation: 0.014346,  model checking: 0.103908):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), s(z))
leq_nat(z, s(z)) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), 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))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
taller(leaf, s(z)) <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


;
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)
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, s(x_1_0)) <= True
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> s(_nwbpw_0)  ;  n2 -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

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

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


-------------------------------------------
Step 7, which took 0.104171 s (model generation: 0.012509,  model checking: 0.091662):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), s(z))
leq_nat(z, s(z)) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), 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))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


;
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)
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= taller(x_0_1, x_1_0)
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> s(z)  ;  n2 -> z  ;  t1 -> node(_rnepw_0, leaf, leaf)  ;  t2 -> leaf
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

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

taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m)  :
Yes: {
m -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_hoepw_0, node(_mpepw_0, _mpepw_1, _mpepw_2), _hoepw_2)
}

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


-------------------------------------------
Step 8, which took 0.172802 s (model generation: 0.014004,  model checking: 0.158798):

Clauses:
{
shallower(leaf, n) <= True -> 0
subtree(leaf, t) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa) -> 0
height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa) -> 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
False <= leq_nat(s(nn1), z) -> 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
leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(t1, m) <= shallower(node(e, t1, t2), s(m)) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
taller(node(e, t1, t2), s(m)) <= taller(t1, m) -> 0
taller(t1, m) \/ taller(node(e, t1, t2), s(m)) <= taller(t2, m) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
False <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), s(z))
leq_nat(z, s(z)) <= shallower(node(a, leaf, leaf), z) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ taller(node(a, leaf, leaf), 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))
False <= subtree(node(a, leaf, leaf), leaf) /\ taller(node(a, leaf, leaf), s(z))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

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


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


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


;
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)
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= subtree(x_0_1, x_1_2)
}
]


;
taller ->
[
taller : <etree * nat>
{
  taller(leaf, z) <= True
  taller(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= taller(x_0_2, x_1_0)
  taller(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: ()

subtree(leaf, t) <= True  :
No: ()

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

taller(node(e, t1, t2), z) <= True  :
No: ()

height(node(e, t1, t2), s(_ra)) \/ le_nat(_oa, _pa) <= height(t1, _oa) /\ height(t1, _ra) /\ height(t2, _pa)  :
No: ()

height(node(e, t1, t2), s(_qa)) <= height(t1, _oa) /\ height(t2, _pa) /\ height(t2, _qa) /\ le_nat(_oa, _pa)  :
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: ()

False <= leq_nat(s(nn1), z)  :
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: ()

leq_nat(n1, n2) <= shallower(t1, n1) /\ shallower(t2, n2) /\ subtree(t1, t2) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
n1 -> s(s(z))  ;  n2 -> s(z)  ;  t1 -> node(_oghpw_0, leaf, node(_ilhpw_0, leaf, leaf))  ;  t2 -> node(_pghpw_0, leaf, leaf)
}

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> node(_uhhpw_0, node(_lohpw_0, leaf, _lohpw_2), _uhhpw_2)  ;  ta2 -> leaf  ;  tb1 -> node(_whhpw_0, _whhpw_1, node(_mohpw_0, _mohpw_1, node(_emhpw_0, _emhpw_1, _emhpw_2)))  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_pihpw_0, _pihpw_1, _pihpw_2)  ;  tb1 -> node(_qihpw_0, _qihpw_1, _qihpw_2)  ;  tb2 -> leaf
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_ejhpw_0, leaf, _ejhpw_2)  ;  tb1 -> leaf  ;  tb2 -> node(_llhpw_0, _llhpw_1, node(_emhpw_0, _emhpw_1, _emhpw_2))
}

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> s(z)  ;  t1 -> node(_ljhpw_0, _ljhpw_1, node(_pmhpw_0, _pmhpw_1, _pmhpw_2))  ;  t2 -> leaf
}

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

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


Total time: 0.828463
Learner time: 0.097918
Teacher time: 0.355465
Reasons for stopping: Yes: |_
name: None

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


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


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


;
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)
}
]


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
}
]


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



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