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


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, n2])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(max, F:
{(leq([n, m])) -> max([n, m, m])
(not leq([n, m])) -> max([n, m, n])}
(max([_nn, _on, _pn]) /\ max([_nn, _on, _qn])) -> eq_nat([_pn, _qn])
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)])}
(plus([_sn, _tn, _un]) /\ plus([_sn, _tn, _vn])) -> eq_nat([_un, _vn])
)
(height, F:
{() -> height([leaf, z])
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)])}
(height([_zn, _ao]) /\ height([_zn, _bo])) -> eq_nat([_ao, _bo])
)
(numnodes, F:
{() -> numnodes([leaf, z])
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)])}
(numnodes([_fo, _go]) /\ numnodes([_fo, _ho])) -> eq_nat([_go, _ho])
)
}

properties:
{(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo])}


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

Clause system for inference is:

{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> numnodes([leaf, z]) -> 0
() -> plus([n, z, n]) -> 0
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 0
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 0
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 0
}


Solving took 60.002438 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2911, q_gen_2912, q_gen_2913, q_gen_2930, q_gen_2931, q_gen_2940, q_gen_2941, q_gen_2952, q_gen_2953, q_gen_2954, q_gen_2957, q_gen_2958, q_gen_2959, q_gen_2960, q_gen_2961, q_gen_2962, q_gen_2964, q_gen_2965, q_gen_2966, q_gen_2980, q_gen_2981, q_gen_2982, q_gen_2985, q_gen_2987, q_gen_2993, q_gen_2994, q_gen_2995, q_gen_3002, q_gen_3003, q_gen_3004, q_gen_3009, q_gen_3010, q_gen_3022, q_gen_3023, q_gen_3024},
Q_f={},
Delta=
{
<leaf>() -> q_gen_2912
<b>() -> q_gen_2913
<a>() -> q_gen_2931
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<node>(q_gen_2913, q_gen_2912, q_gen_2961) -> q_gen_2960
<node>(q_gen_2931, q_gen_2912, q_gen_2912) -> q_gen_2961
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2965
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2911
<node, s>(q_gen_2931, q_gen_2912, q_gen_2904) -> q_gen_2930
<node, s>(q_gen_2913, q_gen_2912, q_gen_2941) -> q_gen_2940
<node, z>(q_gen_2931, q_gen_2912, q_gen_2912) -> q_gen_2941
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2952
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2953
<node, s>(q_gen_2913, q_gen_2960, q_gen_2958) -> q_gen_2957
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2962
<node, s>(q_gen_2913, q_gen_2965, q_gen_2958) -> q_gen_2964
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2966
<node, s>(q_gen_2913, q_gen_2954, q_gen_2981) -> q_gen_2980
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2981
<node, s>(q_gen_2913, q_gen_2954, q_gen_2962) -> q_gen_2982
<node, s>(q_gen_2913, q_gen_2912, q_gen_2981) -> q_gen_2985
<node, s>(q_gen_2913, q_gen_2961, q_gen_2958) -> q_gen_2987
<node, s>(q_gen_2913, q_gen_2912, q_gen_2952) -> q_gen_2993
<node, s>(q_gen_2913, q_gen_2965, q_gen_2995) -> q_gen_2994
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2995
<node, s>(q_gen_2913, q_gen_2912, q_gen_3003) -> q_gen_3002
<node, z>(q_gen_2913, q_gen_2912, q_gen_2965) -> q_gen_3003
<node, s>(q_gen_2913, q_gen_2954, q_gen_2966) -> q_gen_3004
<node, s>(q_gen_2913, q_gen_2954, q_gen_3010) -> q_gen_3009
<node, z>(q_gen_2913, q_gen_2954, q_gen_2965) -> q_gen_3010
<node, s>(q_gen_2913, q_gen_2954, q_gen_2952) -> q_gen_3022
<node, s>(q_gen_2913, q_gen_2912, q_gen_3024) -> q_gen_3023
<node, z>(q_gen_2913, q_gen_2954, q_gen_2954) -> q_gen_3024
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_2900, q_gen_2910, q_gen_2914, q_gen_2915, q_gen_2920, q_gen_2921, q_gen_2932, q_gen_2942, q_gen_2963, q_gen_2984},
Q_f={},
Delta=
{
<z>() -> q_gen_2915
<s>(q_gen_2915) -> q_gen_2921
<z, z>() -> q_gen_2900
<s, s>(q_gen_2900) -> q_gen_2910
<z, s>(q_gen_2915) -> q_gen_2914
<z, s>(q_gen_2921) -> q_gen_2920
<s, z>(q_gen_2915) -> q_gen_2932
<s, z>(q_gen_2921) -> q_gen_2942
<s, s>(q_gen_2932) -> q_gen_2963
<s, s>(q_gen_2963) -> q_gen_2984
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_2901, q_gen_2916, q_gen_2917, q_gen_2928, q_gen_2929, q_gen_2933, q_gen_2939, q_gen_2943, q_gen_2944},
Q_f={},
Delta=
{
<z>() -> q_gen_2917
<z, z>() -> q_gen_2929
<s, s>(q_gen_2929) -> q_gen_2944
<z, z, z>() -> q_gen_2901
<z, s, z>(q_gen_2917) -> q_gen_2916
<z, s, s>(q_gen_2929) -> q_gen_2928
<s, z, s>(q_gen_2929) -> q_gen_2933
<s, s, s>(q_gen_2901) -> q_gen_2939
<s, z, s>(q_gen_2944) -> q_gen_2943
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2907, q_gen_2908, q_gen_2909, q_gen_2926, q_gen_2927, q_gen_2936, q_gen_2937, q_gen_2938, q_gen_2949, q_gen_2950, q_gen_2951, q_gen_2955, q_gen_2956, q_gen_2967, q_gen_2968, q_gen_2969, q_gen_2973, q_gen_2974, q_gen_2975, q_gen_2976, q_gen_2979, q_gen_2983, q_gen_2988, q_gen_2989, q_gen_2991, q_gen_2992, q_gen_2996, q_gen_2998, q_gen_2999, q_gen_3000, q_gen_3001, q_gen_3005, q_gen_3007, q_gen_3008, q_gen_3011, q_gen_3012, q_gen_3013, q_gen_3016, q_gen_3017, q_gen_3018, q_gen_3019, q_gen_3020, q_gen_3021},
Q_f={},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<a>() -> q_gen_2927
<z>() -> q_gen_2938
<s>(q_gen_2938) -> q_gen_2951
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2927, q_gen_2908, q_gen_2908) -> q_gen_2974
<s>(q_gen_2951) -> q_gen_3000
<node>(q_gen_2909, q_gen_2908, q_gen_2974) -> q_gen_3001
<node>(q_gen_2909, q_gen_2956, q_gen_2908) -> q_gen_3008
<s>(q_gen_3000) -> q_gen_3018
<node>(q_gen_2909, q_gen_2908, q_gen_3020) -> q_gen_3019
<node>(q_gen_2909, q_gen_3008, q_gen_3021) -> q_gen_3020
<node>(q_gen_2909, q_gen_3008, q_gen_2908) -> q_gen_3021
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2907
<node, s>(q_gen_2927, q_gen_2908, q_gen_2903) -> q_gen_2926
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2936
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2908, q_gen_2950) -> q_gen_2949
<leaf, s>(q_gen_2951) -> q_gen_2950
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2955
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2927, q_gen_2956, q_gen_2969) -> q_gen_2968
<node, s>(q_gen_2909, q_gen_2956, q_gen_2955) -> q_gen_2969
<node, s>(q_gen_2909, q_gen_2974, q_gen_2968) -> q_gen_2973
<node, s>(q_gen_2927, q_gen_2908, q_gen_2937) -> q_gen_2975
<node, s>(q_gen_2927, q_gen_2956, q_gen_2937) -> q_gen_2976
<node, s>(q_gen_2909, q_gen_2974, q_gen_2976) -> q_gen_2979
<node, s>(q_gen_2909, q_gen_2956, q_gen_2907) -> q_gen_2983
<node, s>(q_gen_2909, q_gen_2974, q_gen_2903) -> q_gen_2988
<node, s>(q_gen_2927, q_gen_2956, q_gen_2967) -> q_gen_2989
<node, s>(q_gen_2909, q_gen_2956, q_gen_2992) -> q_gen_2991
<node, s>(q_gen_2927, q_gen_2956, q_gen_2955) -> q_gen_2992
<node, s>(q_gen_2909, q_gen_2908, q_gen_2975) -> q_gen_2996
<node, s>(q_gen_2909, q_gen_3001, q_gen_2999) -> q_gen_2998
<leaf, s>(q_gen_3000) -> q_gen_2999
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_3005
<node, s>(q_gen_2909, q_gen_3008, q_gen_2950) -> q_gen_3007
<node, s>(q_gen_2909, q_gen_2908, q_gen_3012) -> q_gen_3011
<node, s>(q_gen_2909, q_gen_3008, q_gen_3013) -> q_gen_3012
<node, s>(q_gen_2909, q_gen_3008, q_gen_2937) -> q_gen_3013
<node, s>(q_gen_2909, q_gen_3019, q_gen_3017) -> q_gen_3016
<leaf, s>(q_gen_3018) -> q_gen_3017
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2905, q_gen_2906, q_gen_2918, q_gen_2919, q_gen_2922, q_gen_2923, q_gen_2924, q_gen_2925, q_gen_2934, q_gen_2935, q_gen_2945, q_gen_2946, q_gen_2947, q_gen_2948, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2977, q_gen_2978, q_gen_2986, q_gen_2990, q_gen_2997, q_gen_3006, q_gen_3014, q_gen_3015},
Q_f={},
Delta=
{
<z>() -> q_gen_2925
<s>(q_gen_2925) -> q_gen_2948
<z, z>() -> q_gen_2906
<s, s>(q_gen_2906) -> q_gen_2919
<z, s>(q_gen_2925) -> q_gen_2935
<s, s>(q_gen_2919) -> q_gen_2972
<z, z, z>() -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2905
<s, z, s>(q_gen_2919) -> q_gen_2918
<s, z, s>(q_gen_2906) -> q_gen_2922
<s, s, s>(q_gen_2924) -> q_gen_2923
<z, z, s>(q_gen_2925) -> q_gen_2924
<z, s, s>(q_gen_2935) -> q_gen_2934
<s, z, s>(q_gen_2935) -> q_gen_2945
<s, s, s>(q_gen_2947) -> q_gen_2946
<z, z, s>(q_gen_2948) -> q_gen_2947
<s, s, s>(q_gen_2971) -> q_gen_2970
<z, s, s>(q_gen_2972) -> q_gen_2971
<s, s, s>(q_gen_2978) -> q_gen_2977
<s, s, s>(q_gen_2902) -> q_gen_2978
<s, s, s>(q_gen_2945) -> q_gen_2986
<s, s, s>(q_gen_2923) -> q_gen_2990
<s, s, s>(q_gen_2918) -> q_gen_2997
<s, s, s>(q_gen_2922) -> q_gen_3006
<s, s, s>(q_gen_3015) -> q_gen_3014
<s, z, s>(q_gen_2972) -> q_gen_3015
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005370 s (model generation: 0.004837,  model checking: 0.000533):

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

}

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

}

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> numnodes([leaf, z]) -> 0
() -> plus([n, z, n]) -> 0
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 0
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 1
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.005314 s (model generation: 0.004850,  model checking: 0.000464):

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

}

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

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

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> numnodes([leaf, z]) -> 0
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.004598 s (model generation: 0.004431,  model checking: 0.000167):

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

}

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

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

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 1
}
Sat witness: Found: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 3, which took 0.004149 s (model generation: 0.004012,  model checking: 0.000137):

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

}

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

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 0
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 1
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.006113 s (model generation: 0.004595,  model checking: 0.001518):

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

}

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

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 1
}
Sat witness: Found: (() -> height([leaf, z]), {

})

-------------------------------------------
Step 5, which took 0.005379 s (model generation: 0.005271,  model checking: 0.000108):

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

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

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 1
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]), {
_rn -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.006992 s (model generation: 0.006801,  model checking: 0.000191):

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

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

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> z  ;  _do -> z  ;  _eo -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 7, which took 0.008824 s (model generation: 0.008568,  model checking: 0.000256):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 8, which took 0.009710 s (model generation: 0.009465,  model checking: 0.000245):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.012290 s (model generation: 0.012170,  model checking: 0.000120):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 1
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> z  ;  _yn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 10, which took 0.007285 s (model generation: 0.006664,  model checking: 0.000621):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 2
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 11, which took 0.013310 s (model generation: 0.012357,  model checking: 0.000953):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 3
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.008529 s (model generation: 0.008305,  model checking: 0.000224):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 3
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 4
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 4
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.007059 s (model generation: 0.005864,  model checking: 0.001195):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

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

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 4
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 4
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]), {
_rn -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 14, which took 0.016405 s (model generation: 0.013967,  model checking: 0.002438):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 4
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> z  ;  _do -> z  ;  _eo -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 15, which took 0.014874 s (model generation: 0.014293,  model checking: 0.000581):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 4
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 4
(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 -> 5
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 16, which took 0.015989 s (model generation: 0.014903,  model checking: 0.001086):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 4
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 4
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 7
(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 -> 5
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> z  ;  _yn -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 17, which took 0.016414 s (model generation: 0.015288,  model checking: 0.001126):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 5
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 5
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 5
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 18, which took 0.016106 s (model generation: 0.015667,  model checking: 0.000439):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 6
() -> leq([z, n2]) -> 6
() -> numnodes([leaf, z]) -> 6
() -> plus([n, z, n]) -> 6
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 6
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 9
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 7
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 19, which took 0.017391 s (model generation: 0.015695,  model checking: 0.001696):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 7
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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 -> 9
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 7
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]), {
_rn -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.017355 s (model generation: 0.016324,  model checking: 0.001031):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 7
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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 -> 9
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 10
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 10
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> z  ;  _do -> z  ;  _eo -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 21, which took 0.018139 s (model generation: 0.017372,  model checking: 0.000767):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 7
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 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 -> 9
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 10
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 10
}
Sat witness: Found: ((leq([n, m])) -> max([n, m, m]), {
m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.018893 s (model generation: 0.017717,  model checking: 0.001176):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 7
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 7
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 10
(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 -> 9
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 10
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 10
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 23, which took 0.020402 s (model generation: 0.018818,  model checking: 0.001584):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 8
() -> leq([z, n2]) -> 8
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 8
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 8
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 10
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 10
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 10
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 10
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 24, which took 0.021471 s (model generation: 0.019740,  model checking: 0.001731):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 9
() -> leq([z, n2]) -> 9
() -> numnodes([leaf, z]) -> 9
() -> plus([n, z, n]) -> 9
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 9
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 10
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 10
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]), {
_rn -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 25, which took 0.024796 s (model generation: 0.021807,  model checking: 0.002989):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 10
() -> leq([z, n2]) -> 10
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 10
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 10
(leq([n, m])) -> max([n, m, m]) -> 10
(not leq([n, m])) -> max([n, m, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 13
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 13
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> z  ;  _do -> z  ;  _eo -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 26, which took 0.026227 s (model generation: 0.023052,  model checking: 0.003175):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 10
() -> leq([z, n2]) -> 10
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 10
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 13
(leq([n, m])) -> max([n, m, m]) -> 11
(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
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 13
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 13
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> z  ;  _yn -> z  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 27, which took 0.032699 s (model generation: 0.024148,  model checking: 0.008551):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 11
() -> leq([z, n2]) -> 11
() -> numnodes([leaf, z]) -> 11
() -> plus([n, z, n]) -> 11
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 11
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 13
(leq([n, m])) -> max([n, m, m]) -> 12
(not leq([n, m])) -> max([n, m, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 16
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 14
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(z)  ;  _do -> z  ;  _eo -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 28, which took 0.028296 s (model generation: 0.024443,  model checking: 0.003853):

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

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 12
() -> leq([z, n2]) -> 12
() -> numnodes([leaf, z]) -> 12
() -> plus([n, z, n]) -> 12
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 12
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 13
(not leq([n, m])) -> max([n, m, n]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 16
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 14
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> s(z)  ;  _xn -> z  ;  _yn -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, node(a, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 29, which took 0.027811 s (model generation: 0.027649,  model checking: 0.000162):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<z>() -> q_gen_2959
<leaf, s>(q_gen_2959) -> q_gen_2904
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 12
() -> leq([z, n2]) -> 12
() -> numnodes([leaf, z]) -> 12
() -> plus([n, z, n]) -> 12
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 15
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 13
(not leq([n, m])) -> max([n, m, n]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 16
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 14
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(z)  ;  _jo -> z  ;  t1 -> leaf
})

-------------------------------------------
Step 30, which took 0.029525 s (model generation: 0.027340,  model checking: 0.002185):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2941, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2941) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2941
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2941
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 13
() -> leq([z, n2]) -> 13
() -> numnodes([leaf, z]) -> 13
() -> plus([n, z, n]) -> 13
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 18
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 14
(not leq([n, m])) -> max([n, m, n]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 16
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 15
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(s(z))  ;  _jo -> s(z)  ;  t1 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 31, which took 0.029037 s (model generation: 0.028216,  model checking: 0.000821):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2941, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2941) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2941
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2941
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 14
() -> leq([z, n2]) -> 14
() -> numnodes([leaf, z]) -> 14
() -> plus([n, z, n]) -> 14
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 18
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 16
(leq([n, m])) -> max([n, m, m]) -> 14
(not leq([n, m])) -> max([n, m, n]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 15
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 16
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 15
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 32, which took 0.050840 s (model generation: 0.029292,  model checking: 0.021548):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2940, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2940
<node, s>(q_gen_2913, q_gen_2912, q_gen_2940) -> q_gen_2940
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2940
}

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_2901, q_gen_2916, q_gen_2917, q_gen_2929},
Q_f={q_gen_2901},
Delta=
{
<z>() -> q_gen_2917
<s, s>(q_gen_2929) -> q_gen_2929
<z, z>() -> q_gen_2929
<s, s, s>(q_gen_2901) -> q_gen_2901
<s, z, s>(q_gen_2929) -> q_gen_2901
<z, s, s>(q_gen_2929) -> q_gen_2901
<z, z, z>() -> q_gen_2901
<z, s, z>(q_gen_2917) -> q_gen_2916
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 15
() -> leq([z, n2]) -> 15
() -> numnodes([leaf, z]) -> 15
() -> plus([n, z, n]) -> 15
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 18
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 19
(leq([n, m])) -> max([n, m, m]) -> 15
(not leq([n, m])) -> max([n, m, n]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 16
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 17
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 16
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> s(z)  ;  _xn -> z  ;  _yn -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 33, which took 0.050964 s (model generation: 0.031461,  model checking: 0.019503):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 16
() -> leq([z, n2]) -> 16
() -> numnodes([leaf, z]) -> 16
() -> plus([n, z, n]) -> 16
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 21
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 19
(leq([n, m])) -> max([n, m, m]) -> 16
(not leq([n, m])) -> max([n, m, n]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(leq([s(nn1), z])) -> BOT -> 17
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 18
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 17
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(s(z))  ;  _jo -> s(z)  ;  t1 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 34, which took 0.068141 s (model generation: 0.034967,  model checking: 0.033174):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959, q_gen_2960},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2960
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2960
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2960, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2938},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<leaf, s>(q_gen_2938) -> q_gen_2903
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 17
() -> leq([z, n2]) -> 17
() -> numnodes([leaf, z]) -> 17
() -> plus([n, z, n]) -> 17
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 21
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 22
(leq([n, m])) -> max([n, m, m]) -> 17
(not leq([n, m])) -> max([n, m, n]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 18
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 19
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 18
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> s(z)  ;  _xn -> z  ;  _yn -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 35, which took 0.079516 s (model generation: 0.038624,  model checking: 0.040892):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 18
() -> leq([z, n2]) -> 18
() -> numnodes([leaf, z]) -> 18
() -> plus([n, z, n]) -> 18
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 21
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 22
(leq([n, m])) -> max([n, m, m]) -> 18
(not leq([n, m])) -> max([n, m, n]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 22
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 19
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(z)  ;  _do -> s(s(s(s(z))))  ;  _eo -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)))
})

-------------------------------------------
Step 36, which took 0.057042 s (model generation: 0.044989,  model checking: 0.012053):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 19
() -> leq([z, n2]) -> 19
() -> numnodes([leaf, z]) -> 19
() -> plus([n, z, n]) -> 19
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 22
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 22
(leq([n, m])) -> max([n, m, m]) -> 19
(not leq([n, m])) -> max([n, m, n]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20
(leq([s(nn1), z])) -> BOT -> 20
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 25
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 20
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(s(z))  ;  _do -> s(s(z))  ;  _eo -> s(s(z))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 37, which took 0.082635 s (model generation: 0.054163,  model checking: 0.028472):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2955, q_gen_2956},
Q_f={q_gen_2903, q_gen_2955},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2955
<node, s>(q_gen_2909, q_gen_2956, q_gen_2955) -> q_gen_2955
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 20
() -> leq([z, n2]) -> 20
() -> numnodes([leaf, z]) -> 20
() -> plus([n, z, n]) -> 20
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 22
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 25
(leq([n, m])) -> max([n, m, m]) -> 20
(not leq([n, m])) -> max([n, m, n]) -> 21
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 21
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 25
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 21
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 38, which took 0.061552 s (model generation: 0.058532,  model checking: 0.003020):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2907, q_gen_2908, q_gen_2909, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2907},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2907
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2907
<node, s>(q_gen_2909, q_gen_2908, q_gen_2907) -> q_gen_2907
<node, s>(q_gen_2909, q_gen_2956, q_gen_2907) -> q_gen_2907
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 21
() -> leq([z, n2]) -> 21
() -> numnodes([leaf, z]) -> 21
() -> plus([n, z, n]) -> 21
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 25
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 25
(leq([n, m])) -> max([n, m, m]) -> 21
(not leq([n, m])) -> max([n, m, n]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 22
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 25
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 22
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(s(s(z)))  ;  _jo -> s(s(z))  ;  t1 -> node(b, node(b, leaf, leaf), node(b, leaf, leaf))
})

-------------------------------------------
Step 39, which took 0.080237 s (model generation: 0.068729,  model checking: 0.011508):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2927, q_gen_2937, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2927, q_gen_2908, q_gen_2908) -> q_gen_2908
<b>() -> q_gen_2909
<a>() -> q_gen_2927
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2927, q_gen_2908, q_gen_2903) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2927, q_gen_2908, q_gen_2937) -> q_gen_2937
<node, s>(q_gen_2927, q_gen_2956, q_gen_2937) -> q_gen_2937
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 22
() -> leq([z, n2]) -> 22
() -> numnodes([leaf, z]) -> 22
() -> plus([n, z, n]) -> 22
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 25
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 25
(leq([n, m])) -> max([n, m, m]) -> 22
(not leq([n, m])) -> max([n, m, n]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 23
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 28
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 23
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> z  ;  _do -> z  ;  _eo -> s(z)  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 40, which took 0.069687 s (model generation: 0.062820,  model checking: 0.006867):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2955, q_gen_2956},
Q_f={q_gen_2903, q_gen_2955},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2955) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2955
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 23
() -> leq([z, n2]) -> 23
() -> numnodes([leaf, z]) -> 23
() -> plus([n, z, n]) -> 23
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 25
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 28
(leq([n, m])) -> max([n, m, m]) -> 23
(not leq([n, m])) -> max([n, m, n]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 24
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 28
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 24
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 41, which took 0.052055 s (model generation: 0.051397,  model checking: 0.000658):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2936, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2936) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2908, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2936
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2924, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2924) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, z>() -> q_gen_2902
<s, s, s>(q_gen_2902) -> q_gen_2924
<z, z, s>(q_gen_2925) -> q_gen_2924
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 24
() -> leq([z, n2]) -> 24
() -> numnodes([leaf, z]) -> 24
() -> plus([n, z, n]) -> 24
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 25
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 28
(leq([n, m])) -> max([n, m, m]) -> 24
(not leq([n, m])) -> max([n, m, n]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 24
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 28
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 27
}
Sat witness: Found: ((plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]), {
_rn -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 42, which took 0.060453 s (model generation: 0.056698,  model checking: 0.003755):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2927, q_gen_2937, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<node>(q_gen_2927, q_gen_2908, q_gen_2908) -> q_gen_2908
<b>() -> q_gen_2909
<a>() -> q_gen_2927
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2927, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2927, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2927, q_gen_2956, q_gen_2937) -> q_gen_2937
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 25
() -> leq([z, n2]) -> 25
() -> numnodes([leaf, z]) -> 25
() -> plus([n, z, n]) -> 25
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 28
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 28
(leq([n, m])) -> max([n, m, m]) -> 25
(not leq([n, m])) -> max([n, m, n]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 25
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 28
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 27
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(s(z))  ;  _jo -> s(z)  ;  t1 -> node(b, node(a, leaf, leaf), leaf)
})

-------------------------------------------
Step 43, which took 0.077134 s (model generation: 0.073490,  model checking: 0.003644):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2936, q_gen_2937, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903, q_gen_2936},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2936) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2936
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 26
() -> leq([z, n2]) -> 26
() -> numnodes([leaf, z]) -> 26
() -> plus([n, z, n]) -> 26
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 28
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 28
(leq([n, m])) -> max([n, m, m]) -> 26
(not leq([n, m])) -> max([n, m, n]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 26
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 31
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 28
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(s(z))  ;  _do -> s(s(z))  ;  _eo -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(a, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 44, which took 0.118030 s (model generation: 0.079358,  model checking: 0.038672):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2927, q_gen_2937, q_gen_2938, q_gen_2956},
Q_f={q_gen_2903},
Delta=
{
<leaf>() -> q_gen_2908
<b>() -> q_gen_2909
<a>() -> q_gen_2927
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2927, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2903
<node, s>(q_gen_2927, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2927, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2927, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2927, q_gen_2956, q_gen_2937) -> q_gen_2937
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 27
() -> leq([z, n2]) -> 27
() -> numnodes([leaf, z]) -> 27
() -> plus([n, z, n]) -> 27
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 28
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 31
(leq([n, m])) -> max([n, m, m]) -> 27
(not leq([n, m])) -> max([n, m, n]) -> 27
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 27
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 31
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 29
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, node(b, leaf, leaf))
})

-------------------------------------------
Step 45, which took 0.172156 s (model generation: 0.094022,  model checking: 0.078134):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2936, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2936},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2908, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 28
() -> leq([z, n2]) -> 28
() -> numnodes([leaf, z]) -> 28
() -> plus([n, z, n]) -> 28
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 29
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 31
(leq([n, m])) -> max([n, m, m]) -> 28
(not leq([n, m])) -> max([n, m, n]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 28
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 34
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 30
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(s(s(z)))  ;  _do -> s(z)  ;  _eo -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, leaf, node(a, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 46, which took 0.085605 s (model generation: 0.080834,  model checking: 0.004771):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2937},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 29
() -> leq([z, n2]) -> 29
() -> numnodes([leaf, z]) -> 29
() -> plus([n, z, n]) -> 29
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 30
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 34
(leq([n, m])) -> max([n, m, m]) -> 29
(not leq([n, m])) -> max([n, m, n]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 29
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 34
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 31
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 47, which took 0.096870 s (model generation: 0.095869,  model checking: 0.001001):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2955, q_gen_2956},
Q_f={q_gen_2903, q_gen_2955},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2955
<node, s>(q_gen_2909, q_gen_2956, q_gen_2955) -> q_gen_2955
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 30
() -> leq([z, n2]) -> 30
() -> numnodes([leaf, z]) -> 30
() -> plus([n, z, n]) -> 30
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 33
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 34
(leq([n, m])) -> max([n, m, m]) -> 30
(not leq([n, m])) -> max([n, m, n]) -> 30
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 30
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 34
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 31
}
Sat witness: Found: ((height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]), {
_io -> s(s(s(z)))  ;  _jo -> s(s(z))  ;  t1 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 48, which took 0.170237 s (model generation: 0.099065,  model checking: 0.071172):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2937},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 31
() -> leq([z, n2]) -> 31
() -> numnodes([leaf, z]) -> 31
() -> plus([n, z, n]) -> 31
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 34
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 34
(leq([n, m])) -> max([n, m, m]) -> 31
(not leq([n, m])) -> max([n, m, n]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 31
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 37
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 32
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(s(z))  ;  _do -> s(z)  ;  _eo -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 49, which took 0.132836 s (model generation: 0.098038,  model checking: 0.034798):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2937, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2937},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<node>(q_gen_2909, q_gen_2956, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2937) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2937) -> q_gen_2937
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 32
() -> leq([z, n2]) -> 32
() -> numnodes([leaf, z]) -> 32
() -> plus([n, z, n]) -> 32
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 34
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 37
(leq([n, m])) -> max([n, m, m]) -> 32
(not leq([n, m])) -> max([n, m, n]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 32
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 37
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 33
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 50, which took 1.187715 s (model generation: 0.112597,  model checking: 1.075118):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2954, q_gen_2954) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2936, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2936},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<node>(q_gen_2909, q_gen_2956, q_gen_2908) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2908, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 33
() -> leq([z, n2]) -> 33
() -> numnodes([leaf, z]) -> 33
() -> plus([n, z, n]) -> 33
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 35
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 37
(leq([n, m])) -> max([n, m, m]) -> 33
(not leq([n, m])) -> max([n, m, n]) -> 33
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 33
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 40
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 34
}
Sat witness: Found: ((numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]), {
_co -> s(s(s(s(z))))  ;  _do -> s(z)  ;  _eo -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(b, leaf, node(b, node(b, node(b, leaf, leaf), leaf), node(b, node(b, node(b, leaf, leaf), leaf), leaf)))  ;  t2 -> leaf
})

-------------------------------------------
Step 51, which took 0.119006 s (model generation: 0.113681,  model checking: 0.005325):

Model:
|_
{
height -> 
{{{
Q={q_gen_2904, q_gen_2912, q_gen_2913, q_gen_2954, q_gen_2958, q_gen_2959},
Q_f={q_gen_2904},
Delta=
{
<leaf>() -> q_gen_2912
<a>() -> q_gen_2913
<b>() -> q_gen_2913
<node>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2954
<node>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2954
<node>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2954
<z>() -> q_gen_2959
<leaf, z>() -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2912, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2904) -> q_gen_2904
<node, s>(q_gen_2913, q_gen_2954, q_gen_2958) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2912) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2912, q_gen_2954) -> q_gen_2904
<node, z>(q_gen_2913, q_gen_2954, q_gen_2912) -> q_gen_2904
<leaf, s>(q_gen_2959) -> q_gen_2958
<node, s>(q_gen_2913, q_gen_2912, q_gen_2958) -> q_gen_2958
<node, z>(q_gen_2913, q_gen_2954, q_gen_2954) -> q_gen_2958
}

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

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

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_2903, q_gen_2908, q_gen_2909, q_gen_2936, q_gen_2938, q_gen_2956, q_gen_2967},
Q_f={q_gen_2903, q_gen_2936},
Delta=
{
<leaf>() -> q_gen_2908
<a>() -> q_gen_2909
<b>() -> q_gen_2909
<s>(q_gen_2938) -> q_gen_2938
<z>() -> q_gen_2938
<node>(q_gen_2909, q_gen_2908, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2908, q_gen_2956) -> q_gen_2956
<node>(q_gen_2909, q_gen_2956, q_gen_2908) -> q_gen_2956
<node>(q_gen_2909, q_gen_2956, q_gen_2956) -> q_gen_2956
<leaf, z>() -> q_gen_2903
<node, s>(q_gen_2909, q_gen_2908, q_gen_2903) -> q_gen_2903
<leaf, s>(q_gen_2938) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2908, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2936) -> q_gen_2936
<node, s>(q_gen_2909, q_gen_2956, q_gen_2903) -> q_gen_2967
<node, s>(q_gen_2909, q_gen_2956, q_gen_2967) -> q_gen_2967
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2902, q_gen_2906, q_gen_2925},
Q_f={q_gen_2902},
Delta=
{
<s>(q_gen_2925) -> q_gen_2925
<z>() -> q_gen_2925
<s, s>(q_gen_2906) -> q_gen_2906
<z, s>(q_gen_2925) -> q_gen_2906
<z, z>() -> q_gen_2906
<s, s, s>(q_gen_2902) -> q_gen_2902
<s, z, s>(q_gen_2906) -> q_gen_2902
<z, s, s>(q_gen_2906) -> q_gen_2902
<z, z, s>(q_gen_2925) -> q_gen_2902
<z, z, z>() -> q_gen_2902
}

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

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

Teacher's answer:
New clause system:
{
() -> height([leaf, z]) -> 34
() -> leq([z, n2]) -> 34
() -> numnodes([leaf, z]) -> 34
() -> plus([n, z, n]) -> 34
(height([t1, _io]) /\ numnodes([t1, _jo])) -> leq([_io, _jo]) -> 36
(height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]) -> 40
(leq([n, m])) -> max([n, m, m]) -> 34
(not leq([n, m])) -> max([n, m, n]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 34
(numnodes([t1, _co]) /\ numnodes([t2, _do]) /\ plus([_co, _do, _eo])) -> numnodes([node(e, t1, t2), s(_eo)]) -> 40
(plus([n, mm, _rn])) -> plus([n, s(mm), s(_rn)]) -> 35
}
Sat witness: Found: ((height([t1, _wn]) /\ height([t2, _xn]) /\ max([_wn, _xn, _yn])) -> height([node(e, t1, t2), s(_yn)]), {
_wn -> z  ;  _xn -> s(z)  ;  _yn -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(b, leaf, leaf), node(b, leaf, leaf))
})

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