Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, n2])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(max, F:
{(leq([n, m])) -> max([n, m, m])
(not leq([n, m])) -> max([n, m, n])}
(max([_sz, _tz, _uz]) /\ max([_sz, _tz, _vz])) -> eq_nat([_uz, _vz])
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)])}
(plus([_xz, _yz, _aaa]) /\ plus([_xz, _yz, _zz])) -> eq_nat([_zz, _aaa])
)
(height, F:
{() -> height([leaf, z])
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)])}
(height([_eaa, _faa]) /\ height([_eaa, _gaa])) -> eq_nat([_faa, _gaa])
)
}

properties:
{(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa])}


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

Clause system for inference is:

{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> plus([n, z, n]) -> 0
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 0
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 0
(leq([n, m])) -> max([n, m, m]) -> 0
(not leq([n, m])) -> max([n, m, n]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 0
}


Solving took 60.000076 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5208, q_gen_5209, q_gen_5214, q_gen_5215, q_gen_5216, q_gen_5217, q_gen_5222, q_gen_5223, q_gen_5224, q_gen_5225, q_gen_5226, q_gen_5228, q_gen_5229, q_gen_5231, q_gen_5232, q_gen_5237, q_gen_5238, q_gen_5239, q_gen_5240, q_gen_5242, q_gen_5243, q_gen_5244, q_gen_5245, q_gen_5246, q_gen_5247, q_gen_5248, q_gen_5249, q_gen_5251, q_gen_5252, q_gen_5253, q_gen_5254, q_gen_5255, q_gen_5256, q_gen_5257, q_gen_5258, q_gen_5259},
Q_f={},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<a>() -> q_gen_5209
<z>() -> q_gen_5216
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5217
<s>(q_gen_5216) -> q_gen_5225
<node>(q_gen_5209, q_gen_5191, q_gen_5191) -> q_gen_5226
<node>(q_gen_5192, q_gen_5217, q_gen_5191) -> q_gen_5232
<s>(q_gen_5225) -> q_gen_5240
<node>(q_gen_5209, q_gen_5217, q_gen_5191) -> q_gen_5246
<node>(q_gen_5192, q_gen_5191, q_gen_5226) -> q_gen_5255
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5190
<node, s>(q_gen_5209, q_gen_5191, q_gen_5186) -> q_gen_5208
<node, s>(q_gen_5192, q_gen_5217, q_gen_5215) -> q_gen_5214
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5209, q_gen_5191, q_gen_5215) -> q_gen_5222
<node, s>(q_gen_5192, q_gen_5226, q_gen_5224) -> q_gen_5223
<leaf, s>(q_gen_5225) -> q_gen_5224
<node, s>(q_gen_5192, q_gen_5191, q_gen_5224) -> q_gen_5228
<node, s>(q_gen_5192, q_gen_5191, q_gen_5190) -> q_gen_5229
<node, s>(q_gen_5192, q_gen_5232, q_gen_5224) -> q_gen_5231
<node, s>(q_gen_5192, q_gen_5191, q_gen_5214) -> q_gen_5237
<node, s>(q_gen_5192, q_gen_5217, q_gen_5239) -> q_gen_5238
<leaf, s>(q_gen_5240) -> q_gen_5239
<node, s>(q_gen_5192, q_gen_5226, q_gen_5190) -> q_gen_5242
<node, s>(q_gen_5209, q_gen_5217, q_gen_5215) -> q_gen_5243
<node, s>(q_gen_5209, q_gen_5217, q_gen_5186) -> q_gen_5244
<node, s>(q_gen_5192, q_gen_5246, q_gen_5244) -> q_gen_5245
<node, s>(q_gen_5192, q_gen_5217, q_gen_5224) -> q_gen_5247
<node, s>(q_gen_5192, q_gen_5217, q_gen_5249) -> q_gen_5248
<node, s>(q_gen_5192, q_gen_5217, q_gen_5186) -> q_gen_5249
<node, s>(q_gen_5192, q_gen_5226, q_gen_5222) -> q_gen_5251
<node, s>(q_gen_5192, q_gen_5191, q_gen_5253) -> q_gen_5252
<node, s>(q_gen_5192, q_gen_5255, q_gen_5254) -> q_gen_5253
<node, s>(q_gen_5209, q_gen_5255, q_gen_5186) -> q_gen_5254
<node, s>(q_gen_5192, q_gen_5255, q_gen_5257) -> q_gen_5256
<node, s>(q_gen_5209, q_gen_5255, q_gen_5224) -> q_gen_5257
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5258
<node, s>(q_gen_5192, q_gen_5217, q_gen_5190) -> q_gen_5259
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5189, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5206, q_gen_5227, q_gen_5230, q_gen_5241},
Q_f={},
Delta=
{
<z>() -> q_gen_5194
<s>(q_gen_5194) -> q_gen_5196
<z, z>() -> q_gen_5183
<s, s>(q_gen_5183) -> q_gen_5189
<z, s>(q_gen_5194) -> q_gen_5193
<s, z>(q_gen_5196) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5206
<s, s>(q_gen_5206) -> q_gen_5227
<s, s>(q_gen_5227) -> q_gen_5230
<s, s>(q_gen_5230) -> q_gen_5241
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5197, q_gen_5198, q_gen_5199, q_gen_5207, q_gen_5212, q_gen_5213, q_gen_5233, q_gen_5234, q_gen_5235, q_gen_5236, q_gen_5250},
Q_f={},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5199) -> q_gen_5198
<z, z>() -> q_gen_5199
<z, z, z>() -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5197
<s, s, s>(q_gen_5184) -> q_gen_5207
<z, s, s>(q_gen_5199) -> q_gen_5212
<s, z, s>(q_gen_5199) -> q_gen_5213
<s, s, s>(q_gen_5234) -> q_gen_5233
<s, s, s>(q_gen_5235) -> q_gen_5234
<s, z, z>(q_gen_5236) -> q_gen_5235
<s, s, s>(q_gen_5213) -> q_gen_5250
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5187, q_gen_5188, q_gen_5200, q_gen_5201, q_gen_5202, q_gen_5203, q_gen_5204, q_gen_5205, q_gen_5210, q_gen_5211, q_gen_5218, q_gen_5219, q_gen_5220, q_gen_5221},
Q_f={},
Delta=
{
<z>() -> q_gen_5205
<s>(q_gen_5205) -> q_gen_5221
<z, z>() -> q_gen_5188
<s, s>(q_gen_5188) -> q_gen_5201
<z, s>(q_gen_5205) -> q_gen_5211
<z, z, z>() -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5187
<s, z, s>(q_gen_5201) -> q_gen_5200
<s, z, s>(q_gen_5188) -> q_gen_5202
<s, s, s>(q_gen_5204) -> q_gen_5203
<z, z, s>(q_gen_5205) -> q_gen_5204
<z, s, s>(q_gen_5211) -> q_gen_5210
<s, z, s>(q_gen_5211) -> q_gen_5218
<s, s, s>(q_gen_5220) -> q_gen_5219
<z, z, s>(q_gen_5221) -> q_gen_5220
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006041 s (model generation: 0.005471,  model checking: 0.000570):

Model:
|_
{
height -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> plus([n, z, n]) -> 0
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 0
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 0
(leq([n, m])) -> max([n, m, m]) -> 0
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.005855 s (model generation: 0.005385,  model checking: 0.000470):

Model:
|_
{
height -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={},
Delta=
{
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={q_gen_5184},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 1
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.004895 s (model generation: 0.004797,  model checking: 0.000098):

Model:
|_
{
height -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={},
Delta=
{
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={q_gen_5184},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185},
Q_f={q_gen_5185},
Delta=
{
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 1
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 3, which took 0.005456 s (model generation: 0.005291,  model checking: 0.000165):

Model:
|_
{
height -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185},
Q_f={q_gen_5185},
Delta=
{
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 1
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Found: (() -> height([leaf, z]), {

})

-------------------------------------------
Step 4, which took 0.005090 s (model generation: 0.004820,  model checking: 0.000270):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186},
Q_f={q_gen_5186},
Delta=
{
<leaf, z>() -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185},
Q_f={q_gen_5185},
Delta=
{
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 1
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.004841 s (model generation: 0.004536,  model checking: 0.000305):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186},
Q_f={q_gen_5186},
Delta=
{
<leaf, z>() -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 1
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.005873 s (model generation: 0.005695,  model checking: 0.000178):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186},
Q_f={q_gen_5186},
Delta=
{
<leaf, z>() -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<s, s>(q_gen_5183) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 7, which took 0.005495 s (model generation: 0.004339,  model checking: 0.001156):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186},
Q_f={q_gen_5186},
Delta=
{
<leaf, z>() -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<s, s>(q_gen_5183) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={q_gen_5184},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 2
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> z  ;  _daa -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 8, which took 0.006362 s (model generation: 0.005904,  model checking: 0.000458):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183},
Q_f={q_gen_5183},
Delta=
{
<s, s>(q_gen_5183) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={q_gen_5184},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> z  ;  _iaa -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.005175 s (model generation: 0.004889,  model checking: 0.000286):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194},
Q_f={q_gen_5183},
Delta=
{
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184},
Q_f={q_gen_5184},
Delta=
{
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 10, which took 0.005323 s (model generation: 0.005115,  model checking: 0.000208):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<z, z>() -> q_gen_5188
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> plus([n, z, n]) -> 6
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 11, which took 0.006628 s (model generation: 0.006416,  model checking: 0.000212):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188},
Q_f={q_gen_5185},
Delta=
{
<s, s>(q_gen_5188) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 12, which took 0.006533 s (model generation: 0.006509,  model checking: 0.000024):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 4
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 7
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 13, which took 0.006196 s (model generation: 0.005671,  model checking: 0.000525):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 7
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 7
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 14, which took 0.007494 s (model generation: 0.006472,  model checking: 0.001022):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5
(leq([n, m])) -> max([n, m, m]) -> 7
(not leq([n, m])) -> max([n, m, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 7
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> z  ;  _daa -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 15, which took 0.007587 s (model generation: 0.006873,  model checking: 0.000714):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 5
() -> leq([z, n2]) -> 5
() -> plus([n, z, n]) -> 7
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 6
(leq([n, m])) -> max([n, m, m]) -> 7
(not leq([n, m])) -> max([n, m, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 7
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 16, which took 0.008224 s (model generation: 0.007276,  model checking: 0.000948):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 6
() -> leq([z, n2]) -> 6
() -> plus([n, z, n]) -> 7
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 7
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 8
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 17, which took 0.008722 s (model generation: 0.007074,  model checking: 0.001648):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
() -> plus([n, z, n]) -> 7
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 10
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 8
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(z)  ;  _caa -> z  ;  _daa -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.008811 s (model generation: 0.007489,  model checking: 0.001322):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<z>() -> q_gen_5216
<leaf, s>(q_gen_5216) -> q_gen_5186
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 8
() -> leq([z, n2]) -> 8
() -> plus([n, z, n]) -> 8
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 10
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 9
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 19, which took 0.010461 s (model generation: 0.008591,  model checking: 0.001870):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<z>() -> q_gen_5216
<leaf, s>(q_gen_5216) -> q_gen_5186
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 9
() -> leq([z, n2]) -> 9
() -> plus([n, z, n]) -> 9
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 13
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 10
(leq([n, m])) -> max([n, m, m]) -> 11
(not leq([n, m])) -> max([n, m, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> z  ;  _daa -> s(s(z))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 20, which took 0.009574 s (model generation: 0.008620,  model checking: 0.000954):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, s>(q_gen_5216) -> q_gen_5186
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 10
() -> leq([z, n2]) -> 10
() -> plus([n, z, n]) -> 10
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 13
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 13
(leq([n, m])) -> max([n, m, m]) -> 11
(not leq([n, m])) -> max([n, m, n]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(z))  ;  _iaa -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 21, which took 0.009400 s (model generation: 0.008658,  model checking: 0.000742):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, s>(q_gen_5216) -> q_gen_5186
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 11
() -> leq([z, n2]) -> 11
() -> plus([n, z, n]) -> 11
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 13
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 13
(leq([n, m])) -> max([n, m, m]) -> 11
(not leq([n, m])) -> max([n, m, n]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 12
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 22, which took 0.012126 s (model generation: 0.010357,  model checking: 0.001769):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 12
() -> leq([z, n2]) -> 12
() -> plus([n, z, n]) -> 12
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 13
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 12
(not leq([n, m])) -> max([n, m, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 13
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(s(z)))  ;  _iaa -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 23, which took 0.017210 s (model generation: 0.010893,  model checking: 0.006317):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216, q_gen_5217},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5217
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5217, q_gen_5215) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 13
() -> leq([z, n2]) -> 13
() -> plus([n, z, n]) -> 13
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 13
(not leq([n, m])) -> max([n, m, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> z  ;  _daa -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 24, which took 0.012451 s (model generation: 0.011937,  model checking: 0.000514):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195, q_gen_5227},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, s>(q_gen_5227) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
<s, s>(q_gen_5195) -> q_gen_5227
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198},
Q_f={q_gen_5184},
Delta=
{
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 13
() -> leq([z, n2]) -> 13
() -> plus([n, z, n]) -> 13
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 16
(not leq([n, m])) -> max([n, m, n]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 25, which took 0.012394 s (model generation: 0.011798,  model checking: 0.000596):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195, q_gen_5227},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<s, s>(q_gen_5227) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, z>(q_gen_5194) -> q_gen_5195
<s, s>(q_gen_5195) -> q_gen_5227
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 14
() -> leq([z, n2]) -> 14
() -> plus([n, z, n]) -> 14
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 16
(not leq([n, m])) -> max([n, m, n]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 15
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 15
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 26, which took 0.013972 s (model generation: 0.012070,  model checking: 0.001902):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216, q_gen_5217},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5217
<node>(q_gen_5192, q_gen_5217, q_gen_5191) -> q_gen_5217
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5217, q_gen_5215) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 15
() -> leq([z, n2]) -> 15
() -> plus([n, z, n]) -> 15
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 19
(leq([n, m])) -> max([n, m, m]) -> 17
(not leq([n, m])) -> max([n, m, n]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 16
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 16
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(s(s(z))))  ;  _iaa -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 27, which took 0.021590 s (model generation: 0.013926,  model checking: 0.007664):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186, q_gen_5190},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5190
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5190
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5190) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 16
() -> leq([z, n2]) -> 16
() -> plus([n, z, n]) -> 16
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 19
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 19
(leq([n, m])) -> max([n, m, m]) -> 17
(not leq([n, m])) -> max([n, m, n]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 17
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> s(z)  ;  _daa -> s(z)  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 28, which took 0.015589 s (model generation: 0.015408,  model checking: 0.000181):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5214, q_gen_5216},
Q_f={q_gen_5186},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<leaf, s>(q_gen_5216) -> q_gen_5214
<node, s>(q_gen_5192, q_gen_5191, q_gen_5214) -> q_gen_5214
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5199, q_gen_5213, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5199) -> q_gen_5198
<z, z>() -> q_gen_5199
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5199) -> q_gen_5184
<z, z, z>() -> q_gen_5184
<s, s, s>(q_gen_5213) -> q_gen_5213
<s, z, s>(q_gen_5199) -> q_gen_5213
<s, z, z>(q_gen_5236) -> q_gen_5213
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 16
() -> leq([z, n2]) -> 16
() -> plus([n, z, n]) -> 16
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 19
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 19
(leq([n, m])) -> max([n, m, m]) -> 17
(not leq([n, m])) -> max([n, m, n]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 17
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 29, which took 0.071852 s (model generation: 0.017171,  model checking: 0.054681):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5214, q_gen_5215, q_gen_5216, q_gen_5217},
Q_f={q_gen_5186, q_gen_5214},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5217
<node>(q_gen_5192, q_gen_5217, q_gen_5191) -> q_gen_5217
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5217, q_gen_5186) -> q_gen_5214
<node, s>(q_gen_5192, q_gen_5217, q_gen_5215) -> q_gen_5214
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5214) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 17
() -> leq([z, n2]) -> 17
() -> plus([n, z, n]) -> 17
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 22
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 20
(leq([n, m])) -> max([n, m, m]) -> 18
(not leq([n, m])) -> max([n, m, n]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(leq([s(nn1), z])) -> BOT -> 18
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 18
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> s(z)  ;  _daa -> s(z)  ;  e -> b  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> node(a, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 30, which took 0.023316 s (model generation: 0.020058,  model checking: 0.003258):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5191, q_gen_5192, q_gen_5214, q_gen_5215, q_gen_5216, q_gen_5217},
Q_f={q_gen_5186, q_gen_5214},
Delta=
{
<leaf>() -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5217
<node>(q_gen_5192, q_gen_5217, q_gen_5191) -> q_gen_5217
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5217, q_gen_5215) -> q_gen_5214
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5214) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5217, q_gen_5186) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 18
() -> leq([z, n2]) -> 18
() -> plus([n, z, n]) -> 18
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 22
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 23
(leq([n, m])) -> max([n, m, m]) -> 19
(not leq([n, m])) -> max([n, m, n]) -> 21
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 19
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(s(z)))  ;  _iaa -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 31, which took 0.027873 s (model generation: 0.024467,  model checking: 0.003406):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186, q_gen_5190},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<a>() -> q_gen_5192
<b>() -> q_gen_5192
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5190
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5190
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5190) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5233, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
<s, s, s>(q_gen_5233) -> q_gen_5233
<s, z, z>(q_gen_5236) -> q_gen_5233
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 19
() -> leq([z, n2]) -> 19
() -> plus([n, z, n]) -> 19
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 25
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 23
(leq([n, m])) -> max([n, m, m]) -> 20
(not leq([n, m])) -> max([n, m, n]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20
(leq([s(nn1), z])) -> BOT -> 20
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 20
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> s(z)  ;  _daa -> s(s(z))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 32, which took 0.028195 s (model generation: 0.024991,  model checking: 0.003204):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5209, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186, q_gen_5190},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<node>(q_gen_5209, q_gen_5191, q_gen_5191) -> q_gen_5191
<b>() -> q_gen_5192
<a>() -> q_gen_5209
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5190
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5190
<node, s>(q_gen_5209, q_gen_5191, q_gen_5186) -> q_gen_5190
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5190) -> q_gen_5215
<node, s>(q_gen_5209, q_gen_5191, q_gen_5215) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 20
() -> leq([z, n2]) -> 20
() -> plus([n, z, n]) -> 20
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 25
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 26
(leq([n, m])) -> max([n, m, m]) -> 21
(not leq([n, m])) -> max([n, m, n]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 21
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 21
}
Sat witness: Found: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(s(s(z))))  ;  _iaa -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, node(a, leaf, leaf)), node(a, node(b, leaf, node(a, leaf, leaf)), leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 33, which took 0.051417 s (model generation: 0.033182,  model checking: 0.018235):

Model:
|_
{
height -> 
{{{
Q={q_gen_5186, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5209, q_gen_5215, q_gen_5216},
Q_f={q_gen_5186, q_gen_5190},
Delta=
{
<leaf>() -> q_gen_5191
<node>(q_gen_5192, q_gen_5191, q_gen_5191) -> q_gen_5191
<node>(q_gen_5209, q_gen_5191, q_gen_5191) -> q_gen_5191
<b>() -> q_gen_5192
<a>() -> q_gen_5209
<s>(q_gen_5216) -> q_gen_5216
<z>() -> q_gen_5216
<leaf, z>() -> q_gen_5186
<node, s>(q_gen_5209, q_gen_5191, q_gen_5186) -> q_gen_5186
<node, s>(q_gen_5192, q_gen_5191, q_gen_5186) -> q_gen_5190
<node, s>(q_gen_5192, q_gen_5191, q_gen_5215) -> q_gen_5190
<leaf, s>(q_gen_5216) -> q_gen_5215
<node, s>(q_gen_5192, q_gen_5191, q_gen_5190) -> q_gen_5215
<node, s>(q_gen_5209, q_gen_5191, q_gen_5215) -> q_gen_5215
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_5183, q_gen_5194, q_gen_5195},
Q_f={q_gen_5183},
Delta=
{
<s>(q_gen_5194) -> q_gen_5194
<z>() -> q_gen_5194
<s, s>(q_gen_5183) -> q_gen_5183
<z, s>(q_gen_5194) -> q_gen_5183
<z, z>() -> q_gen_5183
<s, s>(q_gen_5195) -> q_gen_5195
<s, z>(q_gen_5194) -> q_gen_5195
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_5184, q_gen_5198, q_gen_5236},
Q_f={q_gen_5184},
Delta=
{
<z>() -> q_gen_5236
<s, s>(q_gen_5198) -> q_gen_5198
<z, z>() -> q_gen_5198
<s, s, s>(q_gen_5184) -> q_gen_5184
<s, z, s>(q_gen_5198) -> q_gen_5184
<s, z, z>(q_gen_5236) -> q_gen_5184
<z, s, s>(q_gen_5198) -> q_gen_5184
<z, z, z>() -> q_gen_5184
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5185, q_gen_5188, q_gen_5205},
Q_f={q_gen_5185},
Delta=
{
<s>(q_gen_5205) -> q_gen_5205
<z>() -> q_gen_5205
<s, s>(q_gen_5188) -> q_gen_5188
<z, s>(q_gen_5205) -> q_gen_5188
<z, z>() -> q_gen_5188
<s, s, s>(q_gen_5185) -> q_gen_5185
<s, z, s>(q_gen_5188) -> q_gen_5185
<z, s, s>(q_gen_5188) -> q_gen_5185
<z, z, s>(q_gen_5205) -> q_gen_5185
<z, z, z>() -> q_gen_5185
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 21
() -> leq([z, n2]) -> 21
() -> plus([n, z, n]) -> 21
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 28
(height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 26
(leq([n, m])) -> max([n, m, m]) -> 22
(not leq([n, m])) -> max([n, m, n]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 22
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 22
}
Sat witness: Found: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> s(s(z))  ;  _caa -> s(z)  ;  _daa -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

Total time: 60.000076
Reason for stopping: DontKnow. Stopped because: timeout