Solving ../../benchmarks/true/tree_height_subtree.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([_sz, _tz, _uz]) /\ max([_sz, _tz, _vz])) -> eq_nat([_uz, _vz])
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)])}
(plus([_xz, _yz, _aaa]) /\ plus([_xz, _yz, _zz])) -> eq_nat([_zz, _aaa])
)
(height, F:
{() -> height([leaf, z])
(height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)])}
(height([_eaa, _faa]) /\ height([_eaa, _gaa])) -> eq_nat([_faa, _gaa])
)
}

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


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

Clause system for inference is:

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


Solving took 30.000329 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6894, q_gen_6895, q_gen_6908, q_gen_6909, q_gen_6918, q_gen_6919, q_gen_6920, q_gen_6921, q_gen_6926, q_gen_6927, q_gen_6928, q_gen_6930, q_gen_6931, q_gen_6932, q_gen_6933, q_gen_6934, q_gen_6935},
Q_f={},
Delta=
{
<z>() -> q_gen_6920
<s>(q_gen_6920) -> q_gen_6932
<s>(q_gen_6932) -> q_gen_6935
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6894
<b, z>() -> q_gen_6895
<node, s>(q_gen_6909, q_gen_6890, q_gen_6890) -> q_gen_6908
<a, z>() -> q_gen_6909
<node, s>(q_gen_6921, q_gen_6919, q_gen_6894) -> q_gen_6918
<leaf, s>(q_gen_6920) -> q_gen_6919
<b, s>(q_gen_6920) -> q_gen_6921
<node, s>(q_gen_6927, q_gen_6919, q_gen_6919) -> q_gen_6926
<a, s>(q_gen_6920) -> q_gen_6927
<node, s>(q_gen_6921, q_gen_6919, q_gen_6919) -> q_gen_6928
<node, s>(q_gen_6933, q_gen_6931, q_gen_6928) -> q_gen_6930
<leaf, s>(q_gen_6932) -> q_gen_6931
<a, s>(q_gen_6932) -> q_gen_6933
<leaf, s>(q_gen_6935) -> q_gen_6934
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_6887, q_gen_6893, q_gen_6896, q_gen_6897, q_gen_6898, q_gen_6902, q_gen_6903, q_gen_6910, q_gen_6936, q_gen_6937},
Q_f={},
Delta=
{
<z>() -> q_gen_6897
<s>(q_gen_6897) -> q_gen_6903
<z, z>() -> q_gen_6887
<s, s>(q_gen_6887) -> q_gen_6893
<z, s>(q_gen_6897) -> q_gen_6896
<s, z>(q_gen_6897) -> q_gen_6898
<z, s>(q_gen_6903) -> q_gen_6902
<s, z>(q_gen_6903) -> q_gen_6910
<s, s>(q_gen_6937) -> q_gen_6936
<s, s>(q_gen_6898) -> q_gen_6937
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  max -> 
{{{
Q={q_gen_6888, q_gen_6899, q_gen_6900, q_gen_6907, q_gen_6911, q_gen_6912, q_gen_6917, q_gen_6929},
Q_f={},
Delta=
{
<z, z>() -> q_gen_6900
<s, s>(q_gen_6900) -> q_gen_6912
<z, z, z>() -> q_gen_6888
<s, z, s>(q_gen_6900) -> q_gen_6899
<s, s, s>(q_gen_6888) -> q_gen_6907
<s, z, s>(q_gen_6912) -> q_gen_6911
<z, s, s>(q_gen_6900) -> q_gen_6917
<z, s, s>(q_gen_6912) -> q_gen_6929
}

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6891, q_gen_6892, q_gen_6901, q_gen_6904, q_gen_6905, q_gen_6906, q_gen_6913, q_gen_6914, q_gen_6915, q_gen_6916, q_gen_6922, q_gen_6923, q_gen_6924, q_gen_6925},
Q_f={},
Delta=
{
<z>() -> q_gen_6906
<s>(q_gen_6906) -> q_gen_6925
<z, z>() -> q_gen_6892
<s, s>(q_gen_6892) -> q_gen_6914
<z, s>(q_gen_6906) -> q_gen_6916
<z, z, z>() -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6891
<s, z, s>(q_gen_6892) -> q_gen_6901
<s, s, s>(q_gen_6905) -> q_gen_6904
<z, z, s>(q_gen_6906) -> q_gen_6905
<s, z, s>(q_gen_6914) -> q_gen_6913
<z, s, s>(q_gen_6916) -> q_gen_6915
<s, z, s>(q_gen_6916) -> q_gen_6922
<s, s, s>(q_gen_6924) -> q_gen_6923
<z, z, s>(q_gen_6925) -> q_gen_6924
}

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.004018 s (model generation: 0.003882,  model checking: 0.000136):

Model:
|_
{
height -> 
{{{
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
}}}
  ;  plus -> 
{{{
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:
{
() -> height([leaf, z]) -> 0  ;  () -> leq([z, n2]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 0  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 0  ;  (leq([n, m])) -> max([n, m, m]) -> 0  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.003816 s (model generation: 0.003673,  model checking: 0.000143):

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

}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
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:
{
() -> height([leaf, z]) -> 0  ;  () -> leq([z, n2]) -> 0  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 1  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.003467 s (model generation: 0.003435,  model checking: 0.000032):

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

}

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

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

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

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:
{
() -> height([leaf, z]) -> 0  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 1  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Yes: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 3, which took 0.003407 s (model generation: 0.003338,  model checking: 0.000069):

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

}

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

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

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

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 1  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 1
}
Sat witness: Yes: (() -> height([leaf, z]), {

})

-------------------------------------------
Step 4, which took 0.003516 s (model generation: 0.003454,  model checking: 0.000062):

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

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

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

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

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 1  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.004468 s (model generation: 0.004369,  model checking: 0.000099):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 1  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.007310 s (model generation: 0.007135,  model checking: 0.000175):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 1  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 1  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 7, which took 0.010835 s (model generation: 0.010692,  model checking: 0.000143):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 2  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> z  ;  _daa -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 8, which took 0.007538 s (model generation: 0.007429,  model checking: 0.000109):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3  ;  (leq([s(nn1), z])) -> BOT -> 3  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> z  ;  _iaa -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.009069 s (model generation: 0.007864,  model checking: 0.001205):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.011457 s (model generation: 0.011378,  model checking: 0.000079):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 3  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 11, which took 0.008993 s (model generation: 0.008858,  model checking: 0.000135):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 3  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 4
}
Sat witness: Yes: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.013048 s (model generation: 0.012599,  model checking: 0.000449):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892},
Q_f={q_gen_6889},
Delta=
{
<z, z>() -> q_gen_6892
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 4  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.011373 s (model generation: 0.011354,  model checking: 0.000019):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 4  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 4  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 7  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 14, which took 0.007477 s (model generation: 0.006413,  model checking: 0.001064):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 4  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 4  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 7  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 7  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.015122 s (model generation: 0.013686,  model checking: 0.001436):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 4  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 5  ;  (leq([n, m])) -> max([n, m, m]) -> 7  ;  (not leq([n, m])) -> max([n, m, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 7  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> z  ;  _daa -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.014593 s (model generation: 0.013407,  model checking: 0.001186):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 5  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 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  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 17, which took 0.016010 s (model generation: 0.014901,  model checking: 0.001109):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 6  ;  () -> leq([z, n2]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 7  ;  (leq([n, m])) -> max([n, m, m]) -> 7  ;  (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 -> 7  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 18, which took 0.012017 s (model generation: 0.011777,  model checking: 0.000240):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 7  ;  () -> leq([z, n2]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 7  ;  (leq([n, m])) -> max([n, m, m]) -> 7  ;  (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 -> 7  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.009191 s (model generation: 0.009001,  model checking: 0.000190):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 7  ;  () -> leq([z, n2]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 7  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 7  ;  (leq([n, m])) -> max([n, m, m]) -> 10  ;  (not leq([n, m])) -> max([n, m, n]) -> 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  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Yes: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.014191 s (model generation: 0.010606,  model checking: 0.003585):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 7  ;  () -> leq([z, n2]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 10  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 8  ;  (leq([n, m])) -> max([n, m, m]) -> 10  ;  (not leq([n, m])) -> max([n, m, n]) -> 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  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 10
}
Sat witness: Yes: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> s(z)  ;  _daa -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 21, which took 0.017877 s (model generation: 0.016669,  model checking: 0.001208):

Model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6895, q_gen_6920},
Q_f={q_gen_6890},
Delta=
{
<z>() -> q_gen_6920
<leaf, s>(q_gen_6920) -> q_gen_6890
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6890
<a, z>() -> q_gen_6895
<b, s>(q_gen_6920) -> q_gen_6895
<b, z>() -> q_gen_6895
}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 8  ;  () -> leq([z, n2]) -> 8  ;  () -> plus([n, z, n]) -> 10  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 10  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 9  ;  (leq([n, m])) -> max([n, m, m]) -> 10  ;  (not leq([n, m])) -> max([n, m, n]) -> 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  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]), {
_wz -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.022682 s (model generation: 0.017714,  model checking: 0.004968):

Model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6895, q_gen_6920},
Q_f={q_gen_6890},
Delta=
{
<z>() -> q_gen_6920
<leaf, s>(q_gen_6920) -> q_gen_6890
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6890
<a, z>() -> q_gen_6895
<b, s>(q_gen_6920) -> q_gen_6895
<b, z>() -> q_gen_6895
}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<s>(q_gen_6906) -> q_gen_6906
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 9  ;  () -> leq([z, n2]) -> 9  ;  () -> plus([n, z, n]) -> 10  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 13  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 10  ;  (leq([n, m])) -> max([n, m, m]) -> 11  ;  (not leq([n, m])) -> max([n, m, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 13
}
Sat witness: Yes: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> s(z)  ;  _daa -> s(z)  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 23, which took 0.037875 s (model generation: 0.019848,  model checking: 0.018027):

Model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6895, q_gen_6920},
Q_f={q_gen_6890},
Delta=
{
<z>() -> q_gen_6920
<leaf, s>(q_gen_6920) -> q_gen_6890
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6890
<a, s>(q_gen_6920) -> q_gen_6895
<a, z>() -> q_gen_6895
<b, s>(q_gen_6920) -> q_gen_6895
<b, z>() -> q_gen_6895
}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<s>(q_gen_6906) -> q_gen_6906
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 10  ;  () -> leq([z, n2]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 11  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Yes: ((height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]), {
_baa -> z  ;  _caa -> s(s(z))  ;  _daa -> s(s(z))  ;  e -> a  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 24, which took 0.010908 s (model generation: 0.010501,  model checking: 0.000407):

Model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6895, q_gen_6920},
Q_f={q_gen_6890},
Delta=
{
<s>(q_gen_6920) -> q_gen_6920
<z>() -> q_gen_6920
<leaf, s>(q_gen_6920) -> q_gen_6890
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6890
<a, s>(q_gen_6920) -> q_gen_6895
<a, z>() -> q_gen_6895
<b, s>(q_gen_6920) -> q_gen_6895
<b, z>() -> q_gen_6895
}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<s>(q_gen_6906) -> q_gen_6906
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 11  ;  () -> leq([z, n2]) -> 11  ;  () -> plus([n, z, n]) -> 11  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 14  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12  ;  (leq([s(nn1), z])) -> BOT -> 12  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Yes: ((height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]), {
_haa -> s(s(s(z)))  ;  _iaa -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 25, which took 0.020669 s (model generation: 0.020181,  model checking: 0.000488):

Model:
|_
{
height -> 
{{{
Q={q_gen_6890, q_gen_6895, q_gen_6920},
Q_f={q_gen_6890},
Delta=
{
<s>(q_gen_6920) -> q_gen_6920
<z>() -> q_gen_6920
<leaf, s>(q_gen_6920) -> q_gen_6890
<leaf, z>() -> q_gen_6890
<node, s>(q_gen_6895, q_gen_6890, q_gen_6890) -> q_gen_6890
<a, s>(q_gen_6920) -> q_gen_6895
<a, z>() -> q_gen_6895
<b, s>(q_gen_6920) -> q_gen_6895
<b, z>() -> q_gen_6895
}

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

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

Datatype: <nat, nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6889, q_gen_6892, q_gen_6906},
Q_f={q_gen_6889},
Delta=
{
<s>(q_gen_6906) -> q_gen_6906
<z>() -> q_gen_6906
<s, s>(q_gen_6892) -> q_gen_6892
<z, s>(q_gen_6906) -> q_gen_6892
<z, z>() -> q_gen_6892
<s, s, s>(q_gen_6889) -> q_gen_6889
<s, z, s>(q_gen_6892) -> q_gen_6889
<z, s, s>(q_gen_6892) -> q_gen_6889
<z, z, s>(q_gen_6906) -> q_gen_6889
<z, z, z>() -> q_gen_6889
}

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:
{
() -> height([leaf, z]) -> 12  ;  () -> leq([z, n2]) -> 12  ;  () -> plus([n, z, n]) -> 12  ;  (height([t1, _baa]) /\ height([t2, _caa]) /\ max([_baa, _caa, _daa])) -> height([node(e, t1, t2), s(_daa)]) -> 16  ;  (height([t1, _haa]) /\ height([node(e, t2, t1), _iaa])) -> leq([_haa, _iaa]) -> 14  ;  (leq([n, m])) -> max([n, m, m]) -> 12  ;  (not leq([n, m])) -> max([n, m, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (plus([n, mm, _wz])) -> plus([n, s(mm), s(_wz)]) -> 14
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

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