Solving ../../benchmarks/true/isaplanner_prop79.smt2...

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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(minus, F:
{() -> minus([s(u), z, s(u)])
() -> minus([z, y, z])
(minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa])}
(minus([_qaa, _raa, _saa]) /\ minus([_qaa, _raa, _taa])) -> eq_nat([_saa, _taa])
)
}

properties:
{(minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa])}


over-approximation: {minus}
under-approximation: {}

Clause system for inference is:

{
() -> minus([s(u), z, s(u)]) -> 0  ;  () -> minus([z, y, z]) -> 0  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 0  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 0
}


Solving took 30.881163 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
minus -> 
{{{
Q={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_2803, q_gen_2804, q_gen_2805, q_gen_2806, q_gen_2807, 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_2816, q_gen_2817, q_gen_2818, q_gen_2819, 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_2836, q_gen_2837, q_gen_2838, q_gen_2839, 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_2851, q_gen_2852, q_gen_2853, q_gen_2854, q_gen_2855, q_gen_2856, 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_2871, 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_2888, q_gen_2889, 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_gen_2900, q_gen_2901, q_gen_2902, q_gen_2903, q_gen_2904, q_gen_2905, q_gen_2906, q_gen_2907, q_gen_2908, q_gen_2909, q_gen_2910, q_gen_2911, q_gen_2912, q_gen_2913, q_gen_2914, q_gen_2915, q_gen_2916, q_gen_2917, q_gen_2918, q_gen_2919, q_gen_2920},
Q_f={},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2877
<z, z>() -> q_gen_2796
<s, s>(q_gen_2796) -> q_gen_2801
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2812
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2817) -> q_gen_2840
<s, s>(q_gen_2801) -> q_gen_2846
<z, s>(q_gen_2817) -> q_gen_2848
<s, z>(q_gen_2806) -> q_gen_2852
<s, s>(q_gen_2808) -> q_gen_2859
<s, s>(q_gen_2838) -> q_gen_2871
<s, s>(q_gen_2846) -> q_gen_2879
<z, s>(q_gen_2877) -> q_gen_2885
<s, s>(q_gen_2891) -> q_gen_2890
<s, s>(q_gen_2812) -> q_gen_2891
<s, s>(q_gen_2879) -> q_gen_2902
<s, z>(q_gen_2877) -> q_gen_2906
<s, s>(q_gen_2906) -> q_gen_2910
<s, s>(q_gen_2852) -> q_gen_2920
<z, z, z>() -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, s, z>(q_gen_2796) -> q_gen_2797
<z, s, z>(q_gen_2799) -> q_gen_2798
<s, z, s>(q_gen_2801) -> q_gen_2800
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<z, s, z>(q_gen_2806) -> q_gen_2805
<s, s, z>(q_gen_2808) -> q_gen_2807
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, s, s>(q_gen_2811) -> q_gen_2810
<s, z, s>(q_gen_2812) -> q_gen_2811
<s, s, s>(q_gen_2814) -> q_gen_2813
<s, s, s>(q_gen_2809) -> q_gen_2814
<s, z, z>(q_gen_2806) -> q_gen_2815
<z, s, z>(q_gen_2817) -> q_gen_2816
<s, s, s>(q_gen_2819) -> q_gen_2818
<s, s, z>(q_gen_2820) -> q_gen_2819
<s, s, s>(q_gen_2818) -> q_gen_2821
<s, s, s>(q_gen_2823) -> q_gen_2822
<s, s, z>(q_gen_2801) -> q_gen_2823
<s, s, s>(q_gen_2797) -> q_gen_2824
<s, s, s>(q_gen_2804) -> q_gen_2825
<s, s, s>(q_gen_2824) -> q_gen_2826
<s, s, s>(q_gen_2815) -> q_gen_2827
<s, s, s>(q_gen_2829) -> q_gen_2828
<s, z, s>(q_gen_2820) -> q_gen_2829
<s, s, s>(q_gen_2827) -> q_gen_2830
<s, s, s>(q_gen_2832) -> q_gen_2831
<s, s, s>(q_gen_2798) -> q_gen_2832
<s, s, s>(q_gen_2834) -> q_gen_2833
<s, s, s>(q_gen_2795) -> q_gen_2834
<s, s, s>(q_gen_2836) -> q_gen_2835
<s, s, s>(q_gen_2802) -> q_gen_2836
<s, s, z>(q_gen_2838) -> q_gen_2837
<s, s, z>(q_gen_2840) -> q_gen_2839
<s, s, z>(q_gen_2812) -> q_gen_2841
<s, s, s>(q_gen_2843) -> q_gen_2842
<s, z, s>(q_gen_2838) -> q_gen_2843
<s, s, s>(q_gen_2837) -> q_gen_2844
<s, z, s>(q_gen_2846) -> q_gen_2845
<s, z, s>(q_gen_2848) -> q_gen_2847
<s, s, s>(q_gen_2850) -> q_gen_2849
<s, s, s>(q_gen_2851) -> q_gen_2850
<s, z, s>(q_gen_2852) -> q_gen_2851
<s, s, z>(q_gen_2852) -> q_gen_2853
<s, s, s>(q_gen_2855) -> q_gen_2854
<s, s, s>(q_gen_2807) -> q_gen_2855
<s, s, s>(q_gen_2857) -> q_gen_2856
<s, s, s>(q_gen_2858) -> q_gen_2857
<s, s, z>(q_gen_2859) -> q_gen_2858
<s, s, s>(q_gen_2825) -> q_gen_2860
<s, s, s>(q_gen_2862) -> q_gen_2861
<s, s, s>(q_gen_2853) -> q_gen_2862
<s, s, s>(q_gen_2864) -> q_gen_2863
<s, z, s>(q_gen_2859) -> q_gen_2864
<s, s, s>(q_gen_2866) -> q_gen_2865
<s, z, z>(q_gen_2817) -> q_gen_2866
<s, s, s>(q_gen_2868) -> q_gen_2867
<s, s, s>(q_gen_2865) -> q_gen_2868
<s, s, s>(q_gen_2870) -> q_gen_2869
<s, z, s>(q_gen_2871) -> q_gen_2870
<s, s, s>(q_gen_2849) -> q_gen_2872
<s, s, s>(q_gen_2867) -> q_gen_2873
<s, s, s>(q_gen_2861) -> q_gen_2874
<s, s, s>(q_gen_2844) -> q_gen_2875
<z, s, z>(q_gen_2877) -> q_gen_2876
<s, z, s>(q_gen_2879) -> q_gen_2878
<s, s, s>(q_gen_2839) -> q_gen_2880
<s, s, s>(q_gen_2842) -> q_gen_2881
<s, s, s>(q_gen_2883) -> q_gen_2882
<s, s, s>(q_gen_2884) -> q_gen_2883
<s, z, s>(q_gen_2885) -> q_gen_2884
<s, s, s>(q_gen_2887) -> q_gen_2886
<s, s, s>(q_gen_2888) -> q_gen_2887
<s, s, s>(q_gen_2847) -> q_gen_2888
<s, s, z>(q_gen_2890) -> q_gen_2889
<s, s, s>(q_gen_2893) -> q_gen_2892
<s, s, z>(q_gen_2848) -> q_gen_2893
<s, s, s>(q_gen_2895) -> q_gen_2894
<s, s, s>(q_gen_2896) -> q_gen_2895
<s, z, s>(q_gen_2840) -> q_gen_2896
<s, s, s>(q_gen_2898) -> q_gen_2897
<s, s, s>(q_gen_2899) -> q_gen_2898
<s, s, s>(q_gen_2900) -> q_gen_2899
<s, z, z>(q_gen_2877) -> q_gen_2900
<s, s, z>(q_gen_2902) -> q_gen_2901
<s, s, s>(q_gen_2904) -> q_gen_2903
<s, s, s>(q_gen_2831) -> q_gen_2904
<s, s, z>(q_gen_2906) -> q_gen_2905
<s, s, z>(q_gen_2885) -> q_gen_2907
<s, s, s>(q_gen_2909) -> q_gen_2908
<s, s, z>(q_gen_2910) -> q_gen_2909
<s, s, s>(q_gen_2880) -> q_gen_2911
<s, s, s>(q_gen_2813) -> q_gen_2912
<s, s, s>(q_gen_2914) -> q_gen_2913
<s, s, s>(q_gen_2833) -> q_gen_2914
<s, s, s>(q_gen_2916) -> q_gen_2915
<s, s, s>(q_gen_2905) -> q_gen_2916
<s, s, s>(q_gen_2918) -> q_gen_2917
<s, s, s>(q_gen_2919) -> q_gen_2918
<s, z, s>(q_gen_2920) -> q_gen_2919
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010324 s (model generation: 0.009980,  model checking: 0.000344):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 0  ;  () -> minus([z, y, z]) -> 3  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 1  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 1
}
Sat witness: Yes: (() -> minus([z, y, z]), {
y -> z
})

-------------------------------------------
Step 1, which took 0.010442 s (model generation: 0.010181,  model checking: 0.000261):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794},
Q_f={q_gen_2794},
Delta=
{
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 3  ;  () -> minus([z, y, z]) -> 3  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 1  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 1
}
Sat witness: Yes: (() -> minus([s(u), z, s(u)]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.010889 s (model generation: 0.010795,  model checking: 0.000094):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796},
Q_f={q_gen_2794},
Delta=
{
<z, z>() -> q_gen_2796
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 3  ;  () -> minus([z, y, z]) -> 3  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 1  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 4
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> z  ;  x2 -> z
})

-------------------------------------------
Step 3, which took 0.008108 s (model generation: 0.006787,  model checking: 0.001321):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796},
Q_f={q_gen_2794},
Delta=
{
<z, z>() -> q_gen_2796
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 3  ;  () -> minus([z, y, z]) -> 6  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 2  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 4
}
Sat witness: Yes: (() -> minus([z, y, z]), {
y -> s(z)
})

-------------------------------------------
Step 4, which took 0.004293 s (model generation: 0.004151,  model checking: 0.000142):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<z, z>() -> q_gen_2796
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 6  ;  () -> minus([z, y, z]) -> 6  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 3  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 4
}
Sat witness: Yes: (() -> minus([s(u), z, s(u)]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.004023 s (model generation: 0.003810,  model checking: 0.000213):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 6  ;  () -> minus([z, y, z]) -> 6  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 4  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 7
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(z)  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 6, which took 0.005244 s (model generation: 0.004172,  model checking: 0.001072):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s, s>(q_gen_2794) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 6  ;  () -> minus([z, y, z]) -> 6  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 7  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 7
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> s(z)  ;  _waa -> z  ;  _xaa -> z  ;  k -> z  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 7, which took 0.004249 s (model generation: 0.004119,  model checking: 0.000130):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 6  ;  () -> minus([z, y, z]) -> 9  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 7  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 7
}
Sat witness: Yes: (() -> minus([z, y, z]), {
y -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.005122 s (model generation: 0.004830,  model checking: 0.000292):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 7  ;  () -> minus([z, y, z]) -> 9  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 7  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 10
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> z  ;  x2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.005064 s (model generation: 0.004618,  model checking: 0.000446):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 7  ;  () -> minus([z, y, z]) -> 9  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 10  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 10
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> s(z)  ;  _waa -> z  ;  _xaa -> z  ;  k -> z  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 10, which took 0.005383 s (model generation: 0.005106,  model checking: 0.000277):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2808},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 8  ;  () -> minus([z, y, z]) -> 10  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 10  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 13
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 11, which took 0.007052 s (model generation: 0.006113,  model checking: 0.000939):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2804, q_gen_2808},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2795) -> q_gen_2795
<s, s, z>(q_gen_2796) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 9  ;  () -> minus([z, y, z]) -> 10  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 13  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 13
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.006418 s (model generation: 0.006229,  model checking: 0.000189):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, s>(q_gen_2806) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, z>(q_gen_2806) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 10  ;  () -> minus([z, y, z]) -> 13  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 13  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 13
}
Sat witness: Yes: (() -> minus([z, y, z]), {
y -> s(s(s(z)))
})

-------------------------------------------
Step 13, which took 0.007103 s (model generation: 0.006693,  model checking: 0.000410):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2808, q_gen_2809},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 11  ;  () -> minus([z, y, z]) -> 13  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 13  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 16
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(z)  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 14, which took 0.008948 s (model generation: 0.007816,  model checking: 0.001132):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2797, q_gen_2799, q_gen_2803, q_gen_2808},
Q_f={q_gen_2794, q_gen_2797},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2797) -> q_gen_2797
<s, s, s>(q_gen_2803) -> q_gen_2797
<s, s, z>(q_gen_2796) -> q_gen_2797
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 12  ;  () -> minus([z, y, z]) -> 13  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 16  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 16
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> s(z)  ;  _waa -> s(z)  ;  _xaa -> z  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 15, which took 0.011188 s (model generation: 0.010856,  model checking: 0.000332):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2797, q_gen_2799, q_gen_2803, q_gen_2808},
Q_f={q_gen_2794, q_gen_2797},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2797) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2797
<s, s, z>(q_gen_2796) -> q_gen_2797
<z, s, z>(q_gen_2799) -> q_gen_2797
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 13  ;  () -> minus([z, y, z]) -> 14  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 16  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 19
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(z))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 16, which took 0.013262 s (model generation: 0.012885,  model checking: 0.000377):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2802, q_gen_2803, q_gen_2808},
Q_f={q_gen_2794, q_gen_2802},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2802) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, s, z>(q_gen_2808) -> q_gen_2802
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 14  ;  () -> minus([z, y, z]) -> 15  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 19  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 19
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> z  ;  _waa -> s(s(s(z)))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 17, which took 0.015393 s (model generation: 0.014996,  model checking: 0.000397):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2804, q_gen_2806, q_gen_2808},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s, z>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2795) -> q_gen_2795
<s, s, z>(q_gen_2808) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2806) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 15  ;  () -> minus([z, y, z]) -> 16  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 19  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 22
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(z))  ;  x2 -> z
})

-------------------------------------------
Step 18, which took 0.017270 s (model generation: 0.016808,  model checking: 0.000462):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2804, q_gen_2806, q_gen_2808},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s, s>(q_gen_2795) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2795
<s, s, z>(q_gen_2808) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2806) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 16  ;  () -> minus([z, y, z]) -> 17  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 22  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 22
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> z  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.017187 s (model generation: 0.016590,  model checking: 0.000597):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 17  ;  () -> minus([z, y, z]) -> 18  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 22  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 25
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(s(z)))  ;  x2 -> s(z)
})

-------------------------------------------
Step 20, which took 0.019377 s (model generation: 0.017829,  model checking: 0.001548):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2802, q_gen_2803, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2802},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2802) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, s, z>(q_gen_2820) -> q_gen_2802
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 18  ;  () -> minus([z, y, z]) -> 19  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 25  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 25
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> s(s(z))  ;  _waa -> s(s(z))  ;  _xaa -> z  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 21, which took 0.022605 s (model generation: 0.022112,  model checking: 0.000493):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2798, q_gen_2799, q_gen_2803, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2798},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2798) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2798
<s, s, z>(q_gen_2820) -> q_gen_2798
<z, s, z>(q_gen_2799) -> q_gen_2798
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 19  ;  () -> minus([z, y, z]) -> 20  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 25  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 28
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(z)))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 22, which took 0.038986 s (model generation: 0.033466,  model checking: 0.005520):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2802, q_gen_2803, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2802},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2802) -> q_gen_2802
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 20  ;  () -> minus([z, y, z]) -> 21  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 28  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 28
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(s(z))  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 23, which took 0.043354 s (model generation: 0.042990,  model checking: 0.000364):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2798, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2815},
Q_f={q_gen_2794, q_gen_2798},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, s>(q_gen_2806) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2798) -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2798
<z, s, z>(q_gen_2799) -> q_gen_2798
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 21  ;  () -> minus([z, y, z]) -> 22  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 28  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 31
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 24, which took 0.030299 s (model generation: 0.029462,  model checking: 0.000837):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2798, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2815},
Q_f={q_gen_2794, q_gen_2798},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2796
<z, s>(q_gen_2806) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, z>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<s, s, s>(q_gen_2798) -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2798
<z, s, z>(q_gen_2799) -> q_gen_2798
<z, s, z>(q_gen_2806) -> q_gen_2798
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 22  ;  () -> minus([z, y, z]) -> 23  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 31  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 31
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 25, which took 0.030579 s (model generation: 0.030127,  model checking: 0.000452):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2812},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s>(q_gen_2812) -> q_gen_2812
<s, z>(q_gen_2799) -> q_gen_2812
<z, s>(q_gen_2806) -> q_gen_2812
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2812) -> q_gen_2803
<s, z, s>(q_gen_2812) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 23  ;  () -> minus([z, y, z]) -> 24  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 31  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 34
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> z  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 26, which took 0.036728 s (model generation: 0.035506,  model checking: 0.001222):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2795) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 24  ;  () -> minus([z, y, z]) -> 25  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 34  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 34
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(s(z))  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 27, which took 0.039242 s (model generation: 0.038400,  model checking: 0.000842):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2820) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 25  ;  () -> minus([z, y, z]) -> 26  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 34  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 37
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(z)  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 28, which took 0.046447 s (model generation: 0.045711,  model checking: 0.000736):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2820) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2795) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, s, z>(q_gen_2808) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 26  ;  () -> minus([z, y, z]) -> 27  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 37  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 37
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 29, which took 0.049208 s (model generation: 0.048679,  model checking: 0.000529):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, s>(q_gen_2806) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 27  ;  () -> minus([z, y, z]) -> 28  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 37  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 40
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 30, which took 0.057786 s (model generation: 0.056535,  model checking: 0.001251):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, s>(q_gen_2806) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 28  ;  () -> minus([z, y, z]) -> 29  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 40  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 40
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(z)  ;  _waa -> z  ;  _xaa -> z  ;  k -> s(z)  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 31, which took 0.051440 s (model generation: 0.050695,  model checking: 0.000745):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 29  ;  () -> minus([z, y, z]) -> 30  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 40  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 43
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(z)))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(z)
})

-------------------------------------------
Step 32, which took 0.078104 s (model generation: 0.076671,  model checking: 0.001433):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, z>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 30  ;  () -> minus([z, y, z]) -> 31  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 43  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 43
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 33, which took 0.085446 s (model generation: 0.084888,  model checking: 0.000558):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2810, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2795) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2810) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2810
<s, s, z>(q_gen_2820) -> q_gen_2810
<s, z, s>(q_gen_2820) -> q_gen_2810
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 31  ;  () -> minus([z, y, z]) -> 32  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 43  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 46
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 34, which took 0.081890 s (model generation: 0.081155,  model checking: 0.000735):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2808, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, s, s>(q_gen_2795) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 32  ;  () -> minus([z, y, z]) -> 33  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 46  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 46
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(z)  ;  _waa -> s(s(z))  ;  _xaa -> s(s(z))  ;  k -> z  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 35, which took 0.091505 s (model generation: 0.090613,  model checking: 0.000892):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2795) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 33  ;  () -> minus([z, y, z]) -> 34  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 46  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 49
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(s(s(z))))
})

-------------------------------------------
Step 36, which took 0.111737 s (model generation: 0.111551,  model checking: 0.000186):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2801, q_gen_2803, q_gen_2804, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2799) -> q_gen_2799
<z>() -> q_gen_2799
<z, z>() -> q_gen_2796
<s, s>(q_gen_2796) -> q_gen_2801
<s, s>(q_gen_2808) -> q_gen_2801
<s, s>(q_gen_2801) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2795) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, s, z>(q_gen_2796) -> q_gen_2795
<s, s, z>(q_gen_2808) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, s>(q_gen_2801) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, s, z>(q_gen_2801) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 36  ;  () -> minus([z, y, z]) -> 34  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 46  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 49
}
Sat witness: Yes: (() -> minus([s(u), z, s(u)]), {
u -> s(s(z))
})

-------------------------------------------
Step 37, which took 0.105417 s (model generation: 0.099025,  model checking: 0.006392):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2795) -> q_gen_2795
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 37  ;  () -> minus([z, y, z]) -> 35  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 49  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 49
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> s(s(z))  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 38, which took 0.097869 s (model generation: 0.097279,  model checking: 0.000590):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2801, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<z, z>() -> q_gen_2796
<s, s>(q_gen_2796) -> q_gen_2801
<s, s>(q_gen_2801) -> q_gen_2801
<s, s>(q_gen_2820) -> q_gen_2801
<s, z>(q_gen_2806) -> q_gen_2801
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2801) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2801) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 38  ;  () -> minus([z, y, z]) -> 36  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 49  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 52
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> s(z)  ;  x2 -> s(z)
})

-------------------------------------------
Step 39, which took 0.095208 s (model generation: 0.093865,  model checking: 0.001343):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2794) -> q_gen_2803
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, s>(q_gen_2838) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 39  ;  () -> minus([z, y, z]) -> 37  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 52  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 52
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> s(z)  ;  _waa -> z  ;  _xaa -> z  ;  k -> z  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 40, which took 0.087421 s (model generation: 0.086772,  model checking: 0.000649):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2838) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 40  ;  () -> minus([z, y, z]) -> 38  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 52  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 55
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(s(z)))  ;  x2 -> z
})

-------------------------------------------
Step 41, which took 0.088587 s (model generation: 0.086979,  model checking: 0.001608):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 41  ;  () -> minus([z, y, z]) -> 39  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 55  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 55
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(s(z))  ;  _waa -> z  ;  _xaa -> z  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 42, which took 0.096013 s (model generation: 0.095074,  model checking: 0.000939):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2808) -> q_gen_2838
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 42  ;  () -> minus([z, y, z]) -> 40  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 55  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 58
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(z))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 43, which took 0.112287 s (model generation: 0.110070,  model checking: 0.002217):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2808) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 43  ;  () -> minus([z, y, z]) -> 41  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 58  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 58
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(s(z))))  ;  _vaa -> s(z)  ;  _waa -> s(z)  ;  _xaa -> z  ;  k -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 44, which took 0.128603 s (model generation: 0.127722,  model checking: 0.000881):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2808) -> q_gen_2840
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2804) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2804
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 44  ;  () -> minus([z, y, z]) -> 42  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 58  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 61
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> s(z)  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 45, which took 0.132134 s (model generation: 0.128013,  model checking: 0.004121):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2852},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2806) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2852
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, z>(q_gen_2852) -> q_gen_2815
<s, z, s>(q_gen_2852) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 45  ;  () -> minus([z, y, z]) -> 43  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 61  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 61
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(s(z))  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 46, which took 0.151777 s (model generation: 0.151022,  model checking: 0.000755):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2798, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820},
Q_f={q_gen_2794, q_gen_2798},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2798) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2798
<z, s, z>(q_gen_2799) -> q_gen_2798
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 46  ;  () -> minus([z, y, z]) -> 44  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 61  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 64
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(z)  ;  u -> s(z)  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 47, which took 0.183376 s (model generation: 0.181455,  model checking: 0.001921):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2796
<z, z>() -> q_gen_2796
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, s>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 47  ;  () -> minus([z, y, z]) -> 45  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 64  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 64
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(z)  ;  _waa -> s(z)  ;  _xaa -> z  ;  k -> s(z)  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 48, which took 0.138882 s (model generation: 0.137938,  model checking: 0.000944):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, s>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 48  ;  () -> minus([z, y, z]) -> 46  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 64  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 67
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(z)))  ;  u -> s(s(s(s(s(z)))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 49, which took 0.180298 s (model generation: 0.179516,  model checking: 0.000782):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2802, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820},
Q_f={q_gen_2794, q_gen_2802},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2820
<s, s, s>(q_gen_2802) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 49  ;  () -> minus([z, y, z]) -> 47  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 67  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 67
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(s(z))))  ;  _vaa -> s(s(z))  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(z))))  ;  n -> s(z)
})

-------------------------------------------
Step 50, which took 0.342616 s (model generation: 0.341765,  model checking: 0.000851):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2838) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2809
<s, s, z>(q_gen_2840) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, s>(q_gen_2838) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 50  ;  () -> minus([z, y, z]) -> 48  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 67  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 70
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(s(z))))))  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 51, which took 0.361983 s (model generation: 0.354099,  model checking: 0.007884):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2802, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794, q_gen_2802},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2838) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2802) -> q_gen_2802
<s, s, s>(q_gen_2803) -> q_gen_2802
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 51  ;  () -> minus([z, y, z]) -> 49  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 70  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 70
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(s(z))  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 52, which took 0.242257 s (model generation: 0.241909,  model checking: 0.000348):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2817, q_gen_2820, q_gen_2852},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2817) -> q_gen_2820
<z, s>(q_gen_2817) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2852
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2809
<s, s, z>(q_gen_2852) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, s>(q_gen_2852) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 51  ;  () -> minus([z, y, z]) -> 52  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 70  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 70
}
Sat witness: Yes: (() -> minus([z, y, z]), {
y -> s(s(s(s(z))))
})

-------------------------------------------
Step 53, which took 0.323411 s (model generation: 0.322102,  model checking: 0.001309):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<s, s>(q_gen_2838) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, s>(q_gen_2838) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 52  ;  () -> minus([z, y, z]) -> 53  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 70  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 73
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(s(s(s(z))))  ;  x2 -> z
})

-------------------------------------------
Step 54, which took 0.300736 s (model generation: 0.298025,  model checking: 0.002711):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2798, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2838},
Q_f={q_gen_2794, q_gen_2798},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2838
<s, s, s>(q_gen_2798) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2798
<s, s, z>(q_gen_2808) -> q_gen_2798
<z, s, z>(q_gen_2799) -> q_gen_2798
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 53  ;  () -> minus([z, y, z]) -> 54  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 73  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 73
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(z))))  ;  n -> s(s(z))
})

-------------------------------------------
Step 55, which took 0.277381 s (model generation: 0.276137,  model checking: 0.001244):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2840) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, s>(q_gen_2838) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 54  ;  () -> minus([z, y, z]) -> 55  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 73  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 76
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(z)))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 56, which took 0.281804 s (model generation: 0.273487,  model checking: 0.008317):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2806
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 55  ;  () -> minus([z, y, z]) -> 56  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 76  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 76
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(z))))  ;  n -> s(s(z))
})

-------------------------------------------
Step 57, which took 0.385269 s (model generation: 0.384414,  model checking: 0.000855):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2817) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<z, s>(q_gen_2817) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2809
<s, s, z>(q_gen_2840) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, s>(q_gen_2840) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 56  ;  () -> minus([z, y, z]) -> 57  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 76  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 79
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(s(s(s(z)))))))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 58, which took 0.508419 s (model generation: 0.506550,  model checking: 0.001869):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<z, s>(q_gen_2817) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2809
<s, s, z>(q_gen_2840) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, s>(q_gen_2840) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 57  ;  () -> minus([z, y, z]) -> 58  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 79  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 79
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(z)  ;  _xaa -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 59, which took 0.554586 s (model generation: 0.553807,  model checking: 0.000779):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2810, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2817) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2810) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2810
<s, s, z>(q_gen_2840) -> q_gen_2810
<s, z, s>(q_gen_2840) -> q_gen_2810
<s, z, z>(q_gen_2806) -> q_gen_2810
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 58  ;  () -> minus([z, y, z]) -> 59  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 79  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 82
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(z)))  ;  u -> s(s(s(s(s(s(z))))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 60, which took 0.783649 s (model generation: 0.773486,  model checking: 0.010163):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2810, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2810) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2810
<s, s, z>(q_gen_2840) -> q_gen_2810
<s, z, s>(q_gen_2840) -> q_gen_2810
<s, z, z>(q_gen_2806) -> q_gen_2810
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 59  ;  () -> minus([z, y, z]) -> 60  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 82  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 82
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(s(s(s(z))))  ;  _xaa -> s(s(z))  ;  k -> s(s(z))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 61, which took 0.877030 s (model generation: 0.876090,  model checking: 0.000940):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2803) -> q_gen_2795
<s, s, z>(q_gen_2796) -> q_gen_2795
<s, z, s>(q_gen_2796) -> q_gen_2795
<s, z, z>(q_gen_2817) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2806) -> q_gen_2795
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, s>(q_gen_2795) -> q_gen_2815
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, s>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 60  ;  () -> minus([z, y, z]) -> 61  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 82  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 85
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> s(s(s(s(z))))  ;  x2 -> z
})

-------------------------------------------
Step 62, which took 0.988134 s (model generation: 0.986647,  model checking: 0.001487):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2795, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2810, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794, q_gen_2795},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2795
<z, s, z>(q_gen_2799) -> q_gen_2795
<z, s, z>(q_gen_2806) -> q_gen_2795
<s, s, s>(q_gen_2810) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, s>(q_gen_2795) -> q_gen_2810
<s, s, s>(q_gen_2804) -> q_gen_2810
<s, s, z>(q_gen_2840) -> q_gen_2810
<s, z, s>(q_gen_2840) -> q_gen_2810
<s, z, z>(q_gen_2806) -> q_gen_2810
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 61  ;  () -> minus([z, y, z]) -> 62  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 85  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 85
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(s(z)))  ;  _vaa -> s(s(s(z)))  ;  _waa -> s(s(z))  ;  _xaa -> z  ;  k -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 63, which took 0.997362 s (model generation: 0.996787,  model checking: 0.000575):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2817, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<z, s>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2809) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2809
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2806) -> q_gen_2809
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 62  ;  () -> minus([z, y, z]) -> 63  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 85  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 88
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> z  ;  x2 -> s(s(s(s(z))))
})

-------------------------------------------
Step 64, which took 1.016794 s (model generation: 1.014600,  model checking: 0.002194):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2817) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<z, s>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, z>(q_gen_2817) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 63  ;  () -> minus([z, y, z]) -> 64  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 88  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 88
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> z  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(s(z))  ;  k -> z  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 65, which took 0.974456 s (model generation: 0.973876,  model checking: 0.000580):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2817) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<z, s>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 64  ;  () -> minus([z, y, z]) -> 65  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 88  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 91
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> z  ;  u -> z  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 66, which took 1.217817 s (model generation: 1.203695,  model checking: 0.014122):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<s>(q_gen_2817) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 65  ;  () -> minus([z, y, z]) -> 66  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 91  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 91
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(z)  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(s(s(z))))))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 67, which took 2.265372 s (model generation: 2.263999,  model checking: 0.001373):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2809, q_gen_2810, q_gen_2817, q_gen_2820, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s>(q_gen_2817) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2840) -> q_gen_2840
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2810) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2809
<s, z, z>(q_gen_2817) -> q_gen_2809
<s, s, s>(q_gen_2809) -> q_gen_2810
<s, s, z>(q_gen_2840) -> q_gen_2810
<s, z, s>(q_gen_2840) -> q_gen_2810
<s, z, z>(q_gen_2806) -> q_gen_2810
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 66  ;  () -> minus([z, y, z]) -> 67  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 91  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 94
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(s(z)))))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 68, which took 1.300326 s (model generation: 1.289394,  model checking: 0.010932):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2838, q_gen_2840},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2817) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2838) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, s>(q_gen_2840) -> q_gen_2840
<s, z>(q_gen_2806) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, s, z>(q_gen_2838) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, z, s>(q_gen_2838) -> q_gen_2804
<s, z, s>(q_gen_2840) -> q_gen_2804
<s, z, z>(q_gen_2817) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 67  ;  () -> minus([z, y, z]) -> 68  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 94  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 94
}
Sat witness: Yes: ((minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]), {
_uaa -> s(s(z))  ;  _vaa -> z  ;  _waa -> s(s(z))  ;  _xaa -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(s(s(z))))))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 69, which took 4.048926 s (model generation: 4.047318,  model checking: 0.001608):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2808, q_gen_2815, q_gen_2817, q_gen_2820, q_gen_2840, q_gen_2852, q_gen_2866},
Q_f={q_gen_2794},
Delta=
{
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2817) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<s, s>(q_gen_2796) -> q_gen_2796
<z, z>() -> q_gen_2796
<s, s>(q_gen_2808) -> q_gen_2808
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2808
<z, s>(q_gen_2817) -> q_gen_2808
<s, s>(q_gen_2820) -> q_gen_2820
<s, s>(q_gen_2852) -> q_gen_2820
<s, z>(q_gen_2799) -> q_gen_2820
<s, z>(q_gen_2817) -> q_gen_2840
<s, z>(q_gen_2806) -> q_gen_2852
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2808) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2815) -> q_gen_2803
<s, s, z>(q_gen_2820) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, s>(q_gen_2866) -> q_gen_2815
<s, s, z>(q_gen_2852) -> q_gen_2815
<s, z, s>(q_gen_2852) -> q_gen_2815
<s, z, z>(q_gen_2806) -> q_gen_2815
<s, z, s>(q_gen_2840) -> q_gen_2866
<s, z, z>(q_gen_2817) -> q_gen_2866
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 68  ;  () -> minus([z, y, z]) -> 69  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 94  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 97
}
Sat witness: Yes: ((minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]), {
_paa -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(z)))))  ;  x2 -> s(z)
})

-------------------------------------------
Step 70, which took 9.013205 s (model generation: 9.012834,  model checking: 0.000371):

Model:
|_
{
minus -> 
{{{
Q={q_gen_2794, q_gen_2796, q_gen_2799, q_gen_2801, q_gen_2803, q_gen_2804, q_gen_2806, q_gen_2807, q_gen_2808, q_gen_2811, q_gen_2812, q_gen_2817, q_gen_2819, q_gen_2820, q_gen_2837, q_gen_2838, q_gen_2840, q_gen_2842, q_gen_2844, q_gen_2845, q_gen_2848, q_gen_2849, q_gen_2850, q_gen_2852, q_gen_2855, q_gen_2856, q_gen_2857, q_gen_2862, q_gen_2867},
Q_f={q_gen_2794, q_gen_2807, q_gen_2844, q_gen_2845},
Delta=
{
<s>(q_gen_2817) -> q_gen_2799
<z>() -> q_gen_2799
<s>(q_gen_2799) -> q_gen_2806
<s>(q_gen_2806) -> q_gen_2817
<z, z>() -> q_gen_2796
<s, s>(q_gen_2796) -> q_gen_2801
<z, s>(q_gen_2799) -> q_gen_2808
<z, s>(q_gen_2806) -> q_gen_2812
<s, z>(q_gen_2799) -> q_gen_2820
<s, s>(q_gen_2820) -> q_gen_2838
<s, s>(q_gen_2840) -> q_gen_2838
<s, s>(q_gen_2848) -> q_gen_2838
<s, s>(q_gen_2801) -> q_gen_2840
<s, z>(q_gen_2817) -> q_gen_2840
<s, s>(q_gen_2808) -> q_gen_2848
<s, s>(q_gen_2812) -> q_gen_2848
<z, s>(q_gen_2817) -> q_gen_2848
<s, s>(q_gen_2838) -> q_gen_2852
<s, s>(q_gen_2852) -> q_gen_2852
<s, z>(q_gen_2806) -> q_gen_2852
<s, s, s>(q_gen_2803) -> q_gen_2794
<s, s, s>(q_gen_2819) -> q_gen_2794
<s, s, z>(q_gen_2796) -> q_gen_2794
<s, s, z>(q_gen_2801) -> q_gen_2794
<s, s, z>(q_gen_2812) -> q_gen_2794
<s, z, s>(q_gen_2796) -> q_gen_2794
<s, z, s>(q_gen_2801) -> q_gen_2794
<z, s, z>(q_gen_2799) -> q_gen_2794
<z, s, z>(q_gen_2806) -> q_gen_2794
<z, s, z>(q_gen_2817) -> q_gen_2794
<z, z, z>() -> q_gen_2794
<s, s, s>(q_gen_2811) -> q_gen_2803
<s, z, s>(q_gen_2820) -> q_gen_2803
<s, z, z>(q_gen_2799) -> q_gen_2803
<s, s, s>(q_gen_2794) -> q_gen_2804
<s, s, s>(q_gen_2804) -> q_gen_2804
<s, s, z>(q_gen_2840) -> q_gen_2804
<s, z, s>(q_gen_2808) -> q_gen_2804
<s, s, z>(q_gen_2808) -> q_gen_2807
<s, z, s>(q_gen_2812) -> q_gen_2811
<s, z, z>(q_gen_2806) -> q_gen_2811
<s, s, z>(q_gen_2820) -> q_gen_2819
<s, s, z>(q_gen_2838) -> q_gen_2837
<s, s, s>(q_gen_2842) -> q_gen_2842
<s, z, s>(q_gen_2838) -> q_gen_2842
<s, z, s>(q_gen_2848) -> q_gen_2842
<s, s, s>(q_gen_2837) -> q_gen_2844
<s, z, s>(q_gen_2852) -> q_gen_2844
<s, s, s>(q_gen_2862) -> q_gen_2845
<s, s, z>(q_gen_2848) -> q_gen_2845
<s, z, s>(q_gen_2840) -> q_gen_2845
<s, s, s>(q_gen_2850) -> q_gen_2849
<s, s, z>(q_gen_2852) -> q_gen_2849
<s, s, s>(q_gen_2844) -> q_gen_2850
<s, s, s>(q_gen_2855) -> q_gen_2850
<s, s, s>(q_gen_2807) -> q_gen_2855
<s, s, s>(q_gen_2857) -> q_gen_2856
<s, s, s>(q_gen_2845) -> q_gen_2857
<s, z, z>(q_gen_2817) -> q_gen_2857
<s, s, s>(q_gen_2849) -> q_gen_2862
<s, s, s>(q_gen_2856) -> q_gen_2867
<s, s, s>(q_gen_2867) -> q_gen_2867
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 71  ;  () -> minus([z, y, z]) -> 69  ;  (minus([_uaa, s(k), _vaa]) /\ minus([_waa, k, _xaa]) /\ minus([m, n, _waa]) /\ minus([s(m), n, _uaa])) -> eq_nat([_vaa, _xaa]) -> 94  ;  (minus([u, x2, _paa])) -> minus([s(u), s(x2), _paa]) -> 97
}
Sat witness: Yes: (() -> minus([s(u), z, s(u)]), {
u -> s(s(s(z)))
})

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