Solving ../../benchmarks/true/tree_depth_leq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


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([_bn, _cn, _dn]) /\ max([_bn, _cn, _en])) -> eq_nat([_dn, _en])
)
(depth, F:
{() -> depth([leaf, z])
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)])}
(depth([_in, _jn]) /\ depth([_in, _kn])) -> eq_nat([_jn, _kn])
)
}

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


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

Clause system for inference is:

{
() -> depth([leaf, z]) -> 0  ;  () -> leq([z, n2]) -> 0  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 0  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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 30.177793 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
depth -> 
{{{
Q={q_gen_6790, q_gen_6792, q_gen_6793, q_gen_6802, q_gen_6803, q_gen_6808, q_gen_6809, q_gen_6810, q_gen_6811, q_gen_6812, q_gen_6813, q_gen_6814, q_gen_6816, q_gen_6817, q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6821},
Q_f={},
Delta=
{
<z>() -> q_gen_6810
<s>(q_gen_6810) -> q_gen_6818
<s>(q_gen_6818) -> q_gen_6821
<leaf, z>() -> q_gen_6790
<node, s>(q_gen_6793, q_gen_6790, q_gen_6790) -> q_gen_6792
<b, z>() -> q_gen_6793
<node, s>(q_gen_6803, q_gen_6790, q_gen_6790) -> q_gen_6802
<a, z>() -> q_gen_6803
<node, s>(q_gen_6811, q_gen_6809, q_gen_6792) -> q_gen_6808
<leaf, s>(q_gen_6810) -> q_gen_6809
<b, s>(q_gen_6810) -> q_gen_6811
<node, s>(q_gen_6813, q_gen_6809, q_gen_6809) -> q_gen_6812
<a, s>(q_gen_6810) -> q_gen_6813
<node, s>(q_gen_6811, q_gen_6809, q_gen_6809) -> q_gen_6814
<node, s>(q_gen_6819, q_gen_6817, q_gen_6814) -> q_gen_6816
<leaf, s>(q_gen_6818) -> q_gen_6817
<b, s>(q_gen_6818) -> q_gen_6819
<leaf, s>(q_gen_6821) -> q_gen_6820
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6791, q_gen_6794, q_gen_6795, q_gen_6796, q_gen_6799, q_gen_6800, q_gen_6804, q_gen_6822, q_gen_6823},
Q_f={},
Delta=
{
<z>() -> q_gen_6795
<s>(q_gen_6795) -> q_gen_6800
<z, z>() -> q_gen_6788
<s, s>(q_gen_6788) -> q_gen_6791
<z, s>(q_gen_6795) -> q_gen_6794
<s, z>(q_gen_6795) -> q_gen_6796
<z, s>(q_gen_6800) -> q_gen_6799
<s, z>(q_gen_6800) -> q_gen_6804
<s, s>(q_gen_6823) -> q_gen_6822
<s, s>(q_gen_6796) -> q_gen_6823
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6797, q_gen_6798, q_gen_6801, q_gen_6805, q_gen_6806, q_gen_6807, q_gen_6815},
Q_f={},
Delta=
{
<z, z>() -> q_gen_6798
<s, s>(q_gen_6798) -> q_gen_6806
<z, z, z>() -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6797
<s, s, s>(q_gen_6789) -> q_gen_6801
<s, z, s>(q_gen_6806) -> q_gen_6805
<z, s, s>(q_gen_6798) -> q_gen_6807
<z, s, s>(q_gen_6806) -> q_gen_6815
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003559 s (model generation: 0.003412,  model checking: 0.000147):

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

}

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

}

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

}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 0  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.003520 s (model generation: 0.003404,  model checking: 0.000116):

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

}

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 1  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 2, which took 0.003518 s (model generation: 0.003470,  model checking: 0.000048):

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

}

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 1  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: (() -> depth([leaf, z]), {

})

-------------------------------------------
Step 3, which took 0.004089 s (model generation: 0.003999,  model checking: 0.000090):

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

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 1  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 4, which took 0.004072 s (model generation: 0.004004,  model checking: 0.000068):

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

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 1  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.003873 s (model generation: 0.003708,  model checking: 0.000165):

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

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> z  ;  _gn -> z  ;  _hn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 6, which took 0.003717 s (model generation: 0.003608,  model checking: 0.000109):

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

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> z  ;  _mn -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 7, which took 0.004068 s (model generation: 0.003873,  model checking: 0.000195):

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

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

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

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 8, which took 0.004005 s (model generation: 0.003957,  model checking: 0.000048):

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

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<z, z>() -> q_gen_6798
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 6  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.004011 s (model generation: 0.003933,  model checking: 0.000078):

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

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<z, z>() -> q_gen_6798
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 6  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 10, which took 0.004262 s (model generation: 0.004054,  model checking: 0.000208):

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<z, z>() -> q_gen_6798
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 6  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 4  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.004537 s (model generation: 0.003958,  model checking: 0.000579):

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 6  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 7  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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: Yes: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> z  ;  _gn -> z  ;  _hn -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 12, which took 0.004527 s (model generation: 0.004143,  model checking: 0.000384):

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 6  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 7  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 6  ;  (leq([n, m])) -> max([n, m, m]) -> 7  ;  (not leq([n, m])) -> max([n, m, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6  ;  (leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.005583 s (model generation: 0.004959,  model checking: 0.000624):

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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]) -> 7  ;  (depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 7  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 7  ;  (leq([n, m])) -> max([n, m, m]) -> 10  ;  (not leq([n, m])) -> max([n, m, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7  ;  (leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 14, which took 0.009868 s (model generation: 0.007927,  model checking: 0.001941):

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, s, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 10  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 8  ;  (leq([n, m])) -> max([n, m, m]) -> 10  ;  (not leq([n, m])) -> max([n, m, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8  ;  (leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> z  ;  _gn -> s(z)  ;  _hn -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 15, which took 0.010813 s (model generation: 0.008392,  model checking: 0.002421):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6790, q_gen_6793, q_gen_6810},
Q_f={q_gen_6790},
Delta=
{
<z>() -> q_gen_6810
<leaf, s>(q_gen_6810) -> q_gen_6790
<leaf, z>() -> q_gen_6790
<node, s>(q_gen_6793, q_gen_6790, q_gen_6790) -> q_gen_6790
<a, z>() -> q_gen_6793
<b, s>(q_gen_6810) -> q_gen_6793
<b, z>() -> q_gen_6793
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, s, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 13  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 9  ;  (leq([n, m])) -> max([n, m, m]) -> 11  ;  (not leq([n, m])) -> max([n, m, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9  ;  (leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Yes: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> z  ;  _gn -> s(z)  ;  _hn -> s(z)  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.018645 s (model generation: 0.008039,  model checking: 0.010606):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6790, q_gen_6793, q_gen_6810},
Q_f={q_gen_6790},
Delta=
{
<z>() -> q_gen_6810
<leaf, s>(q_gen_6810) -> q_gen_6790
<leaf, z>() -> q_gen_6790
<node, s>(q_gen_6793, q_gen_6790, q_gen_6790) -> q_gen_6790
<a, s>(q_gen_6810) -> q_gen_6793
<a, z>() -> q_gen_6793
<b, s>(q_gen_6810) -> q_gen_6793
<b, z>() -> q_gen_6793
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, s, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 16  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 10  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Yes: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> z  ;  _gn -> s(s(z))  ;  _hn -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 17, which took 0.010041 s (model generation: 0.009192,  model checking: 0.000849):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6790, q_gen_6793, q_gen_6810},
Q_f={q_gen_6790},
Delta=
{
<s>(q_gen_6810) -> q_gen_6810
<z>() -> q_gen_6810
<leaf, s>(q_gen_6810) -> q_gen_6790
<leaf, z>() -> q_gen_6790
<node, s>(q_gen_6793, q_gen_6790, q_gen_6790) -> q_gen_6790
<a, s>(q_gen_6810) -> q_gen_6793
<a, z>() -> q_gen_6793
<b, s>(q_gen_6810) -> q_gen_6793
<b, z>() -> q_gen_6793
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, s, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 16  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 13  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.013135 s (model generation: 0.013008,  model checking: 0.000127):

Model:
|_
{
depth -> 
{{{
Q={q_gen_6790, q_gen_6793, q_gen_6810},
Q_f={q_gen_6790},
Delta=
{
<s>(q_gen_6810) -> q_gen_6810
<z>() -> q_gen_6810
<leaf, s>(q_gen_6810) -> q_gen_6790
<leaf, z>() -> q_gen_6790
<node, s>(q_gen_6793, q_gen_6790, q_gen_6790) -> q_gen_6790
<a, s>(q_gen_6810) -> q_gen_6793
<a, z>() -> q_gen_6793
<b, s>(q_gen_6810) -> q_gen_6793
<b, z>() -> q_gen_6793
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6788, q_gen_6795, q_gen_6796},
Q_f={q_gen_6788},
Delta=
{
<s>(q_gen_6795) -> q_gen_6795
<z>() -> q_gen_6795
<s, s>(q_gen_6788) -> q_gen_6788
<s, s>(q_gen_6796) -> q_gen_6788
<z, s>(q_gen_6795) -> q_gen_6788
<z, z>() -> q_gen_6788
<s, z>(q_gen_6795) -> q_gen_6796
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6789, q_gen_6798},
Q_f={q_gen_6789},
Delta=
{
<s, s>(q_gen_6798) -> q_gen_6798
<z, z>() -> q_gen_6798
<s, s, s>(q_gen_6789) -> q_gen_6789
<s, z, s>(q_gen_6798) -> q_gen_6789
<z, s, s>(q_gen_6798) -> q_gen_6789
<z, z, z>() -> q_gen_6789
}

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

}
--
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, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 16  ;  (depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 13  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14  ;  (leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

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