Solving ../../benchmarks/smtlib/true/tree_nat_depth_leq_size.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: {
nat -> {s, z}  ;  nattree -> {leaf, node}
}
definition:
{
(leq, P:
{
leq(z, n2) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(max, F:
{
leq(n, m) \/ max(n, m, n) <= True
max(n, m, m) <= leq(n, m)
}
eq_nat(_xx, _yx) <= max(_vx, _wx, _xx) /\ max(_vx, _wx, _yx)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)
}
eq_nat(_cy, _dy) <= plus(_ay, _by, _cy) /\ plus(_ay, _by, _dy)
)
(height, F:
{
height(leaf, z) <= True
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)
}
eq_nat(_iy, _jy) <= height(_hy, _iy) /\ height(_hy, _jy)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)
}
eq_nat(_oy, _py) <= numnodes(_ny, _oy) /\ numnodes(_ny, _py)
)
}

properties:
{
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)
}


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

Clause system for inference is:

{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}


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

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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



--
Equality automata are defined for: {nat, nattree}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006139 s (model generation: 0.005985,  model checking: 0.000154):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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


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


;
numnodes ->
[
numnodes : <nattree * nat>
{
  
}
]


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



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




Answer of teacher:

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

}

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

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

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

}

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

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 1, which took 0.006647 s (model generation: 0.006536,  model checking: 0.000111):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
leq(z, z) <= True
numnodes(leaf, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

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

leq(z, n2) <= True  :
Yes: {
n2 -> s(_uiygw_0)
}

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

plus(n, z, n) <= True  :
Yes: {
n -> s(_viygw_0)
}

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> z  ;  _my -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
Yes: {
_zx -> z  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 2, which took 0.009675 s (model generation: 0.009471,  model checking: 0.000204):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
leq(s(z), s(z)) <= True
leq(s(z), z) \/ max(s(z), z, s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> z  ;  _gy -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

}

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
Yes: {
_zx -> s(_tjygw_0)  ;  mm -> z  ;  n -> s(_vjygw_0)
}


-------------------------------------------
Step 3, which took 0.015416 s (model generation: 0.015308,  model checking: 0.000108):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= leq(s(z), z)
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 4, which took 0.013334 s (model generation: 0.012806,  model checking: 0.000528):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

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


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


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(s(_vkygw_0))  ;  _ry -> s(z)  ;  t1 -> node(_gkygw_0, _gkygw_1, _gkygw_2)
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 5, which took 0.018194 s (model generation: 0.017823,  model checking: 0.000371):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(z, leaf, leaf), s(s(z)))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

height ->
[
height : <nattree * nat>
{
  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)
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> s(z)  ;  _fy -> z  ;  _gy -> s(_plygw_0)  ;  t1 -> node(_qlygw_0, _qlygw_1, leaf)  ;  t2 -> leaf
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(s(z))  ;  _ry -> s(z)  ;  t1 -> node(_zlygw_0, _zlygw_1, node(_nmygw_0, _nmygw_1, leaf))
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 6, which took 0.019655 s (model generation: 0.019292,  model checking: 0.000363):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(z, leaf, leaf), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
}

Current best model:
|_
name: None

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


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(s(_koygw_0))  ;  _gy -> s(_bnygw_0)  ;  t1 -> leaf  ;  t2 -> node(_dnygw_0, node(_joygw_0, _joygw_1, _joygw_2), _dnygw_2)
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(s(_eoygw_0))  ;  _ry -> s(z)  ;  t1 -> node(_qnygw_0, node(_goygw_0, _goygw_1, _goygw_2), _qnygw_2)
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 7, which took 0.014666 s (model generation: 0.013782,  model checking: 0.000884):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(z, leaf, leaf), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(z)  ;  _gy -> s(s(_svygw_0))  ;  t1 -> node(_brygw_0, leaf, leaf)  ;  t2 -> node(_crygw_0, leaf, leaf)
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> s(z)  ;  _my -> s(_ksygw_0)  ;  t1 -> leaf  ;  t2 -> node(_msygw_0, leaf, leaf)
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 8, which took 0.017637 s (model generation: 0.016753,  model checking: 0.000884):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
numnodes(node(z, leaf, node(z, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(z, leaf, leaf), s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= height(node(z, leaf, leaf), z) /\ max(z, s(z), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
}

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(z)  ;  _gy -> s(s(_jczgw_0))  ;  t1 -> leaf  ;  t2 -> node(_jwygw_0, leaf, leaf)
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> s(s(z))  ;  _my -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_lazgw_0, leaf, node(_hdzgw_0, leaf, leaf))
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 9, which took 0.021463 s (model generation: 0.020709,  model checking: 0.000754):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
numnodes(node(z, leaf, node(z, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(node(z, leaf, leaf), s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= height(node(z, leaf, leaf), z) /\ max(z, s(z), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(z, leaf, node(z, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
numnodes(node(z, leaf, node(z, leaf, node(z, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
}

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)) <= numnodes(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(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)
  numnodes(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


;
numnodes ->
[
numnodes : <nattree * 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)) <= numnodes(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(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)
  numnodes(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> s(_yfzgw_0)  ;  _fy -> s(_zfzgw_0)  ;  _gy -> s(_agzgw_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(_ajzgw_0)  ;  _ry -> z  ;  t1 -> leaf
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> z  ;  _my -> z  ;  t1 -> node(_mmzgw_0, _mmzgw_1, _mmzgw_2)  ;  t2 -> leaf
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 10, which took 0.078077 s (model generation: 0.077551,  model checking: 0.000526):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
numnodes(node(z, leaf, node(z, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(z, leaf, leaf), s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= height(node(z, leaf, leaf), z) /\ max(z, s(z), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(z, leaf, node(z, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(z, leaf, leaf), z)
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
numnodes(node(z, leaf, node(z, leaf, node(z, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
}

Current best model:
|_
name: None

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


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> s(z)  ;  _fy -> s(z)  ;  _gy -> s(s(_zrzgw_0))  ;  t1 -> node(_oozgw_0, leaf, _oozgw_2)  ;  t2 -> node(_pozgw_0, leaf, _pozgw_2)
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(z)  ;  _ry -> s(s(_crzgw_0))  ;  t1 -> node(_sozgw_0, leaf, _sozgw_2)
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> s(s(s(z)))  ;  _ly -> s(z)  ;  _my -> s(z)  ;  t1 -> node(_wqzgw_0, node(_xrzgw_0, node(_pszgw_0, leaf, _pszgw_2), _xrzgw_2), _wqzgw_2)  ;  t2 -> node(_xqzgw_0, leaf, _xqzgw_2)
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 11, which took 0.122481 s (model generation: 0.121846,  model checking: 0.000635):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
numnodes(node(z, leaf, node(z, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(z, leaf, leaf), s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= height(node(z, leaf, leaf), z) /\ max(z, s(z), s(s(z)))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(z, leaf, node(z, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
False <= numnodes(node(z, leaf, leaf), z)
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
numnodes(node(z, node(z, node(z, node(z, leaf, leaf), leaf), leaf), node(z, leaf, leaf)), s(s(z))) <= numnodes(node(z, node(z, node(z, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
numnodes(node(z, leaf, node(z, leaf, node(z, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
}

Current best model:
|_
name: None

height ->
[
height : <nattree * nat>
{
  _r_1(leaf, z) <= True
  _r_1(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_1(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0)
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(s(s(_xyzgw_0)))  ;  _ry -> s(s(z))  ;  t1 -> node(_quzgw_0, leaf, node(_nyzgw_0, _nyzgw_1, _nyzgw_2))
}

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> s(_rvzgw_0)  ;  _my -> s(_svzgw_0)  ;  t1 -> leaf  ;  t2 -> leaf
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 12, which took 0.105287 s (model generation: 0.104231,  model checking: 0.001056):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

Accumulated learning constraints:
{
height(leaf, z) <= True
height(node(z, leaf, leaf), s(z)) <= True
height(node(z, node(z, leaf, leaf), leaf), s(s(z))) <= True
leq(s(z), s(s(z))) <= True
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), s(z), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
numnodes(leaf, z) <= True
numnodes(node(z, leaf, leaf), s(z)) <= True
numnodes(node(z, leaf, node(z, leaf, leaf)), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= height(leaf, s(z))
False <= height(node(z, leaf, leaf), s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= height(node(z, leaf, leaf), z) /\ max(z, s(z), s(s(z)))
leq(s(s(s(z))), s(s(z))) <= height(node(z, leaf, node(z, leaf, leaf)), s(s(s(z))))
False <= height(node(z, leaf, node(z, leaf, leaf)), s(s(z))) /\ numnodes(node(z, leaf, node(z, leaf, leaf)), s(z))
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
max(z, s(s(z)), s(s(z))) <= leq(z, s(s(z)))
height(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z)))
height(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z))
height(node(z, leaf, node(z, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z)))
numnodes(node(z, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z))
False <= numnodes(node(z, leaf, leaf), z)
False <= numnodes(node(z, node(z, leaf, leaf), leaf), s(z))
numnodes(node(z, node(z, node(z, node(z, leaf, leaf), leaf), leaf), node(z, leaf, leaf)), s(s(z))) <= numnodes(node(z, node(z, node(z, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
numnodes(node(z, leaf, node(z, leaf, node(z, leaf, leaf))), s(s(z))) <= plus(z, s(s(z)), s(z))
}

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> s(z)  ;  _fy -> z  ;  _gy -> s(s(_gdahw_0))  ;  t1 -> node(_ozzgw_0, leaf, _ozzgw_2)  ;  t2 -> leaf
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> s(s(s(z)))  ;  _ly -> z  ;  _my -> s(z)  ;  t1 -> node(_ybahw_0, node(_ldahw_0, node(_ueahw_0, leaf, _ueahw_2), _ldahw_2), _ybahw_2)  ;  t2 -> leaf
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
Yes: {
_zx -> s(_icahw_0)  ;  mm -> z  ;  n -> s(s(_pcahw_0))
}


-------------------------------------------
Step 13, which took 0.123371 s (model generation: 0.122597,  model checking: 0.000774):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

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

Current best model:
|_
name: None

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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(z)  ;  _gy -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_lfahw_0, leaf, _lfahw_2)
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 14, which took 0.164076 s (model generation: 0.158800,  model checking: 0.005276):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(s(z))  ;  _gy -> s(s(s(_wechw_0)))  ;  t1 -> node(_wnahw_0, leaf, leaf)  ;  t2 -> node(_xnahw_0, leaf, node(_zdbhw_0, leaf, leaf))
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> s(z)  ;  _ly -> s(s(z))  ;  _my -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_aqahw_0, leaf, node(_lbbhw_0, leaf, leaf))
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 15, which took 0.231664 s (model generation: 0.227836,  model checking: 0.003828):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> z  ;  _fy -> s(s(z))  ;  _gy -> s(s(s(_tpdhw_0)))  ;  t1 -> leaf  ;  t2 -> node(_sfchw_0, leaf, node(_smchw_0, leaf, leaf))
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
Yes: {
_ky -> z  ;  _ly -> s(s(s(z)))  ;  _my -> s(s(z))  ;  t1 -> leaf  ;  t2 -> node(_skchw_0, leaf, node(_zrchw_0, leaf, node(_fzchw_0, leaf, leaf)))
}

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
Yes: {
_zx -> s(s(_ymchw_0))  ;  mm -> z  ;  n -> s(s(_xmchw_0))
}


-------------------------------------------
Step 16, which took 0.494620 s (model generation: 0.492669,  model checking: 0.001951):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <nattree * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, 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(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  numnodes(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 ->
[
leq : <nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, s(x_1_0)) <= True
  leq(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(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
}
]


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


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy)  :
Yes: {
_ey -> s(s(s(_vzdhw_0)))  ;  _fy -> z  ;  _gy -> s(z)  ;  t1 -> node(z, node(_jaehw_0, _jaehw_1, _jaehw_2), node(z, _czdhw_1, _czdhw_2))  ;  t2 -> leaf
}

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
No: ()

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

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

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

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

numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my)  :
No: ()

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


-------------------------------------------
Step 17, which took 1.282095 s (model generation: 0.420359,  model checking: 0.861736):

Clauses:
{
height(leaf, z) <= True -> 0
leq(n, m) \/ max(n, m, n) <= True -> 0
leq(z, n2) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
height(node(e, t1, t2), s(_gy)) <= height(t1, _ey) /\ height(t2, _fy) /\ max(_ey, _fy, _gy) -> 0
leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry) -> 0
max(n, m, m) <= leq(n, m) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
numnodes(node(e, t1, t2), s(_my)) <= numnodes(t1, _ky) /\ numnodes(t2, _ly) /\ plus(_ky, _ly, _my) -> 0
plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx) -> 0
}

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

Current best model:
|_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
}
]


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


;
numnodes ->
[
numnodes : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  numnodes(leaf, s(x_1_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


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



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




Answer of teacher:

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

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

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

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

plus(n, z, n) <= True  :
No: ()

leq(_qy, _ry) <= height(t1, _qy) /\ numnodes(t1, _ry)  :
Yes: {
_qy -> s(s(s(z)))  ;  _ry -> s(s(z))  ;  t1 -> node(_vdehw_0, leaf, node(_vmfhw_0, node(_rqfhw_0, _rqfhw_1, leaf), leaf))
}

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

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

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

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

plus(n, s(mm), s(_zx)) <= plus(n, mm, _zx)  :
No: ()


Total time: 3.049359
Learner time: 1.864354
Teacher time: 0.880143
Reasons for stopping: Yes: |_
name: None

height ->
[
height : <nattree * 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)
  height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0)
  height(node(x_0_0, x_0_1, x_0_2), z) <= True
}
]


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


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


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



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