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


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([_ww, _xw, _yw]) /\ max([_ww, _xw, _zw])) -> eq_nat([_yw, _zw])
)
(depth, F:
{() -> depth([leaf, z])
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)])}
(depth([_dx, _ex]) /\ depth([_dx, _fx])) -> eq_nat([_ex, _fx])
)
}

properties:
{(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx])}


over-approximation: {depth, max}
under-approximation: {leq}

Clause system for inference is:

{
() -> depth([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 0
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}


Solving took 60.000107 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6096, q_gen_6097, q_gen_6098, q_gen_6108, q_gen_6109, q_gen_6111, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6117, q_gen_6120, q_gen_6122, q_gen_6123, q_gen_6124, q_gen_6125, q_gen_6126, q_gen_6127, q_gen_6128, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6133, q_gen_6134, q_gen_6135, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6139, q_gen_6141, q_gen_6142, q_gen_6143, q_gen_6144, q_gen_6145, q_gen_6146, q_gen_6147, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6153, q_gen_6154, q_gen_6155, q_gen_6156, q_gen_6157, q_gen_6158, q_gen_6159, q_gen_6160, q_gen_6161, q_gen_6162, q_gen_6163, q_gen_6164, q_gen_6165, q_gen_6166, q_gen_6167, q_gen_6168, q_gen_6169, q_gen_6170, q_gen_6171, q_gen_6172, q_gen_6173, q_gen_6174, q_gen_6175, q_gen_6176},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6133
<node>(q_gen_6113, q_gen_6112, q_gen_6133) -> q_gen_6137
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6143
<node>(q_gen_6113, q_gen_6112, q_gen_6143) -> q_gen_6145
<node>(q_gen_6113, q_gen_6133, q_gen_6133) -> q_gen_6148
<node>(q_gen_6113, q_gen_6143, q_gen_6143) -> q_gen_6155
<node>(q_gen_6113, q_gen_6155, q_gen_6112) -> q_gen_6157
<node>(q_gen_6113, q_gen_6143, q_gen_6160) -> q_gen_6159
<node>(q_gen_6113, q_gen_6112, q_gen_6161) -> q_gen_6160
<node>(q_gen_6113, q_gen_6143, q_gen_6112) -> q_gen_6161
<node>(q_gen_6113, q_gen_6159, q_gen_6112) -> q_gen_6163
<node>(q_gen_6113, q_gen_6097, q_gen_6112) -> q_gen_6165
<node>(q_gen_6113, q_gen_6143, q_gen_6165) -> q_gen_6167
<node>(q_gen_6113, q_gen_6112, q_gen_6165) -> q_gen_6169
<node>(q_gen_6113, q_gen_6169, q_gen_6112) -> q_gen_6171
<node>(q_gen_6113, q_gen_6174, q_gen_6112) -> q_gen_6173
<node>(q_gen_6113, q_gen_6175, q_gen_6112) -> q_gen_6174
<node>(q_gen_6113, q_gen_6155, q_gen_6123) -> q_gen_6175
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6096
<b, z>() -> q_gen_6098
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6108
<a, z>() -> q_gen_6109
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6111
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6120
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6122
<a, s>(q_gen_6125) -> q_gen_6124
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6126
<b, s>(q_gen_6125) -> q_gen_6127
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6128
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6130
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6131
<node, s>(q_gen_6109, q_gen_6133, q_gen_6097) -> q_gen_6132
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6134
<node, s>(q_gen_6114, q_gen_6112, q_gen_6133) -> q_gen_6135
<node, s>(q_gen_6124, q_gen_6137, q_gen_6097) -> q_gen_6136
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6138
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6139
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6141
<node, s>(q_gen_6114, q_gen_6112, q_gen_6143) -> q_gen_6142
<node, s>(q_gen_6098, q_gen_6145, q_gen_6112) -> q_gen_6144
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6146
<node, s>(q_gen_6109, q_gen_6148, q_gen_6097) -> q_gen_6147
<node, s>(q_gen_6114, q_gen_6133, q_gen_6133) -> q_gen_6149
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6150
<node, s>(q_gen_6109, q_gen_6143, q_gen_6097) -> q_gen_6151
<node, s>(q_gen_6098, q_gen_6112, q_gen_6133) -> q_gen_6152
<node, s>(q_gen_6114, q_gen_6137, q_gen_6097) -> q_gen_6153
<node, s>(q_gen_6114, q_gen_6155, q_gen_6112) -> q_gen_6154
<node, s>(q_gen_6098, q_gen_6157, q_gen_6112) -> q_gen_6156
<node, s>(q_gen_6098, q_gen_6159, q_gen_6112) -> q_gen_6158
<node, s>(q_gen_6114, q_gen_6097, q_gen_6163) -> q_gen_6162
<node, s>(q_gen_6114, q_gen_6143, q_gen_6165) -> q_gen_6164
<node, s>(q_gen_6098, q_gen_6167, q_gen_6123) -> q_gen_6166
<node, s>(q_gen_6114, q_gen_6169, q_gen_6112) -> q_gen_6168
<node, s>(q_gen_6124, q_gen_6171, q_gen_6097) -> q_gen_6170
<node, s>(q_gen_6109, q_gen_6173, q_gen_6097) -> q_gen_6172
<node, s>(q_gen_6114, q_gen_6174, q_gen_6112) -> q_gen_6176
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6095, q_gen_6099, q_gen_6100, q_gen_6101, q_gen_6102, q_gen_6106, q_gen_6118, q_gen_6129},
Q_f={},
Delta=
{
<z>() -> q_gen_6100
<s>(q_gen_6100) -> q_gen_6102
<z, z>() -> q_gen_6092
<s, s>(q_gen_6092) -> q_gen_6095
<z, s>(q_gen_6100) -> q_gen_6099
<s, z>(q_gen_6102) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6106
<s, s>(q_gen_6106) -> q_gen_6118
<s, s>(q_gen_6118) -> q_gen_6129
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6103, q_gen_6104, q_gen_6105, q_gen_6107, q_gen_6110, q_gen_6119, q_gen_6121, q_gen_6140},
Q_f={},
Delta=
{
<s, s>(q_gen_6105) -> q_gen_6104
<z, z>() -> q_gen_6105
<z, z, z>() -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6103
<s, s, s>(q_gen_6093) -> q_gen_6107
<z, s, s>(q_gen_6105) -> q_gen_6110
<s, z, s>(q_gen_6105) -> q_gen_6119
<z, s, s>(q_gen_6104) -> q_gen_6121
<s, s, s>(q_gen_6119) -> q_gen_6140
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.018413 s (model generation: 0.018209,  model checking: 0.000204):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 0
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.009309 s (model generation: 0.009120,  model checking: 0.000189):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 0
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 1
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 2, which took 0.009521 s (model generation: 0.009444,  model checking: 0.000077):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 1
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: (() -> depth([leaf, z]), {

})

-------------------------------------------
Step 3, which took 0.010361 s (model generation: 0.010261,  model checking: 0.000100):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 1
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 4, which took 0.010373 s (model generation: 0.010285,  model checking: 0.000088):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 1
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.011088 s (model generation: 0.010941,  model checking: 0.000147):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 4
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> z  ;  _bx -> z  ;  _cx -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 6, which took 0.010943 s (model generation: 0.010774,  model checking: 0.000169):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 4
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> z  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 7, which took 0.010964 s (model generation: 0.009502,  model checking: 0.001462):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 4
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.011266 s (model generation: 0.011066,  model checking: 0.000200):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
}

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 4
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 9, which took 0.010161 s (model generation: 0.009358,  model checking: 0.000803):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 4
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.010841 s (model generation: 0.009863,  model checking: 0.000978):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 4
() -> leq([z, n2]) -> 4
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 7
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> z  ;  _bx -> z  ;  _cx -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.012904 s (model generation: 0.011898,  model checking: 0.001006):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 5
() -> leq([z, n2]) -> 5
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 7
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 6
(leq([n, m])) -> max([n, m, m]) -> 10
(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 -> 8
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.014482 s (model generation: 0.012606,  model checking: 0.001876):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 6
() -> leq([z, n2]) -> 6
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 10
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 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
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> z  ;  _bx -> s(z)  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 13, which took 0.013547 s (model generation: 0.012665,  model checking: 0.000882):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6113, q_gen_6115},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6097
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6098
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 10
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 10
(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
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 14, which took 0.014508 s (model generation: 0.013980,  model checking: 0.000528):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6113, q_gen_6115},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6097
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6098
<b, z>() -> q_gen_6098
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 8
() -> leq([z, n2]) -> 8
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 10
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 10
(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]) -> 11
(leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 15, which took 0.017657 s (model generation: 0.015784,  model checking: 0.001873):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6098
<b, z>() -> q_gen_6098
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 9
() -> leq([z, n2]) -> 9
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 13
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 11
(leq([n, m])) -> max([n, m, m]) -> 11
(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]) -> 11
(leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(z)  ;  _bx -> z  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.032509 s (model generation: 0.014187,  model checking: 0.018322):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 10
() -> leq([z, n2]) -> 10
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 16
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 12
(leq([n, m])) -> max([n, m, m]) -> 12
(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]) -> 12
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> z  ;  _bx -> s(s(z))  ;  _cx -> s(s(z))  ;  e -> a  ;  t1 -> leaf  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 17, which took 0.018137 s (model generation: 0.016768,  model checking: 0.001369):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<s>(q_gen_6115) -> q_gen_6115
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6115) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 11
() -> leq([z, n2]) -> 11
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 16
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 15
(leq([n, m])) -> max([n, m, m]) -> 13
(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]) -> 13
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(s(z)))  ;  _hx -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.025122 s (model generation: 0.022861,  model checking: 0.002261):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<s>(q_gen_6115) -> q_gen_6115
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6115) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 12
() -> leq([z, n2]) -> 12
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 16
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 18
(leq([n, m])) -> max([n, m, m]) -> 14
(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
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(s(z)))  ;  _hx -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 19, which took 0.033799 s (model generation: 0.027851,  model checking: 0.005948):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<s>(q_gen_6115) -> q_gen_6115
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<a, s>(q_gen_6115) -> q_gen_6114
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 13
() -> leq([z, n2]) -> 13
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 19
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 18
(leq([n, m])) -> max([n, m, m]) -> 15
(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]) -> 15
(leq([s(nn1), z])) -> BOT -> 14
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(s(z))  ;  _bx -> z  ;  _cx -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 20, which took 0.022374 s (model generation: 0.021700,  model checking: 0.000674):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<s>(q_gen_6115) -> q_gen_6115
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<a, s>(q_gen_6115) -> q_gen_6114
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101, q_gen_6118},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<s, s>(q_gen_6118) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, z>(q_gen_6100) -> q_gen_6101
<s, s>(q_gen_6101) -> q_gen_6118
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 14
() -> leq([z, n2]) -> 14
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 19
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 18
(leq([n, m])) -> max([n, m, m]) -> 15
(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]) -> 18
(leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 21, which took 0.023694 s (model generation: 0.020810,  model checking: 0.002884):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6125) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, s>(q_gen_6125) -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 15
() -> leq([z, n2]) -> 15
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 19
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 21
(leq([n, m])) -> max([n, m, m]) -> 16
(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]) -> 19
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> a  ;  t1 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 22, which took 0.026950 s (model generation: 0.026605,  model checking: 0.000345):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<s>(q_gen_6115) -> q_gen_6115
<z>() -> q_gen_6115
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6094
<a, s>(q_gen_6115) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6098
<b, z>() -> q_gen_6098
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6102, q_gen_6106},
Q_f={q_gen_6092},
Delta=
{
<z>() -> q_gen_6100
<s>(q_gen_6100) -> q_gen_6102
<s, s>(q_gen_6092) -> q_gen_6092
<s, z>(q_gen_6102) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6106) -> q_gen_6106
<s, z>(q_gen_6100) -> q_gen_6106
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6103, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6103
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 15
() -> leq([z, n2]) -> 15
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 19
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 21
(leq([n, m])) -> max([n, m, m]) -> 16
(not leq([n, m])) -> max([n, m, n]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 23, which took 0.038216 s (model generation: 0.026923,  model checking: 0.011293):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, s>(q_gen_6125) -> q_gen_6098
<b, z>() -> q_gen_6098
<a, s>(q_gen_6125) -> q_gen_6114
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 16
() -> leq([z, n2]) -> 16
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 22
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 21
(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]) -> 20
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(s(z))  ;  _bx -> z  ;  _cx -> s(s(z))  ;  e -> a  ;  t1 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)))  ;  t2 -> leaf
})

-------------------------------------------
Step 24, which took 0.032717 s (model generation: 0.029375,  model checking: 0.003342):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6125) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, s>(q_gen_6125) -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 17
() -> leq([z, n2]) -> 17
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 22
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 24
(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]) -> 21
(leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 25, which took 0.052909 s (model generation: 0.033783,  model checking: 0.019126):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125, q_gen_6127},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6125) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
<b, s>(q_gen_6125) -> q_gen_6127
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 18
() -> leq([z, n2]) -> 18
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 25
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 24
(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]) -> 22
(leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(z)  ;  _bx -> z  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 26, which took 0.038670 s (model generation: 0.034979,  model checking: 0.003691):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, s>(q_gen_6125) -> q_gen_6109
<a, z>() -> q_gen_6109
<b, s>(q_gen_6125) -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 19
() -> leq([z, n2]) -> 19
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 25
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 27
(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]) -> 23
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> a  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 27, which took 0.386158 s (model generation: 0.034346,  model checking: 0.351812):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125, q_gen_6127},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<a, s>(q_gen_6125) -> q_gen_6114
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6116
<b, s>(q_gen_6125) -> q_gen_6127
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 20
() -> leq([z, n2]) -> 20
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 28
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 27
(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]) -> 24
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(s(z))  ;  _bx -> s(z)  ;  _cx -> s(s(z))  ;  e -> a  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 28, which took 0.043944 s (model generation: 0.040317,  model checking: 0.003627):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125, q_gen_6127},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6125) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6116
<b, s>(q_gen_6125) -> q_gen_6127
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 21
() -> leq([z, n2]) -> 21
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 28
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 30
(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]) -> 25
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, leaf, leaf)))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 29, which took 0.069898 s (model generation: 0.046192,  model checking: 0.023706):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, z>() -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6109
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6123) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6117
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 22
() -> leq([z, n2]) -> 22
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 31
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 30
(leq([n, m])) -> max([n, m, m]) -> 23
(not leq([n, m])) -> max([n, m, n]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(s(z))  ;  _bx -> z  ;  _cx -> s(s(z))  ;  e -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 30, which took 0.063315 s (model generation: 0.052671,  model checking: 0.010644):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, z>() -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6109
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6123) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6112) -> q_gen_6117
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 23
() -> leq([z, n2]) -> 23
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 31
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 33
(leq([n, m])) -> max([n, m, m]) -> 24
(not leq([n, m])) -> max([n, m, n]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> a  ;  t1 -> node(b, node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)), node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)))  ;  t2 -> leaf
})

-------------------------------------------
Step 31, which took 0.966645 s (model generation: 0.054952,  model checking: 0.911693):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, z>() -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6109
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6112, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6123) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6112) -> q_gen_6117
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 24
() -> leq([z, n2]) -> 24
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 34
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 33
(leq([n, m])) -> max([n, m, m]) -> 25
(not leq([n, m])) -> max([n, m, n]) -> 27
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(z)  ;  _bx -> s(z)  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 32, which took 0.087794 s (model generation: 0.060480,  model checking: 0.027314):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, z>() -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6109
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6112, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6123) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6112) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6123) -> q_gen_6117
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 25
() -> leq([z, n2]) -> 25
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 34
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 36
(leq([n, m])) -> max([n, m, m]) -> 26
(not leq([n, m])) -> max([n, m, n]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> a  ;  t1 -> node(b, node(b, leaf, leaf), node(b, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 33, which took 0.115297 s (model generation: 0.070214,  model checking: 0.045083):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6109, q_gen_6112, q_gen_6113, q_gen_6115, q_gen_6117, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6109, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<b, z>() -> q_gen_6098
<a, z>() -> q_gen_6109
<b, s>(q_gen_6115) -> q_gen_6109
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6112, q_gen_6123) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6097) -> q_gen_6117
<node, s>(q_gen_6109, q_gen_6123, q_gen_6112) -> q_gen_6117
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 26
() -> leq([z, n2]) -> 26
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 37
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 36
(leq([n, m])) -> max([n, m, m]) -> 27
(not leq([n, m])) -> max([n, m, n]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(z)  ;  _bx -> z  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)))  ;  t2 -> leaf
})

-------------------------------------------
Step 34, which took 0.112388 s (model generation: 0.078277,  model checking: 0.034111):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125, q_gen_6127},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6094
<a, s>(q_gen_6125) -> q_gen_6098
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6116
<b, s>(q_gen_6125) -> q_gen_6127
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 27
() -> leq([z, n2]) -> 27
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 37
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 39
(leq([n, m])) -> max([n, m, m]) -> 28
(not leq([n, m])) -> max([n, m, n]) -> 30
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 28
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))), node(b, leaf, leaf))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 35, which took 0.205011 s (model generation: 0.087473,  model checking: 0.117538):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6125, q_gen_6127},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6123, q_gen_6112) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6123
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6127, q_gen_6123, q_gen_6097) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<a, s>(q_gen_6125) -> q_gen_6114
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6127, q_gen_6112, q_gen_6097) -> q_gen_6116
<b, s>(q_gen_6125) -> q_gen_6127
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 28
() -> leq([z, n2]) -> 28
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 40
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 39
(leq([n, m])) -> max([n, m, m]) -> 29
(not leq([n, m])) -> max([n, m, n]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 29
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> z  ;  _bx -> s(z)  ;  _cx -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, leaf)))), node(b, leaf, leaf))
})

-------------------------------------------
Step 36, which took 0.124762 s (model generation: 0.103733,  model checking: 0.021029):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6097, q_gen_6112) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6112) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6116
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 29
() -> leq([z, n2]) -> 29
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 40
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 42
(leq([n, m])) -> max([n, m, m]) -> 30
(not leq([n, m])) -> max([n, m, n]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 30
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf)))  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 37, which took 0.328731 s (model generation: 0.116286,  model checking: 0.212445):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6112) -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6123, q_gen_6097) -> q_gen_6097
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6112) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6116
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 30
() -> leq([z, n2]) -> 30
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 43
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 42
(leq([n, m])) -> max([n, m, m]) -> 31
(not leq([n, m])) -> max([n, m, n]) -> 33
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 31
}
Sat witness: Found: ((depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]), {
_ax -> s(s(z))  ;  _bx -> z  ;  _cx -> s(s(z))  ;  e -> a  ;  t1 -> node(b, node(b, node(b, leaf, leaf), node(b, leaf, node(b, leaf, leaf))), node(b, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 38, which took 0.186680 s (model generation: 0.138304,  model checking: 0.048376):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6094, q_gen_6097, q_gen_6098, q_gen_6112, q_gen_6113, q_gen_6114, q_gen_6115, q_gen_6116, q_gen_6123, q_gen_6124, q_gen_6125},
Q_f={q_gen_6094},
Delta=
{
<leaf>() -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6112) -> q_gen_6097
<node>(q_gen_6113, q_gen_6112, q_gen_6123) -> q_gen_6097
<node>(q_gen_6113, q_gen_6123, q_gen_6097) -> q_gen_6097
<node>(q_gen_6113, q_gen_6097, q_gen_6097) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6112) -> q_gen_6112
<node>(q_gen_6113, q_gen_6123, q_gen_6123) -> q_gen_6112
<b>() -> q_gen_6113
<z>() -> q_gen_6115
<node>(q_gen_6113, q_gen_6112, q_gen_6097) -> q_gen_6123
<node>(q_gen_6113, q_gen_6112, q_gen_6112) -> q_gen_6123
<s>(q_gen_6115) -> q_gen_6125
<leaf, z>() -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6098, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6112, q_gen_6112) -> q_gen_6094
<node, s>(q_gen_6114, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6097, q_gen_6123) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6097) -> q_gen_6094
<node, s>(q_gen_6124, q_gen_6123, q_gen_6112) -> q_gen_6094
<a, z>() -> q_gen_6098
<b, z>() -> q_gen_6098
<b, s>(q_gen_6115) -> q_gen_6114
<node, s>(q_gen_6098, q_gen_6097, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6112, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6123, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6098, q_gen_6123, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6097, q_gen_6097) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6112, q_gen_6123) -> q_gen_6116
<node, s>(q_gen_6114, q_gen_6123, q_gen_6112) -> q_gen_6116
<node, s>(q_gen_6124, q_gen_6112, q_gen_6097) -> q_gen_6116
<a, s>(q_gen_6125) -> q_gen_6124
<b, s>(q_gen_6125) -> q_gen_6124
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_6092, q_gen_6100, q_gen_6101},
Q_f={q_gen_6092},
Delta=
{
<s>(q_gen_6100) -> q_gen_6100
<z>() -> q_gen_6100
<s, s>(q_gen_6092) -> q_gen_6092
<z, s>(q_gen_6100) -> q_gen_6092
<z, z>() -> q_gen_6092
<s, s>(q_gen_6101) -> q_gen_6101
<s, z>(q_gen_6100) -> q_gen_6101
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  max -> 
{{{
Q={q_gen_6093, q_gen_6104},
Q_f={q_gen_6093},
Delta=
{
<s, s>(q_gen_6104) -> q_gen_6104
<z, z>() -> q_gen_6104
<s, s, s>(q_gen_6093) -> q_gen_6093
<s, z, s>(q_gen_6104) -> q_gen_6093
<z, s, s>(q_gen_6104) -> q_gen_6093
<z, z, z>() -> q_gen_6093
}

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

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 31
() -> leq([z, n2]) -> 31
(depth([t1, _ax]) /\ depth([t2, _bx]) /\ max([_ax, _bx, _cx])) -> depth([node(e, t1, t2), s(_cx)]) -> 43
(depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]) -> 45
(leq([n, m])) -> max([n, m, m]) -> 32
(not leq([n, m])) -> max([n, m, n]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35
(leq([s(nn1), z])) -> BOT -> 32
}
Sat witness: Found: ((depth([t1, _gx]) /\ depth([node(e, t1, t2), _hx])) -> leq([_gx, _hx]), {
_gx -> s(s(z))  ;  _hx -> s(z)  ;  e -> a  ;  t1 -> node(b, node(b, node(b, node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, node(b, leaf, leaf), node(b, leaf, leaf))), node(b, node(b, leaf, leaf), leaf)), node(b, leaf, leaf)), node(b, leaf, leaf))  ;  t2 -> leaf
})

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