Solving ../../benchmarks/true/plus_commutative.smt2...

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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)])}
(plus([_qw, _rw, _sw]) /\ plus([_qw, _rw, _tw])) -> eq_nat([_sw, _tw])
)
}

properties:
{(plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw])}


over-approximation: {plus}
under-approximation: {}

Clause system for inference is:

{
() -> plus([n, z, n]) -> 0  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 0  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 0
}


Solving took 30.554950 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4767, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4771, q_gen_4772, q_gen_4773, q_gen_4774, q_gen_4775, q_gen_4776, q_gen_4777, q_gen_4778, q_gen_4779, q_gen_4780, q_gen_4781, q_gen_4782, q_gen_4783, q_gen_4784, q_gen_4785, q_gen_4786, q_gen_4787, q_gen_4788, q_gen_4789, q_gen_4790, q_gen_4791, q_gen_4792, q_gen_4793, q_gen_4794, q_gen_4795, q_gen_4796, q_gen_4797, q_gen_4798, q_gen_4799, q_gen_4800, q_gen_4801, q_gen_4802, q_gen_4803, q_gen_4804, q_gen_4805, q_gen_4806, q_gen_4807, q_gen_4808, q_gen_4809, q_gen_4810, q_gen_4811, q_gen_4812, q_gen_4813, q_gen_4814, q_gen_4815, q_gen_4816, q_gen_4817, q_gen_4818, q_gen_4819, q_gen_4820, q_gen_4821, q_gen_4822, q_gen_4823, q_gen_4824, q_gen_4825, q_gen_4826, q_gen_4827, q_gen_4828, q_gen_4829, q_gen_4830, q_gen_4831, q_gen_4832, q_gen_4833, q_gen_4834, q_gen_4835, q_gen_4836, q_gen_4837, q_gen_4838, q_gen_4839, q_gen_4840, q_gen_4841, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4845, q_gen_4846, q_gen_4847, q_gen_4848, q_gen_4849, q_gen_4850, q_gen_4851, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4856, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4861, q_gen_4862, q_gen_4863, q_gen_4864, q_gen_4865, q_gen_4866, q_gen_4867, q_gen_4868, q_gen_4869, q_gen_4870, q_gen_4871, q_gen_4872, q_gen_4873, q_gen_4874, q_gen_4875, q_gen_4876, q_gen_4877, q_gen_4878, q_gen_4879, q_gen_4880, q_gen_4881, q_gen_4882, q_gen_4883},
Q_f={},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4842
<z, z>() -> q_gen_4766
<s, s>(q_gen_4766) -> q_gen_4772
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4772) -> q_gen_4794
<z, s>(q_gen_4804) -> q_gen_4809
<s, s>(q_gen_4781) -> q_gen_4818
<s, s>(q_gen_4791) -> q_gen_4822
<z, s>(q_gen_4832) -> q_gen_4838
<s, s>(q_gen_4809) -> q_gen_4845
<s, s>(q_gen_4822) -> q_gen_4858
<s, s>(q_gen_4866) -> q_gen_4865
<s, s>(q_gen_4794) -> q_gen_4866
<s, s>(q_gen_4818) -> q_gen_4869
<z, z, z>() -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4767
<s, s, s>(q_gen_4769) -> q_gen_4768
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, z, s>(q_gen_4772) -> q_gen_4771
<s, s, s>(q_gen_4774) -> q_gen_4773
<s, z, s>(q_gen_4775) -> q_gen_4774
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4778) -> q_gen_4777
<z, s, s>(q_gen_4775) -> q_gen_4778
<s, s, s>(q_gen_4780) -> q_gen_4779
<z, s, s>(q_gen_4781) -> q_gen_4780
<s, s, s>(q_gen_4783) -> q_gen_4782
<s, s, s>(q_gen_4784) -> q_gen_4783
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4787) -> q_gen_4786
<s, z, s>(q_gen_4781) -> q_gen_4787
<s, s, s>(q_gen_4789) -> q_gen_4788
<s, s, s>(q_gen_4790) -> q_gen_4789
<s, z, s>(q_gen_4791) -> q_gen_4790
<z, s, s>(q_gen_4791) -> q_gen_4792
<s, z, s>(q_gen_4794) -> q_gen_4793
<z, s, s>(q_gen_4772) -> q_gen_4795
<s, s, s>(q_gen_4797) -> q_gen_4796
<s, s, s>(q_gen_4798) -> q_gen_4797
<s, s, s>(q_gen_4767) -> q_gen_4798
<s, s, s>(q_gen_4800) -> q_gen_4799
<s, s, s>(q_gen_4801) -> q_gen_4800
<s, s, s>(q_gen_4768) -> q_gen_4801
<s, s, s>(q_gen_4803) -> q_gen_4802
<z, z, s>(q_gen_4804) -> q_gen_4803
<s, s, s>(q_gen_4802) -> q_gen_4805
<s, s, s>(q_gen_4807) -> q_gen_4806
<s, s, s>(q_gen_4808) -> q_gen_4807
<z, s, s>(q_gen_4809) -> q_gen_4808
<s, s, s>(q_gen_4776) -> q_gen_4810
<s, s, s>(q_gen_4805) -> q_gen_4811
<s, s, s>(q_gen_4792) -> q_gen_4812
<s, s, s>(q_gen_4812) -> q_gen_4813
<s, s, s>(q_gen_4806) -> q_gen_4814
<s, z, s>(q_gen_4809) -> q_gen_4815
<s, s, s>(q_gen_4817) -> q_gen_4816
<s, z, s>(q_gen_4818) -> q_gen_4817
<s, s, s>(q_gen_4820) -> q_gen_4819
<s, s, s>(q_gen_4821) -> q_gen_4820
<s, z, s>(q_gen_4822) -> q_gen_4821
<s, s, s>(q_gen_4810) -> q_gen_4823
<s, s, s>(q_gen_4825) -> q_gen_4824
<s, s, s>(q_gen_4826) -> q_gen_4825
<s, s, s>(q_gen_4765) -> q_gen_4826
<z, s, s>(q_gen_4822) -> q_gen_4827
<s, s, s>(q_gen_4815) -> q_gen_4828
<s, s, s>(q_gen_4830) -> q_gen_4829
<s, s, s>(q_gen_4831) -> q_gen_4830
<z, z, s>(q_gen_4832) -> q_gen_4831
<s, s, s>(q_gen_4834) -> q_gen_4833
<s, s, s>(q_gen_4828) -> q_gen_4834
<s, s, s>(q_gen_4836) -> q_gen_4835
<s, s, s>(q_gen_4829) -> q_gen_4836
<z, s, s>(q_gen_4838) -> q_gen_4837
<s, z, s>(q_gen_4838) -> q_gen_4839
<s, s, s>(q_gen_4841) -> q_gen_4840
<z, z, s>(q_gen_4842) -> q_gen_4841
<s, s, s>(q_gen_4844) -> q_gen_4843
<z, s, s>(q_gen_4845) -> q_gen_4844
<s, s, s>(q_gen_4847) -> q_gen_4846
<s, s, s>(q_gen_4782) -> q_gen_4847
<s, s, s>(q_gen_4823) -> q_gen_4848
<s, s, s>(q_gen_4850) -> q_gen_4849
<s, s, s>(q_gen_4851) -> q_gen_4850
<s, z, s>(q_gen_4845) -> q_gen_4851
<s, s, s>(q_gen_4853) -> q_gen_4852
<s, s, s>(q_gen_4854) -> q_gen_4853
<s, s, s>(q_gen_4839) -> q_gen_4854
<s, s, s>(q_gen_4856) -> q_gen_4855
<s, s, s>(q_gen_4857) -> q_gen_4856
<s, z, s>(q_gen_4858) -> q_gen_4857
<s, s, s>(q_gen_4849) -> q_gen_4859
<s, s, s>(q_gen_4861) -> q_gen_4860
<s, s, s>(q_gen_4862) -> q_gen_4861
<s, s, s>(q_gen_4840) -> q_gen_4862
<z, s, s>(q_gen_4818) -> q_gen_4863
<s, z, s>(q_gen_4865) -> q_gen_4864
<s, s, s>(q_gen_4868) -> q_gen_4867
<s, z, s>(q_gen_4869) -> q_gen_4868
<s, s, s>(q_gen_4852) -> q_gen_4870
<s, s, s>(q_gen_4848) -> q_gen_4871
<s, s, s>(q_gen_4873) -> q_gen_4872
<s, s, s>(q_gen_4824) -> q_gen_4873
<s, s, s>(q_gen_4855) -> q_gen_4874
<s, s, s>(q_gen_4859) -> q_gen_4875
<s, s, s>(q_gen_4827) -> q_gen_4876
<s, s, s>(q_gen_4835) -> q_gen_4877
<s, s, s>(q_gen_4879) -> q_gen_4878
<s, s, s>(q_gen_4880) -> q_gen_4879
<s, s, s>(q_gen_4881) -> q_gen_4880
<s, s, s>(q_gen_4882) -> q_gen_4881
<s, s, s>(q_gen_4837) -> q_gen_4882
<z, s, s>(q_gen_4794) -> q_gen_4883
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010160 s (model generation: 0.009846,  model checking: 0.000314):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 3  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 1  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010505 s (model generation: 0.010233,  model checking: 0.000272):

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

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 3  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 1  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 2, which took 0.011055 s (model generation: 0.010719,  model checking: 0.000336):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766},
Q_f={q_gen_4764},
Delta=
{
<z, z>() -> q_gen_4766
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 2  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 3, which took 0.014177 s (model generation: 0.010837,  model checking: 0.003340):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766},
Q_f={q_gen_4764},
Delta=
{
<z, z>() -> q_gen_4766
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 3  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 4, which took 0.011508 s (model generation: 0.011291,  model checking: 0.000217):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4770},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<z, z>() -> q_gen_4766
<s, s, s>(q_gen_4764) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4770) -> q_gen_4764
<z, z, z>() -> q_gen_4764
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 6  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 7
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(z)  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.011283 s (model generation: 0.010610,  model checking: 0.000673):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<z, z>() -> q_gen_4766
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 9  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 7  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 6, which took 0.014208 s (model generation: 0.011704,  model checking: 0.002504):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 9  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 7  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 7, which took 0.013283 s (model generation: 0.012782,  model checking: 0.000501):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s, s>(q_gen_4764) -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 9  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 10  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 10
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(z))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 8, which took 0.015771 s (model generation: 0.013462,  model checking: 0.002309):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 10  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 10  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 9, which took 0.017067 s (model generation: 0.014729,  model checking: 0.002338):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 11  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 11  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 16
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.016942 s (model generation: 0.016165,  model checking: 0.000777):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s, s>(q_gen_4765) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4764) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 11  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 14  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 16
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(z))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 11, which took 0.016440 s (model generation: 0.014178,  model checking: 0.002262):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 12  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 15  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 19
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.021158 s (model generation: 0.019861,  model checking: 0.001297):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<s>(q_gen_4770) -> q_gen_4770
<z>() -> q_gen_4770
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4765) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 13  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 18  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 19
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.020746 s (model generation: 0.020143,  model checking: 0.000603):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4785) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 14  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 21  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 19
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(s(z))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 14, which took 0.021289 s (model generation: 0.019261,  model checking: 0.002028):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4784, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 15  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 21  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 22
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 15, which took 0.027010 s (model generation: 0.026349,  model checking: 0.000661):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4784, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4785) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 16  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 24  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 22
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(s(z)))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 16, which took 0.021399 s (model generation: 0.020926,  model checking: 0.000473):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4772, q_gen_4775, q_gen_4776, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<z, z>() -> q_gen_4766
<s, s>(q_gen_4766) -> q_gen_4772
<s, s>(q_gen_4775) -> q_gen_4772
<z, s>(q_gen_4785) -> q_gen_4772
<z, s>(q_gen_4770) -> q_gen_4775
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4772) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4772) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 19  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 24  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 22
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(s(z)))
})

-------------------------------------------
Step 17, which took 0.020231 s (model generation: 0.019385,  model checking: 0.000846):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4781
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4781) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 20  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 24  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 25
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 18, which took 0.017378 s (model generation: 0.017032,  model checking: 0.000346):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4785},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4781) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 21  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 27  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 25
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.017556 s (model generation: 0.016933,  model checking: 0.000623):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4775
<s, s, s>(q_gen_4768) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4768
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 22  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 27  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 28
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 20, which took 0.026066 s (model generation: 0.025365,  model checking: 0.000701):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4775
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4768) -> q_gen_4768
<s, s, s>(q_gen_4769) -> q_gen_4768
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 23  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 30  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 28
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 21, which took 0.022476 s (model generation: 0.021386,  model checking: 0.001090):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4784, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4791) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 24  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 30  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 31
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.021263 s (model generation: 0.020705,  model checking: 0.000558):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4785) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 25  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 33  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 31
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 23, which took 0.021427 s (model generation: 0.020800,  model checking: 0.000627):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4791) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 26  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 33  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 34
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 24, which took 0.034428 s (model generation: 0.033777,  model checking: 0.000651):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4784, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4764) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 27  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 36  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 34
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 25, which took 0.032565 s (model generation: 0.031913,  model checking: 0.000652):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 28  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 36  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 37
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 26, which took 0.034036 s (model generation: 0.033383,  model checking: 0.000653):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4785
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4765) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 29  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 39  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 37
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 27, which took 0.033250 s (model generation: 0.032642,  model checking: 0.000608):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4804) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 30  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 39  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 40
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 28, which took 0.033805 s (model generation: 0.033413,  model checking: 0.000392):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4804) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4804) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4791) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 31  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 42  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 40
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(s(s(z)))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 29, which took 0.035320 s (model generation: 0.034953,  model checking: 0.000367):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4781
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4781) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 32  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 42  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 43
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 30, which took 0.031093 s (model generation: 0.030455,  model checking: 0.000638):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4791) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 33  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 45  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 43
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 31, which took 0.033141 s (model generation: 0.032228,  model checking: 0.000913):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4792, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4804) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4792) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4792
<z, z, s>(q_gen_4804) -> q_gen_4792
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 34  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 45  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 46
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 32, which took 0.034664 s (model generation: 0.033948,  model checking: 0.000716):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4804) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 35  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 48  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 46
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(s(s(z))))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 33, which took 0.039056 s (model generation: 0.038105,  model checking: 0.000951):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 36  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 48  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 49
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 34, which took 0.039576 s (model generation: 0.038889,  model checking: 0.000687):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4772, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4795, q_gen_4804},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4772) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4766) -> q_gen_4772
<z, s>(q_gen_4804) -> q_gen_4772
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4772) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4795) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, s, s>(q_gen_4772) -> q_gen_4795
<z, z, s>(q_gen_4804) -> q_gen_4795
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 37  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 51  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 49
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(s(s(z))))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 35, which took 0.041110 s (model generation: 0.039784,  model checking: 0.001326):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4791
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4768) -> q_gen_4768
<s, s, s>(q_gen_4769) -> q_gen_4768
<z, s, s>(q_gen_4775) -> q_gen_4768
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 38  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 51  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 52
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(z)  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 36, which took 0.078631 s (model generation: 0.077797,  model checking: 0.000834):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4791
<s, s, s>(q_gen_4765) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 39  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 54  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 52
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(s(s(s(z))))))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 37, which took 0.110540 s (model generation: 0.109786,  model checking: 0.000754):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4791) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4765) -> q_gen_4769
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 40  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 54  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 55
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 38, which took 0.077248 s (model generation: 0.076402,  model checking: 0.000846):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4791) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<z, s>(q_gen_4785) -> q_gen_4791
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4765) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 41  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 57  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 55
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(z))  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 39, which took 0.112269 s (model generation: 0.110404,  model checking: 0.001865):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4765) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 42  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 57  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 58
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 40, which took 0.107983 s (model generation: 0.107028,  model checking: 0.000955):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4804) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4765) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 43  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 60  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 58
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 41, which took 0.107647 s (model generation: 0.106184,  model checking: 0.001463):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 44  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 60  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 61
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 42, which took 0.134935 s (model generation: 0.133992,  model checking: 0.000943):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4804) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 45  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 63  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 61
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 43, which took 0.152875 s (model generation: 0.151767,  model checking: 0.001108):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 46  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 63  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 64
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 44, which took 0.143602 s (model generation: 0.142754,  model checking: 0.000848):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<s, z, s>(q_gen_4809) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 47  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 66  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 64
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(s(s(z)))))))  ;  _vw -> s(s(s(s(s(s(z))))))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 45, which took 0.144455 s (model generation: 0.142934,  model checking: 0.001521):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 48  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 66  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 67
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 46, which took 0.134899 s (model generation: 0.133528,  model checking: 0.001371):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4765) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 49  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 69  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 67
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 47, which took 0.203955 s (model generation: 0.201860,  model checking: 0.002095):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4832) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 50  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 69  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 70
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 48, which took 0.152270 s (model generation: 0.151001,  model checking: 0.001269):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4767, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764, q_gen_4767},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4767
<s, z, s>(q_gen_4766) -> q_gen_4767
<s, s, s>(q_gen_4767) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4809) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 51  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 72  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 70
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(z)))  ;  m -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 49, which took 0.236764 s (model generation: 0.233886,  model checking: 0.002878):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4832) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4832) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 52  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 72  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 73
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 50, which took 0.230732 s (model generation: 0.229973,  model checking: 0.000759):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4832) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, s>(q_gen_4832) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 53  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 75  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 73
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(s(s(s(z))))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 51, which took 0.256475 s (model generation: 0.254530,  model checking: 0.001945):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4768
<s, s, s>(q_gen_4768) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4809) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 54  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 75  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 76
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 52, which took 0.252362 s (model generation: 0.251017,  model checking: 0.001345):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4768
<s, s, s>(q_gen_4768) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 55  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 78  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 76
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(s(s(s(s(z))))))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 53, which took 0.330695 s (model generation: 0.329671,  model checking: 0.001024):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4832) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 56  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 78  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 79
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 54, which took 0.712074 s (model generation: 0.700294,  model checking: 0.011780):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4832) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<s, s>(q_gen_4809) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 57  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 81  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 79
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(s(z))))))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 55, which took 0.664100 s (model generation: 0.662464,  model checking: 0.001636):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4809) -> q_gen_4766
<z, s>(q_gen_4832) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 58  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 81  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 82
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 56, which took 1.110965 s (model generation: 1.109940,  model checking: 0.001025):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4809) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4791) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4781) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<s, z, s>(q_gen_4781) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 59  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 84  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 82
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 57, which took 1.081735 s (model generation: 1.080752,  model checking: 0.000983):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809, q_gen_4831, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4832) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4831) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, z, s>(q_gen_4832) -> q_gen_4831
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 60  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 84  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 85
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 58, which took 1.145524 s (model generation: 1.027642,  model checking: 0.117882):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4781) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4791) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<s, z, s>(q_gen_4781) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 61  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 87  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 85
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(z))))  ;  m -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 59, which took 0.870778 s (model generation: 0.869776,  model checking: 0.001002):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<s, s>(q_gen_4781) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4791) -> q_gen_4809
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<s, z, s>(q_gen_4781) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 62  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 87  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 88
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> z  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 60, which took 1.245694 s (model generation: 1.244739,  model checking: 0.000955):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, s>(q_gen_4832) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 63  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 90  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 88
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 61, which took 1.122865 s (model generation: 1.121051,  model checking: 0.001814):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4791) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<s, s>(q_gen_4781) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<s, z, s>(q_gen_4781) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 64  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 90  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 91
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 62, which took 1.163595 s (model generation: 1.162738,  model checking: 0.000857):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809, q_gen_4831, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4776) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4776
<s, z, s>(q_gen_4791) -> q_gen_4776
<z, s, s>(q_gen_4791) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4776
<s, s, s>(q_gen_4831) -> q_gen_4803
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
<z, z, s>(q_gen_4832) -> q_gen_4831
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 65  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 93  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 91
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(s(s(z))))))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 63, which took 0.785494 s (model generation: 0.784323,  model checking: 0.001171):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 66  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 93  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 94
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 64, which took 1.497979 s (model generation: 1.497194,  model checking: 0.000785):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809},
Q_f={q_gen_4764, q_gen_4768},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4804) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4768
<s, s, s>(q_gen_4768) -> q_gen_4769
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4776
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 67  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 96  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 94
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(s(z))))))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 65, which took 1.004248 s (model generation: 1.003155,  model checking: 0.001093):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4765) -> q_gen_4784
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4803
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 68  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 96  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 97
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 66, which took 1.134792 s (model generation: 1.133685,  model checking: 0.001107):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4772, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4795, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<s>(q_gen_4832) -> q_gen_4770
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4772) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4766) -> q_gen_4772
<z, s>(q_gen_4832) -> q_gen_4772
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<s, z, s>(q_gen_4772) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4795) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, s, s>(q_gen_4772) -> q_gen_4795
<z, z, s>(q_gen_4832) -> q_gen_4795
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 69  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 99  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 97
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(z)  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 67, which took 1.545303 s (model generation: 1.543200,  model checking: 0.002103):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4832) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4765) -> q_gen_4784
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4803
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 70  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 99  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 100
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 68, which took 0.877305 s (model generation: 0.876455,  model checking: 0.000850):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4804, q_gen_4809, q_gen_4831, q_gen_4832},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s, s>(q_gen_4765) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<s, s, s>(q_gen_4831) -> q_gen_4776
<s, z, s>(q_gen_4809) -> q_gen_4776
<z, s, s>(q_gen_4809) -> q_gen_4776
<z, z, s>(q_gen_4804) -> q_gen_4776
<s, s, s>(q_gen_4776) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<z, z, s>(q_gen_4832) -> q_gen_4831
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 71  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 102  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 100
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(s(s(s(z))))))))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 69, which took 1.002327 s (model generation: 0.999889,  model checking: 0.002438):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4767, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4796, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764, q_gen_4767},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s, s>(q_gen_4767) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4767
<s, z, s>(q_gen_4766) -> q_gen_4767
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4796) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4796
<s, z, s>(q_gen_4809) -> q_gen_4796
<z, s, s>(q_gen_4809) -> q_gen_4796
<z, z, s>(q_gen_4804) -> q_gen_4796
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 72  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 102  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 103
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(s(s(z))))))
})

-------------------------------------------
Step 70, which took 2.106432 s (model generation: 2.105577,  model checking: 0.000855):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4822, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<s, s>(q_gen_4822) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4809) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s>(q_gen_4791) -> q_gen_4822
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4822) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<s, z, s>(q_gen_4822) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 73  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 105  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 103
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(z))))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 71, which took 1.434763 s (model generation: 1.432465,  model checking: 0.002298):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4767, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4796, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764, q_gen_4767},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4832) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s, s>(q_gen_4767) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4767
<s, z, s>(q_gen_4766) -> q_gen_4767
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4796) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4796
<s, z, s>(q_gen_4809) -> q_gen_4796
<z, s, s>(q_gen_4809) -> q_gen_4796
<z, z, s>(q_gen_4804) -> q_gen_4796
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 74  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 105  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 106
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(s(z)))))))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 72, which took 2.364218 s (model generation: 2.362962,  model checking: 0.001256):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4797, q_gen_4804, q_gen_4809, q_gen_4822, q_gen_4832},
Q_f={q_gen_4764},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s>(q_gen_4832) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<s, s>(q_gen_4822) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4809) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<z, s>(q_gen_4832) -> q_gen_4809
<s, s>(q_gen_4791) -> q_gen_4822
<s, s, s>(q_gen_4769) -> q_gen_4764
<s, z, s>(q_gen_4766) -> q_gen_4764
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, s, s>(q_gen_4822) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4797) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<s, z, s>(q_gen_4822) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4797
<s, z, s>(q_gen_4809) -> q_gen_4797
<z, s, s>(q_gen_4809) -> q_gen_4797
<z, z, s>(q_gen_4804) -> q_gen_4797
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 75  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 108  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 106
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(z)))  ;  m -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 73, which took 1.843012 s (model generation: 1.839700,  model checking: 0.003312):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4766, q_gen_4767, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4784, q_gen_4785, q_gen_4791, q_gen_4803, q_gen_4804, q_gen_4809, q_gen_4832},
Q_f={q_gen_4764, q_gen_4767},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4832) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4775) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<z, s>(q_gen_4832) -> q_gen_4775
<s, s>(q_gen_4791) -> q_gen_4791
<z, s>(q_gen_4785) -> q_gen_4791
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4804) -> q_gen_4809
<z, s, s>(q_gen_4766) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4767
<s, z, s>(q_gen_4766) -> q_gen_4767
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, z, s>(q_gen_4832) -> q_gen_4776
<s, s, s>(q_gen_4767) -> q_gen_4784
<s, s, s>(q_gen_4803) -> q_gen_4784
<s, z, s>(q_gen_4791) -> q_gen_4784
<z, s, s>(q_gen_4791) -> q_gen_4784
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4776) -> q_gen_4803
<s, z, s>(q_gen_4809) -> q_gen_4803
<z, s, s>(q_gen_4809) -> q_gen_4803
<z, z, s>(q_gen_4804) -> q_gen_4803
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 76  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 111  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 107
}
Sat witness: Yes: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(s(s(z))))))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 74, which took 1.013975 s (model generation: 1.012430,  model checking: 0.001545):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4769, q_gen_4770, q_gen_4775, q_gen_4776, q_gen_4781, q_gen_4784, q_gen_4785, q_gen_4789, q_gen_4790, q_gen_4791, q_gen_4792, q_gen_4796, q_gen_4797, q_gen_4798, q_gen_4802, q_gen_4803, q_gen_4804, q_gen_4807, q_gen_4808, q_gen_4809, q_gen_4810, q_gen_4812, q_gen_4815, q_gen_4816, q_gen_4817, q_gen_4818, q_gen_4819, q_gen_4820, q_gen_4821, q_gen_4822, q_gen_4823, q_gen_4827, q_gen_4828, q_gen_4829, q_gen_4832, q_gen_4838, q_gen_4845, q_gen_4873},
Q_f={q_gen_4764, q_gen_4765},
Delta=
{
<z>() -> q_gen_4770
<s>(q_gen_4770) -> q_gen_4785
<s>(q_gen_4785) -> q_gen_4804
<s>(q_gen_4832) -> q_gen_4804
<s>(q_gen_4804) -> q_gen_4832
<s, s>(q_gen_4766) -> q_gen_4766
<z, z>() -> q_gen_4766
<s, s>(q_gen_4818) -> q_gen_4775
<z, s>(q_gen_4770) -> q_gen_4775
<s, s>(q_gen_4775) -> q_gen_4781
<z, s>(q_gen_4785) -> q_gen_4791
<z, s>(q_gen_4804) -> q_gen_4809
<s, s>(q_gen_4781) -> q_gen_4818
<s, s>(q_gen_4822) -> q_gen_4818
<s, s>(q_gen_4791) -> q_gen_4822
<z, s>(q_gen_4832) -> q_gen_4838
<s, s>(q_gen_4809) -> q_gen_4845
<s, s, s>(q_gen_4789) -> q_gen_4764
<s, s, s>(q_gen_4812) -> q_gen_4764
<z, z, z>() -> q_gen_4764
<s, s, s>(q_gen_4769) -> q_gen_4765
<s, z, s>(q_gen_4766) -> q_gen_4765
<z, s, s>(q_gen_4766) -> q_gen_4765
<s, s, s>(q_gen_4784) -> q_gen_4769
<s, s, s>(q_gen_4807) -> q_gen_4769
<s, z, s>(q_gen_4775) -> q_gen_4769
<s, z, s>(q_gen_4781) -> q_gen_4769
<z, s, s>(q_gen_4775) -> q_gen_4769
<z, s, s>(q_gen_4781) -> q_gen_4769
<z, z, s>(q_gen_4770) -> q_gen_4769
<s, s, s>(q_gen_4764) -> q_gen_4776
<z, s, s>(q_gen_4818) -> q_gen_4776
<z, z, s>(q_gen_4785) -> q_gen_4784
<s, s, s>(q_gen_4790) -> q_gen_4789
<s, s, s>(q_gen_4802) -> q_gen_4789
<s, z, s>(q_gen_4791) -> q_gen_4790
<z, s, s>(q_gen_4791) -> q_gen_4792
<s, s, s>(q_gen_4797) -> q_gen_4796
<s, s, s>(q_gen_4798) -> q_gen_4797
<s, s, s>(q_gen_4765) -> q_gen_4798
<s, s, s>(q_gen_4803) -> q_gen_4802
<z, z, s>(q_gen_4804) -> q_gen_4803
<s, s, s>(q_gen_4808) -> q_gen_4807
<z, s, s>(q_gen_4809) -> q_gen_4808
<s, s, s>(q_gen_4776) -> q_gen_4810
<s, s, s>(q_gen_4792) -> q_gen_4812
<s, z, s>(q_gen_4809) -> q_gen_4815
<s, s, s>(q_gen_4817) -> q_gen_4816
<s, z, s>(q_gen_4818) -> q_gen_4817
<z, z, s>(q_gen_4832) -> q_gen_4817
<s, s, s>(q_gen_4819) -> q_gen_4819
<s, s, s>(q_gen_4820) -> q_gen_4819
<s, s, s>(q_gen_4823) -> q_gen_4819
<s, s, s>(q_gen_4821) -> q_gen_4820
<s, z, s>(q_gen_4822) -> q_gen_4821
<s, s, s>(q_gen_4810) -> q_gen_4823
<s, s, s>(q_gen_4827) -> q_gen_4823
<s, s, s>(q_gen_4829) -> q_gen_4827
<z, s, s>(q_gen_4822) -> q_gen_4827
<z, s, s>(q_gen_4838) -> q_gen_4827
<s, s, s>(q_gen_4815) -> q_gen_4828
<s, z, s>(q_gen_4838) -> q_gen_4828
<s, z, s>(q_gen_4845) -> q_gen_4828
<z, s, s>(q_gen_4845) -> q_gen_4828
<s, s, s>(q_gen_4816) -> q_gen_4829
<s, s, s>(q_gen_4828) -> q_gen_4829
<s, s, s>(q_gen_4873) -> q_gen_4829
<s, s, s>(q_gen_4796) -> q_gen_4873
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 77  ;  (plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 111  ;  (plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 110
}
Sat witness: Yes: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(z)  ;  n -> s(s(s(s(s(z)))))
})

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