Solving ../../benchmarks/smtlib/true/tree_height_max_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:
{
(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(_yh, _zh) <= max(_wh, _xh, _yh) /\ max(_wh, _xh, _zh)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)
}
eq_nat(_fi, _gi) <= height(_ei, _fi) /\ height(_ei, _gi)
)
}

properties:
{
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)
}


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

Clause system for inference is:

{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}


Solving took 60.043462 seconds.
Maybe:  timeout during teacher: {
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> out of time
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> out of time
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> out of time
}Last solver state:

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006488 s (model generation: 0.006234,  model checking: 0.000254):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

}

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
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: ()


-------------------------------------------
Step 1, which took 0.006040 s (model generation: 0.005942,  model checking: 0.000098):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> z  ;  _bi -> z  ;  _ci -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
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: ()


-------------------------------------------
Step 2, which took 0.008236 s (model generation: 0.008104,  model checking: 0.000132):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(z)  ;  _ii -> s(_fpnhp_0)  ;  _ji -> z  ;  _ki -> s(_hpnhp_0)  ;  t1 -> node(_ipnhp_0, _ipnhp_1, _ipnhp_2)  ;  t2 -> leaf
}

max(n, m, m) <= leq_nat(n, m)  :
Yes: {
m -> z  ;  n -> s(_npnhp_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: {

}


-------------------------------------------
Step 3, which took 0.008442 s (model generation: 0.008144,  model checking: 0.000298):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> z  ;  _bi -> s(z)  ;  _ci -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_gqnhp_0, leaf, _gqnhp_2)
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(z)  ;  _ji -> z  ;  _ki -> s(s(_xrnhp_0))  ;  t1 -> node(_wqnhp_0, leaf, _wqnhp_2)  ;  t2 -> leaf
}

max(n, m, m) <= leq_nat(n, m)  :
Yes: {
m -> s(_yqnhp_0)  ;  n -> s(_zqnhp_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(_crnhp_0)  ;  nn2 -> z
}

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


-------------------------------------------
Step 4, which took 0.015739 s (model generation: 0.015381,  model checking: 0.000358):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
Yes: {
_ai -> s(_yrnhp_0)  ;  _bi -> z  ;  _di -> s(_asnhp_0)  ;  t1 -> node(_bsnhp_0, leaf, _bsnhp_2)  ;  t2 -> leaf
}

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> s(z)  ;  _bi -> s(z)  ;  _ci -> s(_usnhp_0)  ;  t1 -> node(_vsnhp_0, leaf, _vsnhp_2)  ;  t2 -> node(_wsnhp_0, leaf, _wsnhp_2)
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(_punhp_0))  ;  _ii -> z  ;  _ji -> z  ;  _ki -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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


-------------------------------------------
Step 5, which took 0.036377 s (model generation: 0.034383,  model checking: 0.001994):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(z)  ;  _ii -> s(_wbohp_0)  ;  _ji -> s(s(s(_jeohp_0)))  ;  _ki -> s(_ybohp_0)  ;  t1 -> node(_zbohp_0, _zbohp_1, node(_eeohp_0, _eeohp_1, _eeohp_2))  ;  t2 -> node(_acohp_0, node(_nfohp_0, node(_ieohp_0, _ieohp_1, node(_eeohp_0, _eeohp_1, _eeohp_2)), _nfohp_2), _acohp_2)
}

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(_sdohp_0)
}

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

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


-------------------------------------------
Step 6, which took 0.051085 s (model generation: 0.048990,  model checking: 0.002095):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(z)  ;  _ii -> z  ;  _ji -> s(s(_wrohp_0))  ;  _ki -> s(_znohp_0)  ;  t1 -> leaf  ;  t2 -> node(_boohp_0, _boohp_1, node(_vrohp_0, _vrohp_1, _vrohp_2))
}

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

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

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

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


-------------------------------------------
Step 7, which took 0.054988 s (model generation: 0.053001,  model checking: 0.001987):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(s(s(_qfphp_0)))  ;  _ji -> s(s(s(s(_qfphp_0))))  ;  _ki -> s(s(_aiphp_0))  ;  t1 -> node(_sephp_0, node(_fgphp_0, _fgphp_1, node(_pfphp_0, _pfphp_1, _pfphp_2)), _sephp_2)  ;  t2 -> node(_tephp_0, node(_qhphp_0, node(_fgphp_0, _fgphp_1, node(_pfphp_0, _pfphp_1, _pfphp_2)), _qhphp_2), _tephp_2)
}

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


-------------------------------------------
Step 8, which took 0.072691 s (model generation: 0.067251,  model checking: 0.005440):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
Yes: {
_ai -> s(_mkphp_0)  ;  _bi -> z  ;  _di -> s(_okphp_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> z  ;  _bi -> z  ;  _ci -> s(_jeqhp_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(z)  ;  _ii -> s(z)  ;  _ji -> s(z)  ;  _ki -> s(_cxqhp_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

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


-------------------------------------------
Step 9, which took 0.676014 s (model generation: 0.078392,  model checking: 0.597622):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> s(z)  ;  _bi -> s(s(z))  ;  _ci -> s(s(z))  ;  t1 -> node(_jorhp_0, leaf, node(_xkthp_0, node(_xlshp_0, _xlshp_1, _xlshp_2), _xkthp_2))  ;  t2 -> node(_korhp_0, node(_txshp_0, leaf, _txshp_2), _korhp_2)
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(z)  ;  _ji -> s(z)  ;  _ki -> s(s(_ayrhp_0))  ;  t1 -> node(_ssrhp_0, leaf, _ssrhp_2)  ;  t2 -> node(_tsrhp_0, leaf, _tsrhp_2)
}

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


-------------------------------------------
Step 10, which took 0.827664 s (model generation: 0.235803,  model checking: 0.591861):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
Yes: {
_ai -> z  ;  _bi -> s(s(z))  ;  _ci -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(a, leaf, node(_ypjkp_0, leaf, _ypjkp_2))
}

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(z)  ;  _ii -> z  ;  _ji -> s(z)  ;  _ki -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_rijkp_0, leaf, _rijkp_2)
}

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


-------------------------------------------
Step 11, which took 0.772114 s (model generation: 0.147966,  model checking: 0.624148):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> z  ;  _ji -> s(z)  ;  _ki -> s(s(_bxkop_0))  ;  t1 -> leaf  ;  t2 -> node(_bjkop_0, leaf, leaf)
}

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


-------------------------------------------
Step 12, which took 0.730032 s (model generation: 0.143086,  model checking: 0.586946):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(s(s(z))))  ;  _ii -> s(s(s(z)))  ;  _ji -> z  ;  _ki -> s(s(z))  ;  t1 -> node(_cxxrp_0, node(_yhyrp_0, node(_zxyrp_0, _zxyrp_1, _zxyrp_2), node(_byyrp_0, leaf, leaf)), node(_whyrp_0, node(_rfzrp_0, _rfzrp_1, _rfzrp_2), node(_tfzrp_0, leaf, leaf)))  ;  t2 -> leaf
}

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


-------------------------------------------
Step 13, which took 0.186324 s (model generation: 0.168087,  model checking: 0.018237):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
No: ()

height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi)  :
No: ()

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(s(_mrjtp_0))  ;  _ji -> s(s(z))  ;  _ki -> s(s(z))  ;  t1 -> node(_ckjtp_0, _ckjtp_1, node(_lrjtp_0, _lrjtp_1, _lrjtp_2))  ;  t2 -> node(_dkjtp_0, _dkjtp_1, node(_fsjtp_0, _fsjtp_1, _fsjtp_2))
}

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


-------------------------------------------
Step 14, which took 0.752217 s (model generation: 0.171487,  model checking: 0.580730):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(s(z)))  ;  _ii -> s(s(z))  ;  _ji -> s(z)  ;  _ki -> s(z)  ;  t1 -> node(_drktp_0, node(_eavtp_0, leaf, leaf), node(_aavtp_0, _aavtp_1, _aavtp_2))  ;  t2 -> node(_erktp_0, leaf, leaf)
}

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


-------------------------------------------
Step 15, which took 1.298602 s (model generation: 0.174458,  model checking: 1.124144):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


;
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)) <= leq_nat(x_0_0, x_1_0)
  _r_1(z, z) <= True
  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(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
}
]



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(s(z)))  ;  _ii -> s(s(z))  ;  _ji -> z  ;  _ki -> s(s(s(_zjddq_0)))  ;  t1 -> node(_abvxp_0, leaf, node(_xmeyp_0, leaf, leaf))  ;  t2 -> leaf
}

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


-------------------------------------------
Step 16, which took 1.410945 s (model generation: 0.167771,  model checking: 1.243174):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi)  :
Yes: {
_ai -> s(s(z))  ;  _bi -> s(z)  ;  _di -> s(s(z))  ;  t1 -> node(_sjedq_0, node(_boyjq_0, leaf, leaf), leaf)  ;  t2 -> node(_tjedq_0, leaf, leaf)
}

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


-------------------------------------------
Step 17, which took 0.773111 s (model generation: 0.241020,  model checking: 0.532091):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(s(s(z))))  ;  _ii -> s(z)  ;  _ji -> s(s(z))  ;  _ki -> s(s(z))  ;  t1 -> node(_atzjq_0, leaf, leaf)  ;  t2 -> node(_btzjq_0, node(_fpbkq_0, leaf, leaf), node(_zobkq_0, node(_hofkq_0, leaf, leaf), node(_fofkq_0, _fofkq_1, _fofkq_2)))
}

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


-------------------------------------------
Step 18, which took 0.771927 s (model generation: 0.249678,  model checking: 0.522249):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(s(z))  ;  _ji -> s(z)  ;  _ki -> s(s(z))  ;  t1 -> node(_zdznq_0, node(_cseoq_0, leaf, leaf), leaf)  ;  t2 -> node(_aeznq_0, leaf, leaf)
}

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


-------------------------------------------
Step 19, which took 0.727294 s (model generation: 0.211218,  model checking: 0.516076):

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

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

eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki)  :
Yes: {
_hi -> s(s(z))  ;  _ii -> s(s(z))  ;  _ji -> s(z)  ;  _ki -> s(s(z))  ;  t1 -> node(_zwfrq_0, leaf, node(_yojrq_0, leaf, leaf))  ;  t2 -> node(_axfrq_0, leaf, leaf)
}

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


Total time: 60.043462
Learner time: 2.236396
Teacher time: 6.949934
Reasons for stopping: Maybe:  timeout during teacher: {
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> out of time
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> out of time
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> out of time
}Last solver state:

Clauses:
{
height(leaf, z) <= True -> 0
leq_nat(n, m) \/ max(n, m, n) <= True -> 0
leq_nat(z, n2) <= True -> 0
height(node(e, t1, t2), s(_di)) \/ leq_nat(_ai, _bi) <= height(t1, _ai) /\ height(t1, _di) /\ height(t2, _bi) -> 0
height(node(e, t1, t2), s(_ci)) <= height(t1, _ai) /\ height(t2, _bi) /\ height(t2, _ci) /\ leq_nat(_ai, _bi) -> 0
eq_nat(_hi, s(_ki)) <= height(t1, _ii) /\ height(t2, _ji) /\ height(node(e, t1, t2), _hi) /\ max(_ii, _ji, _ki) -> 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
}

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

Current best model:
|_
name: None

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


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



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