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

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


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

Clause system for inference is:

{
() -> depth([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 0
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 0
(leq([n, m])) -> max([n, m, m]) -> 0
(not leq([n, m])) -> max([n, m, n]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 60.000162 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2763, q_gen_2764, q_gen_2767, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2772, q_gen_2774, q_gen_2775, q_gen_2776, q_gen_2777, q_gen_2779, q_gen_2780, q_gen_2781, q_gen_2782, q_gen_2783, q_gen_2785, q_gen_2786, q_gen_2787, q_gen_2788, q_gen_2789, q_gen_2790, q_gen_2791, q_gen_2792, q_gen_2793, q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2797, q_gen_2798, q_gen_2799, q_gen_2800, q_gen_2801, q_gen_2802, q_gen_2808, q_gen_2809, q_gen_2810, q_gen_2811, q_gen_2812, q_gen_2813, q_gen_2814, q_gen_2815, q_gen_2817, q_gen_2818, q_gen_2820, q_gen_2821, q_gen_2822, q_gen_2823, q_gen_2824, q_gen_2825, q_gen_2826, q_gen_2827, q_gen_2828, q_gen_2829, q_gen_2830, q_gen_2831, q_gen_2832, q_gen_2833, q_gen_2834, q_gen_2835, q_gen_2840, q_gen_2841, q_gen_2842, q_gen_2843, q_gen_2844, q_gen_2845, q_gen_2846, q_gen_2847, q_gen_2848, q_gen_2849, q_gen_2850, q_gen_2853, q_gen_2854, q_gen_2857, q_gen_2858, q_gen_2859, q_gen_2860, q_gen_2861, q_gen_2862, q_gen_2863, q_gen_2864, q_gen_2865, q_gen_2866, q_gen_2867, q_gen_2868, q_gen_2869, q_gen_2870, q_gen_2872, q_gen_2873, q_gen_2874, q_gen_2875, q_gen_2876, q_gen_2877, q_gen_2878, q_gen_2879, q_gen_2880, q_gen_2881, q_gen_2882, q_gen_2883, q_gen_2884, q_gen_2885, q_gen_2886, q_gen_2887, q_gen_2890, q_gen_2891, q_gen_2892, q_gen_2893, q_gen_2894, q_gen_2895, q_gen_2896, q_gen_2897, q_gen_2898, q_gen_2899},
Q_f={},
Delta=
{
<leaf>() -> q_gen_2752
<b>() -> q_gen_2753
<a>() -> q_gen_2764
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2782
<node>(q_gen_2764, q_gen_2770, q_gen_2752) -> q_gen_2788
<node>(q_gen_2764, q_gen_2752, q_gen_2752) -> q_gen_2791
<s>(q_gen_2795) -> q_gen_2794
<s>(q_gen_2796) -> q_gen_2795
<s>(q_gen_2797) -> q_gen_2796
<s>(q_gen_2781) -> q_gen_2797
<node>(q_gen_2764, q_gen_2776, q_gen_2752) -> q_gen_2821
<node>(q_gen_2753, q_gen_2752, q_gen_2826) -> q_gen_2825
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2826
<node>(q_gen_2753, q_gen_2776, q_gen_2831) -> q_gen_2830
<node>(q_gen_2753, q_gen_2826, q_gen_2752) -> q_gen_2831
<node>(q_gen_2753, q_gen_2776, q_gen_2770) -> q_gen_2835
<node>(q_gen_2753, q_gen_2770, q_gen_2844) -> q_gen_2843
<node>(q_gen_2764, q_gen_2776, q_gen_2845) -> q_gen_2844
<node>(q_gen_2764, q_gen_2835, q_gen_2782) -> q_gen_2845
<node>(q_gen_2753, q_gen_2826, q_gen_2770) -> q_gen_2850
<node>(q_gen_2753, q_gen_2835, q_gen_2770) -> q_gen_2859
<node>(q_gen_2753, q_gen_2863, q_gen_2752) -> q_gen_2862
<node>(q_gen_2753, q_gen_2791, q_gen_2864) -> q_gen_2863
<node>(q_gen_2753, q_gen_2791, q_gen_2752) -> q_gen_2864
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2868
<node>(q_gen_2753, q_gen_2752, q_gen_2876) -> q_gen_2875
<node>(q_gen_2753, q_gen_2868, q_gen_2752) -> q_gen_2876
<node>(q_gen_2764, q_gen_2880, q_gen_2752) -> q_gen_2879
<node>(q_gen_2764, q_gen_2881, q_gen_2752) -> q_gen_2880
<node>(q_gen_2753, q_gen_2752, q_gen_2882) -> q_gen_2881
<node>(q_gen_2753, q_gen_2864, q_gen_2864) -> q_gen_2882
<node>(q_gen_2764, q_gen_2868, q_gen_2893) -> q_gen_2892
<node>(q_gen_2764, q_gen_2826, q_gen_2894) -> q_gen_2893
<node>(q_gen_2764, q_gen_2868, q_gen_2752) -> q_gen_2894
<node>(q_gen_2764, q_gen_2897, q_gen_2876) -> q_gen_2896
<node>(q_gen_2753, q_gen_2876, q_gen_2752) -> q_gen_2897
<node>(q_gen_2753, q_gen_2896, q_gen_2752) -> q_gen_2899
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2752, q_gen_2749) -> q_gen_2763
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2767
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2774
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2775
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2777
<node, s>(q_gen_2753, q_gen_2782, q_gen_2780) -> q_gen_2779
<leaf, s>(q_gen_2781) -> q_gen_2780
<node, s>(q_gen_2753, q_gen_2770, q_gen_2780) -> q_gen_2783
<node, s>(q_gen_2764, q_gen_2770, q_gen_2768) -> q_gen_2785
<node, s>(q_gen_2753, q_gen_2788, q_gen_2787) -> q_gen_2786
<node, s>(q_gen_2764, q_gen_2752, q_gen_2768) -> q_gen_2787
<node, s>(q_gen_2753, q_gen_2752, q_gen_2780) -> q_gen_2789
<node, s>(q_gen_2753, q_gen_2791, q_gen_2780) -> q_gen_2790
<node, s>(q_gen_2753, q_gen_2770, q_gen_2793) -> q_gen_2792
<leaf, s>(q_gen_2794) -> q_gen_2793
<node, s>(q_gen_2753, q_gen_2770, q_gen_2799) -> q_gen_2798
<node, s>(q_gen_2753, q_gen_2770, q_gen_2800) -> q_gen_2799
<node, s>(q_gen_2753, q_gen_2770, q_gen_2801) -> q_gen_2800
<node, s>(q_gen_2753, q_gen_2752, q_gen_2802) -> q_gen_2801
<node, s>(q_gen_2753, q_gen_2770, q_gen_2763) -> q_gen_2802
<node, s>(q_gen_2753, q_gen_2776, q_gen_2809) -> q_gen_2808
<node, s>(q_gen_2753, q_gen_2770, q_gen_2810) -> q_gen_2809
<node, s>(q_gen_2753, q_gen_2770, q_gen_2811) -> q_gen_2810
<node, s>(q_gen_2753, q_gen_2770, q_gen_2812) -> q_gen_2811
<node, s>(q_gen_2753, q_gen_2752, q_gen_2813) -> q_gen_2812
<node, s>(q_gen_2753, q_gen_2770, q_gen_2787) -> q_gen_2813
<node, s>(q_gen_2753, q_gen_2776, q_gen_2780) -> q_gen_2814
<node, s>(q_gen_2753, q_gen_2782, q_gen_2749) -> q_gen_2815
<node, s>(q_gen_2764, q_gen_2776, q_gen_2768) -> q_gen_2817
<node, s>(q_gen_2764, q_gen_2782, q_gen_2768) -> q_gen_2818
<node, s>(q_gen_2753, q_gen_2821, q_gen_2818) -> q_gen_2820
<node, s>(q_gen_2753, q_gen_2782, q_gen_2772) -> q_gen_2822
<node, s>(q_gen_2753, q_gen_2752, q_gen_2774) -> q_gen_2823
<node, s>(q_gen_2753, q_gen_2825, q_gen_2783) -> q_gen_2824
<node, s>(q_gen_2753, q_gen_2776, q_gen_2828) -> q_gen_2827
<node, s>(q_gen_2753, q_gen_2826, q_gen_2749) -> q_gen_2828
<node, s>(q_gen_2753, q_gen_2830, q_gen_2749) -> q_gen_2829
<node, s>(q_gen_2753, q_gen_2770, q_gen_2833) -> q_gen_2832
<node, s>(q_gen_2764, q_gen_2776, q_gen_2834) -> q_gen_2833
<node, s>(q_gen_2764, q_gen_2835, q_gen_2775) -> q_gen_2834
<node, s>(q_gen_2753, q_gen_2843, q_gen_2841) -> q_gen_2840
<node, s>(q_gen_2764, q_gen_2752, q_gen_2842) -> q_gen_2841
<leaf, s>(q_gen_2796) -> q_gen_2842
<node, s>(q_gen_2753, q_gen_2826, q_gen_2847) -> q_gen_2846
<node, s>(q_gen_2753, q_gen_2752, q_gen_2848) -> q_gen_2847
<leaf, s>(q_gen_2797) -> q_gen_2848
<node, s>(q_gen_2753, q_gen_2850, q_gen_2783) -> q_gen_2849
<node, s>(q_gen_2764, q_gen_2835, q_gen_2768) -> q_gen_2853
<node, s>(q_gen_2753, q_gen_2835, q_gen_2789) -> q_gen_2854
<node, s>(q_gen_2753, q_gen_2859, q_gen_2858) -> q_gen_2857
<node, s>(q_gen_2764, q_gen_2835, q_gen_2848) -> q_gen_2858
<node, s>(q_gen_2764, q_gen_2862, q_gen_2861) -> q_gen_2860
<node, s>(q_gen_2764, q_gen_2752, q_gen_2772) -> q_gen_2861
<node, s>(q_gen_2753, q_gen_2863, q_gen_2848) -> q_gen_2865
<node, s>(q_gen_2753, q_gen_2752, q_gen_2867) -> q_gen_2866
<node, s>(q_gen_2753, q_gen_2868, q_gen_2848) -> q_gen_2867
<node, s>(q_gen_2753, q_gen_2868, q_gen_2870) -> q_gen_2869
<node, s>(q_gen_2753, q_gen_2868, q_gen_2777) -> q_gen_2870
<node, s>(q_gen_2753, q_gen_2875, q_gen_2873) -> q_gen_2872
<node, s>(q_gen_2753, q_gen_2868, q_gen_2874) -> q_gen_2873
<node, s>(q_gen_2753, q_gen_2868, q_gen_2814) -> q_gen_2874
<node, s>(q_gen_2764, q_gen_2879, q_gen_2878) -> q_gen_2877
<node, s>(q_gen_2753, q_gen_2868, q_gen_2768) -> q_gen_2878
<node, s>(q_gen_2764, q_gen_2880, q_gen_2848) -> q_gen_2883
<node, s>(q_gen_2764, q_gen_2868, q_gen_2749) -> q_gen_2884
<node, s>(q_gen_2764, q_gen_2868, q_gen_2886) -> q_gen_2885
<node, s>(q_gen_2764, q_gen_2826, q_gen_2887) -> q_gen_2886
<node, s>(q_gen_2764, q_gen_2868, q_gen_2768) -> q_gen_2887
<node, s>(q_gen_2753, q_gen_2892, q_gen_2891) -> q_gen_2890
<node, s>(q_gen_2764, q_gen_2868, q_gen_2848) -> q_gen_2891
<node, s>(q_gen_2753, q_gen_2896, q_gen_2780) -> q_gen_2895
<node, s>(q_gen_2753, q_gen_2899, q_gen_2772) -> q_gen_2898
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_2747, q_gen_2750, q_gen_2754, q_gen_2755, q_gen_2756, q_gen_2757, q_gen_2761, q_gen_2773, q_gen_2784, q_gen_2816, q_gen_2851, q_gen_2852},
Q_f={},
Delta=
{
<z>() -> q_gen_2755
<s>(q_gen_2755) -> q_gen_2757
<z, z>() -> q_gen_2747
<s, s>(q_gen_2747) -> q_gen_2750
<z, s>(q_gen_2755) -> q_gen_2754
<s, z>(q_gen_2757) -> q_gen_2756
<s, z>(q_gen_2755) -> q_gen_2761
<s, s>(q_gen_2761) -> q_gen_2773
<s, s>(q_gen_2773) -> q_gen_2784
<s, s>(q_gen_2756) -> q_gen_2816
<s, s>(q_gen_2852) -> q_gen_2851
<s, s>(q_gen_2784) -> q_gen_2852
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_2748, q_gen_2758, q_gen_2759, q_gen_2760, q_gen_2762, q_gen_2765, q_gen_2766, q_gen_2778, q_gen_2803, q_gen_2804, q_gen_2805, q_gen_2806, q_gen_2807, q_gen_2819, q_gen_2836, q_gen_2837, q_gen_2838, q_gen_2839, q_gen_2855, q_gen_2856, q_gen_2871, q_gen_2888, q_gen_2889},
Q_f={},
Delta=
{
<s, s>(q_gen_2760) -> q_gen_2759
<z, z>() -> q_gen_2760
<s, s>(q_gen_2839) -> q_gen_2838
<s, s>(q_gen_2759) -> q_gen_2839
<z, z, z>() -> q_gen_2748
<s, z, s>(q_gen_2759) -> q_gen_2758
<s, s, s>(q_gen_2748) -> q_gen_2762
<z, s, s>(q_gen_2760) -> q_gen_2765
<s, z, s>(q_gen_2760) -> q_gen_2766
<s, s, s>(q_gen_2766) -> q_gen_2778
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, s>(q_gen_2805) -> q_gen_2804
<s, s, s>(q_gen_2806) -> q_gen_2805
<s, s, s>(q_gen_2807) -> q_gen_2806
<s, s, s>(q_gen_2778) -> q_gen_2807
<s, s, s>(q_gen_2762) -> q_gen_2819
<s, s, s>(q_gen_2837) -> q_gen_2836
<s, z, s>(q_gen_2838) -> q_gen_2837
<s, s, s>(q_gen_2856) -> q_gen_2855
<s, s, s>(q_gen_2758) -> q_gen_2856
<s, s, s>(q_gen_2855) -> q_gen_2871
<s, s, s>(q_gen_2889) -> q_gen_2888
<s, z, s>(q_gen_2839) -> q_gen_2889
}

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.004659 s (model generation: 0.004528,  model checking: 0.000131):

Model:
|_
{
depth -> 
{{{
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
}}}

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

Teacher's answer:
New clause system:
{
() -> depth([leaf, z]) -> 0
() -> leq([z, n2]) -> 0
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 0
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 0
(leq([n, m])) -> max([n, m, m]) -> 0
(not leq([n, m])) -> max([n, m, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: ((not leq([n, m])) -> max([n, m, n]), {
m -> z  ;  n -> z
})

-------------------------------------------
Step 1, which took 0.006390 s (model generation: 0.006087,  model checking: 0.000303):

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

}

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

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

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

-------------------------------------------
Step 2, which took 0.005176 s (model generation: 0.005098,  model checking: 0.000078):

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

}

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

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

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

})

-------------------------------------------
Step 3, which took 0.004487 s (model generation: 0.004348,  model checking: 0.000139):

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

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

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

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

-------------------------------------------
Step 4, which took 0.005639 s (model generation: 0.005504,  model checking: 0.000135):

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

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

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

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

-------------------------------------------
Step 5, which took 0.005245 s (model generation: 0.004816,  model checking: 0.000429):

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

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

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

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

-------------------------------------------
Step 6, which took 0.006610 s (model generation: 0.005938,  model checking: 0.000672):

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

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

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

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

-------------------------------------------
Step 7, which took 0.006868 s (model generation: 0.005908,  model checking: 0.000960):

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

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

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

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

-------------------------------------------
Step 8, which took 0.005242 s (model generation: 0.005045,  model checking: 0.000197):

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

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

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

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

-------------------------------------------
Step 9, which took 0.005608 s (model generation: 0.005316,  model checking: 0.000292):

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

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

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

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

-------------------------------------------
Step 10, which took 0.006159 s (model generation: 0.005118,  model checking: 0.001041):

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

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

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

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

-------------------------------------------
Step 11, which took 0.006737 s (model generation: 0.005466,  model checking: 0.001271):

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

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

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

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

-------------------------------------------
Step 12, which took 0.008330 s (model generation: 0.006835,  model checking: 0.001495):

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

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

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

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

-------------------------------------------
Step 13, which took 0.007332 s (model generation: 0.006000,  model checking: 0.001332):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2769},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<leaf, s>(q_gen_2769) -> q_gen_2749
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
}

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

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

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

-------------------------------------------
Step 14, which took 0.007995 s (model generation: 0.007411,  model checking: 0.000584):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2769},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<leaf, s>(q_gen_2769) -> q_gen_2749
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
}

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

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

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

-------------------------------------------
Step 15, which took 0.014679 s (model generation: 0.007449,  model checking: 0.007230):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
}

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

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

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

-------------------------------------------
Step 16, which took 0.024707 s (model generation: 0.008060,  model checking: 0.016647):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
}

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

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

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

-------------------------------------------
Step 17, which took 0.012577 s (model generation: 0.008308,  model checking: 0.004269):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
}

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

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

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

-------------------------------------------
Step 18, which took 0.050730 s (model generation: 0.009360,  model checking: 0.041370):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2769, q_gen_2770, q_gen_2772},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<leaf, z>() -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
}

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

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

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

-------------------------------------------
Step 19, which took 0.011588 s (model generation: 0.010570,  model checking: 0.001018):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2769, q_gen_2770, q_gen_2772},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<leaf, z>() -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
}

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

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

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

-------------------------------------------
Step 20, which took 0.011525 s (model generation: 0.010931,  model checking: 0.000594):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2767, q_gen_2769},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2767
<node, s>(q_gen_2753, q_gen_2752, q_gen_2767) -> q_gen_2767
}

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  max -> 
{{{
Q={q_gen_2748, q_gen_2759, q_gen_2760, q_gen_2766},
Q_f={q_gen_2748},
Delta=
{
<s, s>(q_gen_2760) -> q_gen_2759
<z, z>() -> q_gen_2760
<s, s, s>(q_gen_2748) -> q_gen_2748
<s, z, s>(q_gen_2759) -> q_gen_2748
<z, s, s>(q_gen_2760) -> q_gen_2748
<z, z, z>() -> q_gen_2748
<s, s, s>(q_gen_2766) -> q_gen_2766
<s, z, s>(q_gen_2760) -> q_gen_2766
}

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

-------------------------------------------
Step 21, which took 0.016462 s (model generation: 0.010133,  model checking: 0.006329):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 14
() -> leq([z, n2]) -> 14
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 19
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 22
(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)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16
(leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 22, which took 0.012288 s (model generation: 0.011653,  model checking: 0.000635):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 15
() -> leq([z, n2]) -> 15
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 19
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 22
(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]) -> 19
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 23, which took 0.133823 s (model generation: 0.010973,  model checking: 0.122850):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 16
() -> leq([z, n2]) -> 16
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 22
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 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]) -> 20
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(z))  ;  _gn -> s(z)  ;  _hn -> s(s(z))  ;  e -> b  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 24, which took 0.016065 s (model generation: 0.013871,  model checking: 0.002194):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 17
() -> leq([z, n2]) -> 17
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 22
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 25
(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]) -> 21
(leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 25, which took 0.062512 s (model generation: 0.015267,  model checking: 0.047245):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2776, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2776, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2776, q_gen_2772) -> q_gen_2751
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 18
() -> leq([z, n2]) -> 18
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 25
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 25
(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]) -> 22
(leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(z))  ;  _gn -> s(z)  ;  _hn -> s(s(z))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 26, which took 0.384915 s (model generation: 0.016252,  model checking: 0.368663):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2764, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<b>() -> q_gen_2753
<a>() -> q_gen_2764
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2764, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<node>(q_gen_2764, q_gen_2752, q_gen_2752) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2764, q_gen_2752, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2752, q_gen_2749) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2764, q_gen_2770, q_gen_2768) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 19
() -> leq([z, n2]) -> 19
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 28
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 26
(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]) -> 23
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(s(s(s(s(z)))))))  ;  _gn -> s(s(s(s(s(s(z))))))  ;  _hn -> s(s(s(s(s(s(s(z)))))))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(b, leaf, node(b, node(b, leaf, leaf), node(a, leaf, leaf))))))
})

-------------------------------------------
Step 27, which took 0.056770 s (model generation: 0.042703,  model checking: 0.014067):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2776, q_gen_2781},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2771) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2771) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2771
}

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

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

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:
{
() -> depth([leaf, z]) -> 20
() -> leq([z, n2]) -> 20
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 28
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 29
(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]) -> 24
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 28, which took 0.165659 s (model generation: 0.043271,  model checking: 0.122388):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2776, q_gen_2781},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2771) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2771) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2771
}

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

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

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:
{
() -> depth([leaf, z]) -> 21
() -> leq([z, n2]) -> 21
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 31
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 29
(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]) -> 25
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(z))  ;  _gn -> s(s(z))  ;  _hn -> s(s(z))  ;  e -> b  ;  t1 -> node(a, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> node(a, node(b, node(b, node(b, leaf, leaf), leaf), leaf), leaf)
})

-------------------------------------------
Step 29, which took 0.100447 s (model generation: 0.079804,  model checking: 0.020643):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2776, q_gen_2781},
Q_f={q_gen_2749, q_gen_2768},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2771) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2771
}

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

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

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:
{
() -> depth([leaf, z]) -> 22
() -> leq([z, n2]) -> 22
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 31
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 32
(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]) -> 26
(leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 30, which took 0.069278 s (model generation: 0.065714,  model checking: 0.003564):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2767, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2776, q_gen_2781},
Q_f={q_gen_2749, q_gen_2767},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2767
<node, s>(q_gen_2753, q_gen_2770, q_gen_2767) -> q_gen_2767
<node, s>(q_gen_2753, q_gen_2776, q_gen_2767) -> q_gen_2767
<node, s>(q_gen_2753, q_gen_2776, q_gen_2771) -> q_gen_2767
<leaf, s>(q_gen_2781) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2767) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2771
}

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

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

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:
{
() -> depth([leaf, z]) -> 23
() -> leq([z, n2]) -> 23
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 34
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 32
(leq([n, m])) -> max([n, m, m]) -> 24
(not leq([n, m])) -> max([n, m, n]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(z)  ;  _gn -> s(z)  ;  _hn -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 31, which took 0.089610 s (model generation: 0.064590,  model checking: 0.025020):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776, q_gen_2779, q_gen_2781},
Q_f={q_gen_2749},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2749
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2779) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2779
<node, s>(q_gen_2753, q_gen_2770, q_gen_2779) -> q_gen_2779
<node, s>(q_gen_2753, q_gen_2776, q_gen_2779) -> q_gen_2779
}

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

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

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:
{
() -> depth([leaf, z]) -> 24
() -> leq([z, n2]) -> 24
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 34
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 35
(leq([n, m])) -> max([n, m, m]) -> 25
(not leq([n, m])) -> max([n, m, n]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(z))  ;  _mn -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 32, which took 0.778313 s (model generation: 0.064215,  model checking: 0.714098):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2780, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2780) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2780
<node, s>(q_gen_2753, q_gen_2752, q_gen_2780) -> q_gen_2780
}

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

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

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:
{
() -> depth([leaf, z]) -> 25
() -> leq([z, n2]) -> 25
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 37
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 35
(leq([n, m])) -> max([n, m, m]) -> 26
(not leq([n, m])) -> max([n, m, n]) -> 27
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(z)))  ;  _gn -> s(s(z))  ;  _hn -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, leaf, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 33, which took 0.098251 s (model generation: 0.080761,  model checking: 0.017490):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 26
() -> leq([z, n2]) -> 26
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 37
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 38
(leq([n, m])) -> max([n, m, m]) -> 27
(not leq([n, m])) -> max([n, m, n]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(z))  ;  _mn -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 34, which took 0.592773 s (model generation: 0.090620,  model checking: 0.502153):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 27
() -> leq([z, n2]) -> 27
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 40
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 38
(leq([n, m])) -> max([n, m, m]) -> 28
(not leq([n, m])) -> max([n, m, n]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 28
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(s(s(z)))))  ;  _gn -> s(z)  ;  _hn -> s(s(s(s(s(z)))))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), node(a, node(b, node(b, leaf, leaf), leaf), node(a, node(b, node(b, node(b, leaf, leaf), leaf), node(b, leaf, leaf)), node(b, node(b, node(b, leaf, leaf), leaf), leaf))))  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 35, which took 0.172163 s (model generation: 0.130611,  model checking: 0.041552):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2780, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2780) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2780) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2780
}

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

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

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:
{
() -> depth([leaf, z]) -> 28
() -> leq([z, n2]) -> 28
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 40
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 41
(leq([n, m])) -> max([n, m, m]) -> 29
(not leq([n, m])) -> max([n, m, n]) -> 30
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 29
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(s(s(z)))))  ;  _mn -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, leaf))  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 36, which took 0.341251 s (model generation: 0.158999,  model checking: 0.182252):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 29
() -> leq([z, n2]) -> 29
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 43
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 41
(leq([n, m])) -> max([n, m, m]) -> 30
(not leq([n, m])) -> max([n, m, n]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 30
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(s(z))))  ;  _gn -> s(s(z))  ;  _hn -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, node(b, leaf, leaf), leaf), node(b, leaf, leaf)), node(b, leaf, leaf))  ;  t2 -> node(a, node(b, node(b, node(b, leaf, leaf), leaf), node(b, leaf, leaf)), leaf)
})

-------------------------------------------
Step 37, which took 0.497266 s (model generation: 0.246533,  model checking: 0.250733):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2764, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2776) -> q_gen_2752
<node>(q_gen_2764, q_gen_2776, q_gen_2752) -> q_gen_2752
<b>() -> q_gen_2753
<a>() -> q_gen_2764
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2776) -> q_gen_2770
<node>(q_gen_2764, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2770) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2776) -> q_gen_2776
<node>(q_gen_2764, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2764, q_gen_2776, q_gen_2776) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2776, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2776, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2764, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2764, q_gen_2770, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2764, q_gen_2776, q_gen_2751) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 30
() -> leq([z, n2]) -> 30
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 43
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 44
(leq([n, m])) -> max([n, m, m]) -> 31
(not leq([n, m])) -> max([n, m, n]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 31
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(s(z))))  ;  _mn -> s(s(s(z)))  ;  e -> a  ;  t1 -> node(b, node(b, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf)), leaf)  ;  t2 -> node(a, leaf, node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 38, which took 2.154366 s (model generation: 0.252416,  model checking: 1.901950):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 31
() -> leq([z, n2]) -> 31
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 46
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 44
(leq([n, m])) -> max([n, m, m]) -> 32
(not leq([n, m])) -> max([n, m, n]) -> 33
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35
(leq([s(nn1), z])) -> BOT -> 32
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(s(s(z)))))  ;  _gn -> s(s(s(z)))  ;  _hn -> s(s(s(s(s(z)))))  ;  e -> b  ;  t1 -> node(b, leaf, node(b, node(b, leaf, node(b, leaf, leaf)), leaf))  ;  t2 -> node(b, node(b, leaf, node(b, leaf, leaf)), node(b, node(b, leaf, node(b, leaf, leaf)), node(b, node(b, node(b, leaf, leaf), leaf), leaf)))
})

-------------------------------------------
Step 39, which took 0.950208 s (model generation: 0.343465,  model checking: 0.606743):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2764, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2764, q_gen_2776, q_gen_2752) -> q_gen_2752
<b>() -> q_gen_2753
<a>() -> q_gen_2764
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2776) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2776
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2776
<node>(q_gen_2753, q_gen_2770, q_gen_2776) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2770) -> q_gen_2776
<node>(q_gen_2753, q_gen_2776, q_gen_2776) -> q_gen_2776
<node>(q_gen_2764, q_gen_2752, q_gen_2752) -> q_gen_2776
<node>(q_gen_2764, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2764, q_gen_2776, q_gen_2776) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2764, q_gen_2752, q_gen_2749) -> q_gen_2749
<node, s>(q_gen_2764, q_gen_2776, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2764, q_gen_2776, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2751) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2764, q_gen_2770, q_gen_2768) -> q_gen_2768
}

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

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

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:
{
() -> depth([leaf, z]) -> 32
() -> leq([z, n2]) -> 32
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 46
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 47
(leq([n, m])) -> max([n, m, m]) -> 33
(not leq([n, m])) -> max([n, m, n]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 36
(leq([s(nn1), z])) -> BOT -> 33
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(s(z))))  ;  _mn -> s(s(s(z)))  ;  e -> a  ;  t1 -> node(a, node(a, node(b, leaf, node(b, node(b, node(a, leaf, leaf), leaf), node(b, node(a, leaf, leaf), leaf))), leaf), leaf)  ;  t2 -> node(b, node(b, leaf, node(b, leaf, leaf)), leaf)
})

-------------------------------------------
Step 40, which took 0.595567 s (model generation: 0.507122,  model checking: 0.088445):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2772, q_gen_2781},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<s>(q_gen_2769) -> q_gen_2781
<s>(q_gen_2781) -> q_gen_2781
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2772) -> q_gen_2768
<leaf, s>(q_gen_2781) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2752, q_gen_2772) -> q_gen_2772
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2772
}

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

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

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:
{
() -> depth([leaf, z]) -> 33
() -> leq([z, n2]) -> 33
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 49
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 47
(leq([n, m])) -> max([n, m, m]) -> 34
(not leq([n, m])) -> max([n, m, n]) -> 35
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37
(leq([s(nn1), z])) -> BOT -> 34
}
Sat witness: Found: ((depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]), {
_fn -> s(s(s(s(z))))  ;  _gn -> s(z)  ;  _hn -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(a, node(b, leaf, node(b, leaf, leaf)), node(a, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), node(a, node(b, leaf, node(b, leaf, leaf)), leaf)))  ;  t2 -> node(a, node(b, leaf, node(b, leaf, leaf)), leaf)
})

-------------------------------------------
Step 41, which took 0.736832 s (model generation: 0.629687,  model checking: 0.107145):

Model:
|_
{
depth -> 
{{{
Q={q_gen_2749, q_gen_2751, q_gen_2752, q_gen_2753, q_gen_2768, q_gen_2769, q_gen_2770, q_gen_2771, q_gen_2776},
Q_f={q_gen_2749, q_gen_2751},
Delta=
{
<leaf>() -> q_gen_2752
<node>(q_gen_2753, q_gen_2776, q_gen_2752) -> q_gen_2752
<a>() -> q_gen_2753
<b>() -> q_gen_2753
<s>(q_gen_2769) -> q_gen_2769
<z>() -> q_gen_2769
<node>(q_gen_2753, q_gen_2752, q_gen_2752) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2770) -> q_gen_2770
<node>(q_gen_2753, q_gen_2752, q_gen_2776) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2770) -> q_gen_2770
<node>(q_gen_2753, q_gen_2776, q_gen_2770) -> q_gen_2770
<node>(q_gen_2753, q_gen_2776, q_gen_2776) -> q_gen_2770
<node>(q_gen_2753, q_gen_2770, q_gen_2752) -> q_gen_2776
<node>(q_gen_2753, q_gen_2770, q_gen_2776) -> q_gen_2776
<leaf, z>() -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2770, q_gen_2751) -> q_gen_2749
<node, s>(q_gen_2753, q_gen_2752, q_gen_2749) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2770, q_gen_2768) -> q_gen_2751
<node, s>(q_gen_2753, q_gen_2776, q_gen_2771) -> q_gen_2751
<leaf, s>(q_gen_2769) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2770, q_gen_2771) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2749) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2776, q_gen_2768) -> q_gen_2768
<node, s>(q_gen_2753, q_gen_2752, q_gen_2751) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2768) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2752, q_gen_2771) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2770, q_gen_2749) -> q_gen_2771
<node, s>(q_gen_2753, q_gen_2776, q_gen_2751) -> q_gen_2771
}

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

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

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:
{
() -> depth([leaf, z]) -> 34
() -> leq([z, n2]) -> 34
(depth([t1, _fn]) /\ depth([t2, _gn]) /\ max([_fn, _gn, _hn])) -> depth([node(e, t1, t2), s(_hn)]) -> 49
(depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]) -> 50
(leq([n, m])) -> max([n, m, m]) -> 35
(not leq([n, m])) -> max([n, m, n]) -> 36
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38
(leq([s(nn1), z])) -> BOT -> 35
}
Sat witness: Found: ((depth([t1, _ln]) /\ depth([node(e, t1, t2), _mn])) -> leq([_ln, _mn]), {
_ln -> s(s(s(z)))  ;  _mn -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(a, node(b, node(b, node(b, leaf, node(b, leaf, leaf)), leaf), leaf), node(b, node(b, leaf, node(b, leaf, leaf)), leaf)), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

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