Solving ../../benchmarks/smtlib/true/tree_height_heightRB.smt2...

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



Learning problem is:

env: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq_nat, P:
{
leq_nat(z, n2) <= True
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2)
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2))
False <= leq_nat(s(nn1), z)
}
)
(le_nat, P:
{
le_nat(z, s(nn2)) <= True
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2)
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2))
False <= le_nat(s(nn1), z)
False <= le_nat(z, z)
}
)
(max, F:
{
max(s(nn), z, s(nn)) <= True
max(z, m, m) <= True
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)
}
eq_nat(_up, _vp) <= max(_sp, _tp, _up) /\ max(_sp, _tp, _vp)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)
}
eq_nat(_aq, _bq) <= height(_zp, _aq) /\ height(_zp, _bq)
)
(height_rb, F:
{
height_rb(leaf, z) <= True
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)
}
eq_nat(_eq, _fq) <= height_rb(_dq, _eq) /\ height_rb(_dq, _fq)
)
}

properties:
{
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)
}


over-approximation: {height, height_rb, le_nat, max}
under-approximation: {le_nat, leq_nat}

Clause system for inference is:

{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}


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

height ->
[
height : <etree * nat>
{
  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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


;
max ->
[
max : <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(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq_nat(x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= leq_nat(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.006125 s (model generation: 0.006040,  model checking: 0.000085):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


;
le_nat ->
[
le_nat : <nat * 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: {

}

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

}

max(s(nn), z, s(nn)) <= True  :
Yes: {

}

max(z, m, m) <= True  :
Yes: {
m -> z
}

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 1, which took 0.007142 s (model generation: 0.007014,  model checking: 0.000128):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height_rb(leaf, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
Yes: {
m -> s(_iomhp_0)
}

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
Yes: {
_wp -> z  ;  _xp -> z  ;  _yp -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> z  ;  _hq -> z  ;  t2 -> leaf
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
Yes: {
_cq -> z  ;  t2 -> leaf
}

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
Yes: {
_rp -> z  ;  mm -> z  ;  nn -> z
}


-------------------------------------------
Step 2, which took 0.009660 s (model generation: 0.009551,  model checking: 0.000109):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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

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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(_zomhp_0)  ;  _hq -> s(_apmhp_0)  ;  t2 -> node(_bpmhp_0, _bpmhp_1, _bpmhp_2)
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 3, which took 0.008840 s (model generation: 0.008738,  model checking: 0.000102):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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

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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 4, which took 0.009117 s (model generation: 0.008929,  model checking: 0.000188):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 5, which took 0.009212 s (model generation: 0.009138,  model checking: 0.000074):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

}

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 6, which took 0.009583 s (model generation: 0.009381,  model checking: 0.000202):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(s(_zpmhp_0))  ;  _hq -> s(z)  ;  t2 -> node(_mpmhp_0, _mpmhp_1, _mpmhp_2)
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 7, which took 0.009615 s (model generation: 0.009436,  model checking: 0.000179):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(s(z))  ;  _hq -> s(z)  ;  t2 -> node(_dqmhp_0, _dqmhp_1, node(_vqmhp_0, _vqmhp_1, leaf))
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 8, which took 0.009807 s (model generation: 0.009640,  model checking: 0.000167):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(s(_xrmhp_0))  ;  _hq -> s(z)  ;  t2 -> node(_ermhp_0, node(_wrmhp_0, _wrmhp_1, _wrmhp_2), _ermhp_2)
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
Yes: {
_cq -> z  ;  t1 -> node(_zrmhp_0, _zrmhp_1, _zrmhp_2)  ;  t2 -> leaf
}

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 9, which took 0.011270 s (model generation: 0.010897,  model checking: 0.000373):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(s(z))  ;  _hq -> s(z)  ;  t2 -> node(_csmhp_0, node(_ctmhp_0, node(_jtmhp_0, _jtmhp_1, _jtmhp_2), node(_jtmhp_0, _jtmhp_1, _jtmhp_2)), node(_ctmhp_0, node(_jtmhp_0, _jtmhp_1, _jtmhp_2), node(_jtmhp_0, _jtmhp_1, _jtmhp_2)))
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
Yes: {
_cq -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_gsmhp_0, node(_ttmhp_0, _ttmhp_1, _ttmhp_2), node(_ttmhp_0, _ttmhp_1, _ttmhp_2))
}

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 10, which took 0.014274 s (model generation: 0.013941,  model checking: 0.000333):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(a, leaf, leaf), s(z)) <= True
height_rb(leaf, z) <= True
height_rb(node(a, leaf, leaf), s(z)) <= True
height_rb(node(a, node(a, leaf, leaf), leaf), s(z)) <= True
leq_nat(s(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, node(a, leaf, leaf)), s(z)) /\ height_rb(node(a, leaf, node(a, leaf, leaf)), s(s(z)))
False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ height_rb(node(a, node(a, leaf, leaf), leaf), 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(z)) /\ height_rb(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z)))
False <= height_rb(node(a, leaf, leaf), s(s(z)))
height_rb(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height_rb(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= leq_nat(s(s(z)), s(z))
leq_nat(z, s(z)) <= leq_nat(s(z), s(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_rb(x_0_2, x_1_0)
  height_rb(leaf, z) <= True
  height_rb(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
Yes: {
_wp -> s(z)  ;  _xp -> z  ;  _yp -> s(_yumhp_0)  ;  t1 -> node(_zumhp_0, _zumhp_1, leaf)  ;  t2 -> leaf
}

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 11, which took 0.014512 s (model generation: 0.014082,  model checking: 0.000430):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
Yes: {
_wp -> z  ;  _xp -> s(s(s(z)))  ;  _yp -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_lxmhp_0, _lxmhp_1, node(_czmhp_0, _czmhp_1, node(_tzmhp_0, _tzmhp_1, leaf)))
}

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 12, which took 0.018460 s (model generation: 0.018194,  model checking: 0.000266):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
No: ()

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(s(z))  ;  _hq -> s(z)  ;  t2 -> node(_yzmhp_0, node(_bbnhp_0, node(_ibnhp_0, _ibnhp_1, _ibnhp_2), leaf), node(_zanhp_0, _zanhp_1, _zanhp_2))
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
Yes: {
_cq -> z  ;  t2 -> node(_eanhp_0, _eanhp_1, _eanhp_2)
}

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 13, which took 0.021603 s (model generation: 0.020917,  model checking: 0.000686):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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


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


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


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


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



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




Answer of teacher:

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

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
Yes: {
_wp -> z  ;  _xp -> s(z)  ;  _yp -> s(s(_vfnhp_0))  ;  t1 -> leaf  ;  t2 -> node(_pcnhp_0, leaf, leaf)
}

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
Yes: {
_gq -> s(_adnhp_0)  ;  _hq -> z  ;  t2 -> leaf
}

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
Yes: {
_cq -> s(_jdnhp_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


-------------------------------------------
Step 14, which took 0.025659 s (model generation: 0.025122,  model checking: 0.000537):

Clauses:
{
height(leaf, z) <= True -> 0
height_rb(leaf, z) <= True -> 0
max(s(nn), z, s(nn)) <= True -> 0
max(z, m, m) <= True -> 0
height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp) -> 0
leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq) -> 0
height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq) -> 0
le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0
le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0
leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0
leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0
False <= leq_nat(s(nn1), z) -> 0
max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <etree * nat>
{
  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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


;
max ->
[
max : <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(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)) <= leq_nat(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: ()

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

max(s(nn), z, s(nn)) <= True  :
No: ()

max(z, m, m) <= True  :
No: ()

height(node(e, t1, t2), s(_yp)) <= height(t1, _wp) /\ height(t2, _xp) /\ max(_wp, _xp, _yp)  :
Yes: {
_wp -> s(z)  ;  _xp -> s(s(s(z)))  ;  _yp -> s(z)  ;  t1 -> node(_ohnhp_0, _ohnhp_1, leaf)  ;  t2 -> node(_phnhp_0, _phnhp_1, node(_uinhp_0, _uinhp_1, node(_xjnhp_0, _xjnhp_1, leaf)))
}

leq_nat(_gq, _hq) <= height(t2, _hq) /\ height_rb(t2, _gq)  :
No: ()

height_rb(node(e, t1, t2), s(_cq)) <= height_rb(t2, _cq)  :
No: ()

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

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

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

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

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

max(s(nn), s(mm), s(_rp)) <= max(nn, mm, _rp)  :
No: ()


Total time: 0.211737
Learner time: 0.181020
Teacher time: 0.003859
Reasons for stopping: Yes: |_
name: None

height ->
[
height : <etree * nat>
{
  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)) <= height(x_0_2, x_1_0)
}
]


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


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


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


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



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