Solving ../../benchmarks/smtlib/true/tree_higher_leq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(max, F:
{
leq_nat(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= leq_nat(n, m)
}
eq_nat(_bz, _cz) <= max(_zy, _az, _bz) /\ max(_zy, _az, _cz)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)
}
eq_nat(_iz, _jz) <= height(_hz, _iz) /\ height(_hz, _jz)
)
(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(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)
}


over-approximation: {height, max, shallower}
under-approximation: {height, shallower}

Clause system for inference is:

{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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 0.971777 seconds.
Yes: |_
name: None

height ->
[
height : <etree * 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
}
]


;
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)) <= _r_1(x_0_0, x_2_0)
  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>
{
  
}
]


;
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.006234 s (model generation: 0.006101,  model checking: 0.000133):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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

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


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

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

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

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

}

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

}

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

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.007271 s (model generation: 0.007069,  model checking: 0.000202):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(z, z) <= True
taller(leaf, z) <= True
taller(node(a, leaf, leaf), z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> node(_oerfw_0, _oerfw_1, _oerfw_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.013485 s (model generation: 0.013010,  model checking: 0.000475):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(s(z), z) \/ max(s(z), z, s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(z, z, z) <= 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>
{
  
}
]


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


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


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

}

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

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(_verfw_0)  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 3, which took 0.015560 s (model generation: 0.015428,  model checking: 0.000132):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, 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 <= leq_nat(s(z), z)
taller(leaf, s(z)) <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
Yes: {
m -> s(_yerfw_0)  ;  n -> s(_zerfw_0)
}

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

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

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.009745 s (model generation: 0.009083,  model checking: 0.000662):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, z, 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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


;
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, z, z) <= True
}
]


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(s(_fjrfw_0))  ;  m -> z  ;  n -> s(z)  ;  t1 -> node(_yfrfw_0, leaf, _yfrfw_2)  ;  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: ()

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(_hhrfw_0, node(_cirfw_0, _cirfw_1, _cirfw_2), _hhrfw_2)
}

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.023703 s (model generation: 0.022779,  model checking: 0.000924):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
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)
taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) /\ taller(node(a, leaf, leaf), s(z))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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



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




Answer of teacher:

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> z  ;  m -> z  ;  n -> z  ;  t1 -> 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: ()

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> leaf  ;  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))  :
Yes: {
m -> s(_ynrfw_0)  ;  t1 -> node(_znrfw_0, leaf, leaf)  ;  t2 -> leaf
}


-------------------------------------------
Step 6, which took 0.022482 s (model generation: 0.021615,  model checking: 0.000867):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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)
taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


;
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_1, x_1_0)
  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:

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> z  ;  m -> z  ;  n -> z  ;  t1 -> node(_xrrfw_0, _xrrfw_1, _xrrfw_2)  ;  t2 -> node(_xrrfw_0, _xrrfw_1, _xrrfw_2)
}

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

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> z  ;  t1 -> node(_gsrfw_0, _gsrfw_1, _gsrfw_2)  ;  t2 -> node(_rtrfw_0, _rtrfw_1, _rtrfw_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 -> node(_gtrfw_0, node(_xtrfw_0, _xtrfw_1, _xtrfw_2), node(_vtrfw_0, _vtrfw_1, _vtrfw_2))  ;  t2 -> leaf
}


-------------------------------------------
Step 7, which took 0.024489 s (model generation: 0.023425,  model checking: 0.001064):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

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(s(_dzrfw_0))  ;  t1 -> node(_ryrfw_0, leaf, leaf)  ;  t2 -> leaf
}


-------------------------------------------
Step 8, which took 0.025513 s (model generation: 0.024725,  model checking: 0.000788):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z)))
False <= taller(leaf, s(z))
False <= taller(node(a, leaf, leaf), s(s(z)))
taller(leaf, s(s(z))) <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

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


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


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


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(z)  ;  m -> z  ;  n -> s(z)  ;  t1 -> node(_zzrfw_0, _zzrfw_1, node(_qdsfw_0, _qdsfw_1, _qdsfw_2))  ;  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: ()

taller(node(e, t1, t2), s(m)) <= taller(t1, m)  :
Yes: {
m -> s(z)  ;  t1 -> node(_nbsfw_0, _nbsfw_1, node(_ycsfw_0, _ycsfw_1, _ycsfw_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 9, which took 0.137413 s (model generation: 0.032888,  model checking: 0.104525):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(s(z)), s(s(z))) <= True
leq_nat(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, 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(leaf, s(s(z))) <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(z)  ;  m -> s(s(_xlsfw_0))  ;  n -> z  ;  t1 -> 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: ()

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: {
m -> s(_xlsfw_0)
}

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


-------------------------------------------
Step 10, which took 0.107354 s (model generation: 0.026518,  model checking: 0.080836):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(s(z)), s(s(z))) <= True
leq_nat(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= max(s(z), z, s(s(z)))
False <= taller(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))
False <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

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


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(s(_xwcgw_0))  ;  m -> s(z)  ;  n -> z  ;  t1 -> leaf  ;  t2 -> node(_brcgw_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: ()

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 11, which took 0.142230 s (model generation: 0.030767,  model checking: 0.111463):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(s(z)), s(s(z))) <= True
leq_nat(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
False <= max(s(z), z, s(s(z)))
taller(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= taller(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))
False <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(s(_bcfgw_0))  ;  m -> s(z)  ;  n -> s(z)  ;  t1 -> node(_zuegw_0, leaf, leaf)  ;  t2 -> node(_avegw_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: ()

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 12, which took 0.126777 s (model generation: 0.033643,  model checking: 0.093134):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(s(z)), s(s(z))) <= True
leq_nat(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
taller(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
False <= max(s(z), z, s(s(z)))
taller(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= taller(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))
False <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


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


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

max(n, m, m) <= leq_nat(n, m)  :
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: ()

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
Yes: {
_kz -> s(s(s(_pdigw_0)))  ;  m -> z  ;  n -> s(s(z))  ;  t1 -> node(_cchgw_0, node(_vkhgw_0, leaf, leaf), leaf)  ;  t2 -> node(_dchgw_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: ()

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 13, which took 0.161088 s (model generation: 0.047395,  model checking: 0.113693):

Clauses:
{
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
taller(leaf, z) <= True -> 0
taller(node(e, t1, t2), z) <= True -> 0
height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez) -> 0
height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez) -> 0
max(n, m, m) <= leq_nat(n, m) -> 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
taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m) -> 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
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:
{
leq_nat(s(s(z)), s(s(z))) <= True
leq_nat(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True
leq_nat(s(z), s(s(z))) <= True
leq_nat(s(z), s(z)) <= True
leq_nat(z, s(z)) <= True
leq_nat(z, z) <= True
max(s(s(z)), 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
taller(leaf, z) <= True
taller(node(a, leaf, leaf), s(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 <= leq_nat(s(s(z)), s(z))
False <= leq_nat(s(z), z)
taller(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) <= max(s(s(z)), z, s(s(s(z)))) /\ taller(node(a, node(a, leaf, leaf), leaf), s(s(z)))
taller(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
False <= max(s(z), z, s(s(z)))
taller(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= taller(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))
False <= taller(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
}

Current best model:
|_
name: None

height ->
[
height : <etree * 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
}
]


;
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)) <= _r_1(x_0_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>
{
  
}
]


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

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

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

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

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

height(node(e, t1, t2), s(_gz)) \/ leq_nat(_dz, _ez) <= height(t1, _dz) /\ height(t1, _gz) /\ height(t2, _ez)  :
No: ()

height(node(e, t1, t2), s(_fz)) <= height(t1, _dz) /\ height(t2, _ez) /\ height(t2, _fz) /\ leq_nat(_dz, _ez)  :
No: ()

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

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

taller(node(e, t1, t2), s(_kz)) <= max(n, m, _kz) /\ taller(t1, n) /\ taller(t2, m)  :
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: ()

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: 0.971777
Learner time: 0.314445
Teacher time: 0.508898
Reasons for stopping: Yes: |_
name: None

height ->
[
height : <etree * 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
}
]


;
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)) <= _r_1(x_0_0, x_2_0)
  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>
{
  
}
]


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