Solving ../../benchmarks/smtlib/true/tree_shallow_taller_node.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:
{
(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)
}
)
(max, F:
{
le_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= le_nat(n, m)
}
eq_nat(_i, _j) <= max(_g, _h, _i) /\ max(_g, _h, _j)
)
(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:
{
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)
}


over-approximation: {max}
under-approximation: {}

Clause system for inference is:

{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}


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

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


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  max(z, 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)
}
]


;
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.006236 s (model generation: 0.006067,  model checking: 0.000169):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


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



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




Answer of teacher:

le_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> z
}

le_nat(z, s(nn2)) <= True  :
Yes: {

}

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

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

}

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

}

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
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: ()

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

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 1, which took 0.007085 s (model generation: 0.006746,  model checking: 0.000339):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
le_nat(z, s(z)) <= True
le_nat(z, z) \/ max(z, z, z) <= True
shallower(leaf, z) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
}

Current best model:
|_
name: None

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


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


;
shallower ->
[
shallower : <etree * nat>
{
  shallower(leaf, z) <= 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:

le_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> s(_anvnw_0)
}

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
Yes: {
m -> s(_cnvnw_0)  ;  n -> z
}

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

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

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

False <= le_nat(z, z)  :
Yes: {

}

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> z  ;  n1 -> z  ;  n2 -> z  ;  t1 -> node(_vnvnw_0, _vnvnw_1, _vnvnw_2)  ;  t2 -> leaf
}

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

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

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> node(_novnw_0, _novnw_1, _novnw_2)
}

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

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 2, which took 0.010742 s (model generation: 0.010410,  model checking: 0.000332):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

Accumulated learning constraints:
{
le_nat(s(z), z) \/ max(s(z), z, s(z)) <= True
le_nat(z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
shallower(leaf, s(z)) <= True
shallower(leaf, z) <= True
shallower(node(a, leaf, leaf), s(z)) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
taller(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
False <= le_nat(z, z)
}

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, 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
}
]


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

le_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> s(_oovnw_0)  ;  n -> s(_povnw_0)
}

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
Yes: {
m -> z  ;  n -> s(_rovnw_0)
}

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

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

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

}

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
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(_yovnw_0, _yovnw_1, _yovnw_2)
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> z  ;  t1 -> node(_apvnw_0, _apvnw_1, _apvnw_2)
}

False <= shallower(node(e, t1, t2), z)  :
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: ()

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 3, which took 0.013234 s (model generation: 0.012986,  model checking: 0.000248):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, 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
}
]


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

le_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
No: ()

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
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: {

}

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

False <= taller(leaf, s(m))  :
Yes: {

}

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


-------------------------------------------
Step 4, which took 0.074785 s (model generation: 0.010312,  model checking: 0.064473):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, 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)
}
]


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

le_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> s(_xpvnw_0)  ;  n1 -> s(z)  ;  n2 -> z  ;  t1 -> node(_aqvnw_0, _aqvnw_1, node(_xawnw_0, _xawnw_1, _xawnw_2))  ;  t2 -> leaf
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(z)  ;  n1 -> s(z)  ;  n2 -> s(s(z))  ;  t1 -> node(_xsvnw_0, leaf, leaf)  ;  t2 -> node(_ysvnw_0, leaf, node(_ubwnw_0, leaf, leaf))
}

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

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> s(z)  ;  t1 -> node(_zwvnw_0, _zwvnw_1, node(_pyvnw_0, _pyvnw_1, _pyvnw_2))  ;  t2 -> leaf
}

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

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 5, which took 0.091602 s (model generation: 0.013400,  model checking: 0.078202):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, 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)
}
]


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

le_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> s(_wsynw_0)  ;  n1 -> z  ;  n2 -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_atynw_0, node(_ocznw_0, _ocznw_1, _ocznw_2), _atynw_2)
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(z)  ;  n1 -> s(s(z))  ;  n2 -> z  ;  t1 -> node(_bwynw_0, leaf, node(_rdznw_0, leaf, leaf))  ;  t2 -> leaf
}

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

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(_tzynw_0, node(_vaznw_0, _vaznw_1, _vaznw_2), _tzynw_2)
}

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 6, which took 0.035816 s (model generation: 0.034859,  model checking: 0.000957):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


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


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


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

le_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> z  ;  n1 -> z  ;  n2 -> z  ;  t1 -> node(_jlbow_0, _jlbow_1, _jlbow_2)  ;  t2 -> node(_klbow_0, _klbow_1, _klbow_2)
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(_zmbow_0)  ;  n1 -> s(_anbow_0)  ;  n2 -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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

shallower(t2, m) <= shallower(t1, m) /\ shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> s(z)  ;  t1 -> node(_lqbow_0, leaf, leaf)  ;  t2 -> node(_mqbow_0, _mqbow_1, node(_ksbow_0, _ksbow_1, _ksbow_2))
}

shallower(t1, m) <= shallower(node(e, t1, t2), s(m))  :
Yes: {
m -> s(z)  ;  t1 -> node(_tqbow_0, _tqbow_1, node(_dsbow_0, _dsbow_1, _dsbow_2))  ;  t2 -> node(_fsbow_0, _fsbow_1, _fsbow_2)
}

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

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> node(_brbow_0, _brbow_1, _brbow_2)  ;  t2 -> node(_vrbow_0, _vrbow_1, _vrbow_2)
}

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

False <= taller(leaf, s(m))  :
No: ()

taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m))  :
Yes: {
m -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_nrbow_0, _nrbow_1, node(_yrbow_0, _yrbow_1, _yrbow_2))
}


-------------------------------------------
Step 7, which took 0.120406 s (model generation: 0.038419,  model checking: 0.081987):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


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


;
shallower ->
[
shallower : <etree * nat>
{
  _r_1(leaf, s(x_1_0)) <= True
  _r_1(leaf, z) <= True
  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)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0)
}
]


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




Answer of teacher:

le_nat(n, m) \/ max(n, m, n) <= True  :
No: ()

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> s(s(_xgcow_0))  ;  n1 -> s(z)  ;  n2 -> z  ;  t1 -> node(_aubow_0, leaf, leaf)  ;  t2 -> node(_bubow_0, leaf, leaf)
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(_yxbow_0)  ;  n1 -> s(z)  ;  n2 -> z  ;  t1 -> node(_bybow_0, leaf, leaf)  ;  t2 -> leaf
}

shallower(node(e, t1, t2), s(m)) <= shallower(t1, m) /\ shallower(t2, m)  :
Yes: {
m -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_xzbow_0, leaf, 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: ()

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

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 8, which took 0.229673 s (model generation: 0.051775,  model checking: 0.177898):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, 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)
}
]


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




Answer of teacher:

le_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> z  ;  n -> s(s(_toeow_0))
}

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
Yes: {
m -> s(s(_xoeow_0))  ;  n -> s(z)
}

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> s(s(_ateow_0))  ;  n1 -> z  ;  n2 -> s(z)  ;  t1 -> node(_ugeow_0, leaf, leaf)  ;  t2 -> node(_vgeow_0, leaf, leaf)
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(z)  ;  n1 -> z  ;  n2 -> s(s(z))  ;  t1 -> leaf  ;  t2 -> node(_rkeow_0, leaf, node(_kueow_0, leaf, leaf))
}

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

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

False <= taller(leaf, s(m))  :
No: ()

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


-------------------------------------------
Step 9, which took 0.242170 s (model generation: 0.059950,  model checking: 0.182220):

Clauses:
{
le_nat(n, m) \/ max(n, m, n) <= True -> 0
le_nat(z, s(nn2)) <= True -> 0
shallower(leaf, n) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
max(n, m, m) <= le_nat(n, m) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
False <= le_nat(s(nn1), z) -> 0
False <= le_nat(z, z) -> 0
taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2) -> 0
shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2) -> 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
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
False <= taller(leaf, s(m)) -> 0
taller(t1, m) \/ taller(t2, m) <= taller(node(e, t1, t2), s(m)) -> 0
}

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

Current best model:
|_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  max(z, 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)
}
]


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




Answer of teacher:

le_nat(n, m) \/ max(n, m, n) <= True  :
Yes: {
m -> s(z)  ;  n -> s(s(_wykow_0))
}

le_nat(z, s(nn2)) <= True  :
No: ()

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

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

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

max(n, m, m) <= le_nat(n, m)  :
No: ()

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

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

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

False <= le_nat(z, z)  :
No: ()

taller(node(e, t1, t2), s(_k)) <= max(n1, n2, _k) /\ taller(t1, n1) /\ taller(t2, n2)  :
Yes: {
_k -> s(s(s(_fpmow_0)))  ;  n1 -> z  ;  n2 -> s(s(z))  ;  t1 -> node(_cqkow_0, leaf, leaf)  ;  t2 -> node(_dqkow_0, node(_sblow_0, leaf, leaf), leaf)
}

shallower(node(e, t1, t2), s(_l)) <= max(n1, n2, _l) /\ shallower(t1, n1) /\ shallower(t2, n2)  :
Yes: {
_l -> s(z)  ;  n1 -> s(s(z))  ;  n2 -> s(z)  ;  t1 -> node(_askow_0, leaf, node(_ohlow_0, leaf, leaf))  ;  t2 -> leaf
}

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

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

False <= taller(leaf, s(m))  :
No: ()

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


Total time: 1.167512
Learner time: 0.244924
Teacher time: 0.586825
Reasons for stopping: Yes: |_
name: None

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


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  max(z, 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)
}
]


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