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


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 62.749099 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4200, q_gen_4201, q_gen_4202, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4206, q_gen_4207, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4211, q_gen_4212, q_gen_4213, q_gen_4214, q_gen_4215, q_gen_4216, q_gen_4217, q_gen_4218, q_gen_4219, q_gen_4220, q_gen_4221, q_gen_4222, q_gen_4223, q_gen_4224, q_gen_4225, q_gen_4226, q_gen_4227, q_gen_4228, q_gen_4229, q_gen_4230, q_gen_4231, q_gen_4232, q_gen_4233, q_gen_4234, q_gen_4235, q_gen_4236, q_gen_4237, q_gen_4238, q_gen_4239, q_gen_4240, q_gen_4241, q_gen_4242, q_gen_4243, q_gen_4244, q_gen_4245, q_gen_4246, q_gen_4247, q_gen_4248, q_gen_4249, q_gen_4250, q_gen_4251, q_gen_4252, q_gen_4253, q_gen_4254, q_gen_4255, q_gen_4256, q_gen_4257, q_gen_4258, q_gen_4259, q_gen_4260, q_gen_4261, q_gen_4262, q_gen_4263, q_gen_4264, q_gen_4265, q_gen_4266, q_gen_4267, q_gen_4268, q_gen_4269, q_gen_4270, q_gen_4271, q_gen_4272, q_gen_4273, q_gen_4274, q_gen_4275, q_gen_4276, q_gen_4277, q_gen_4278, q_gen_4279, q_gen_4280, q_gen_4281, q_gen_4282, q_gen_4283, q_gen_4284, q_gen_4285, q_gen_4286, q_gen_4287, q_gen_4288, q_gen_4289, q_gen_4290, q_gen_4291, q_gen_4292, q_gen_4293, q_gen_4294, q_gen_4295, q_gen_4296, q_gen_4297, q_gen_4298, q_gen_4299, q_gen_4300, q_gen_4301, q_gen_4302, q_gen_4303, q_gen_4304, q_gen_4305, q_gen_4306, q_gen_4307, q_gen_4308, q_gen_4309, q_gen_4310, q_gen_4311, q_gen_4312, q_gen_4313, q_gen_4314, q_gen_4315, q_gen_4316, q_gen_4317, q_gen_4318, q_gen_4319, q_gen_4320, q_gen_4321, q_gen_4322, q_gen_4323, q_gen_4324},
Q_f={},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s>(q_gen_4262) -> q_gen_4287
<z, z>() -> q_gen_4199
<s, s>(q_gen_4199) -> q_gen_4201
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4208) -> q_gen_4217
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4201) -> q_gen_4233
<s, s>(q_gen_4227) -> q_gen_4238
<z, s>(q_gen_4243) -> q_gen_4256
<s, s>(q_gen_4217) -> q_gen_4265
<s, s>(q_gen_4256) -> q_gen_4276
<z, s>(q_gen_4262) -> q_gen_4280
<s, s>(q_gen_4280) -> q_gen_4312
<z, s>(q_gen_4287) -> q_gen_4316
<z, z, z>() -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, z, s>(q_gen_4201) -> q_gen_4200
<s, z, s>(q_gen_4199) -> q_gen_4202
<s, s, s>(q_gen_4204) -> q_gen_4203
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4207) -> q_gen_4206
<s, z, s>(q_gen_4208) -> q_gen_4207
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, s, s>(q_gen_4212) -> q_gen_4211
<s, s, s>(q_gen_4198) -> q_gen_4212
<s, s, s>(q_gen_4214) -> q_gen_4213
<z, s, s>(q_gen_4208) -> q_gen_4214
<s, s, s>(q_gen_4216) -> q_gen_4215
<z, s, s>(q_gen_4217) -> q_gen_4216
<s, s, s>(q_gen_4219) -> q_gen_4218
<s, s, s>(q_gen_4220) -> q_gen_4219
<z, z, s>(q_gen_4221) -> q_gen_4220
<s, s, s>(q_gen_4223) -> q_gen_4222
<s, z, s>(q_gen_4217) -> q_gen_4223
<s, s, s>(q_gen_4225) -> q_gen_4224
<s, s, s>(q_gen_4226) -> q_gen_4225
<s, z, s>(q_gen_4227) -> q_gen_4226
<z, s, s>(q_gen_4227) -> q_gen_4228
<s, s, s>(q_gen_4230) -> q_gen_4229
<s, s, s>(q_gen_4228) -> q_gen_4230
<s, s, s>(q_gen_4203) -> q_gen_4231
<s, z, s>(q_gen_4233) -> q_gen_4232
<z, s, s>(q_gen_4201) -> q_gen_4234
<s, s, s>(q_gen_4236) -> q_gen_4235
<s, s, s>(q_gen_4237) -> q_gen_4236
<z, s, s>(q_gen_4238) -> q_gen_4237
<s, z, s>(q_gen_4238) -> q_gen_4239
<s, s, s>(q_gen_4241) -> q_gen_4240
<s, s, s>(q_gen_4242) -> q_gen_4241
<z, z, s>(q_gen_4243) -> q_gen_4242
<s, s, s>(q_gen_4202) -> q_gen_4244
<s, s, s>(q_gen_4231) -> q_gen_4245
<s, s, s>(q_gen_4210) -> q_gen_4246
<s, s, s>(q_gen_4240) -> q_gen_4247
<s, s, s>(q_gen_4211) -> q_gen_4248
<s, s, s>(q_gen_4250) -> q_gen_4249
<s, s, s>(q_gen_4244) -> q_gen_4250
<s, s, s>(q_gen_4245) -> q_gen_4251
<s, s, s>(q_gen_4253) -> q_gen_4252
<s, s, s>(q_gen_4254) -> q_gen_4253
<s, s, s>(q_gen_4255) -> q_gen_4254
<z, s, s>(q_gen_4256) -> q_gen_4255
<s, z, s>(q_gen_4256) -> q_gen_4257
<s, s, s>(q_gen_4257) -> q_gen_4258
<s, s, s>(q_gen_4260) -> q_gen_4259
<s, s, s>(q_gen_4261) -> q_gen_4260
<z, z, s>(q_gen_4262) -> q_gen_4261
<s, s, s>(q_gen_4264) -> q_gen_4263
<s, z, s>(q_gen_4265) -> q_gen_4264
<s, s, s>(q_gen_4267) -> q_gen_4266
<s, s, s>(q_gen_4239) -> q_gen_4267
<s, s, s>(q_gen_4269) -> q_gen_4268
<s, s, s>(q_gen_4258) -> q_gen_4269
<s, s, s>(q_gen_4271) -> q_gen_4270
<s, s, s>(q_gen_4259) -> q_gen_4271
<s, s, s>(q_gen_4273) -> q_gen_4272
<s, s, s>(q_gen_4274) -> q_gen_4273
<s, s, s>(q_gen_4275) -> q_gen_4274
<z, s, s>(q_gen_4276) -> q_gen_4275
<s, s, s>(q_gen_4249) -> q_gen_4277
<s, s, s>(q_gen_4251) -> q_gen_4278
<z, s, s>(q_gen_4280) -> q_gen_4279
<s, s, s>(q_gen_4282) -> q_gen_4281
<s, s, s>(q_gen_4283) -> q_gen_4282
<s, s, s>(q_gen_4213) -> q_gen_4283
<s, z, s>(q_gen_4280) -> q_gen_4284
<s, s, s>(q_gen_4286) -> q_gen_4285
<z, z, s>(q_gen_4287) -> q_gen_4286
<s, s, s>(q_gen_4289) -> q_gen_4288
<s, s, s>(q_gen_4290) -> q_gen_4289
<s, s, s>(q_gen_4200) -> q_gen_4290
<s, s, s>(q_gen_4292) -> q_gen_4291
<s, s, s>(q_gen_4293) -> q_gen_4292
<s, s, s>(q_gen_4206) -> q_gen_4293
<s, s, s>(q_gen_4218) -> q_gen_4294
<s, s, s>(q_gen_4288) -> q_gen_4295
<s, s, s>(q_gen_4291) -> q_gen_4296
<s, s, s>(q_gen_4294) -> q_gen_4297
<s, s, s>(q_gen_4246) -> q_gen_4298
<s, s, s>(q_gen_4300) -> q_gen_4299
<s, s, s>(q_gen_4297) -> q_gen_4300
<s, s, s>(q_gen_4302) -> q_gen_4301
<z, s, s>(q_gen_4265) -> q_gen_4302
<s, s, s>(q_gen_4304) -> q_gen_4303
<s, s, s>(q_gen_4305) -> q_gen_4304
<s, s, s>(q_gen_4306) -> q_gen_4305
<s, s, s>(q_gen_4279) -> q_gen_4306
<s, s, s>(q_gen_4248) -> q_gen_4307
<s, s, s>(q_gen_4268) -> q_gen_4308
<s, s, s>(q_gen_4270) -> q_gen_4309
<s, s, s>(q_gen_4311) -> q_gen_4310
<s, z, s>(q_gen_4312) -> q_gen_4311
<s, s, s>(q_gen_4314) -> q_gen_4313
<s, s, s>(q_gen_4315) -> q_gen_4314
<s, z, s>(q_gen_4316) -> q_gen_4315
<s, s, s>(q_gen_4318) -> q_gen_4317
<s, s, s>(q_gen_4319) -> q_gen_4318
<s, s, s>(q_gen_4320) -> q_gen_4319
<s, s, s>(q_gen_4284) -> q_gen_4320
<s, s, s>(q_gen_4322) -> q_gen_4321
<s, s, s>(q_gen_4323) -> q_gen_4322
<s, s, s>(q_gen_4324) -> q_gen_4323
<s, s, s>(q_gen_4285) -> q_gen_4324
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005957 s (model generation: 0.005297,  model checking: 0.000660):

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

}

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.005080 s (model generation: 0.004821,  model checking: 0.000259):

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

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

}
--
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: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 2, which took 0.004485 s (model generation: 0.004247,  model checking: 0.000238):

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

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 3, which took 0.004465 s (model generation: 0.004299,  model checking: 0.000166):

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

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

}
--
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: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 4, which took 0.005985 s (model generation: 0.004589,  model checking: 0.001396):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4205},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s, s>(q_gen_4197) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4205) -> q_gen_4197
<z, z, z>() -> q_gen_4197
}

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

}
--
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: Found: ((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.006802 s (model generation: 0.006244,  model checking: 0.000558):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 7
(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: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 6, which took 0.011602 s (model generation: 0.009379,  model checking: 0.002223):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s, s>(q_gen_4197) -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 7
(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: Found: ((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 7, which took 0.015803 s (model generation: 0.014768,  model checking: 0.001035):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s, s>(q_gen_4198) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4197) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 8
(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: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.021473 s (model generation: 0.018702,  model checking: 0.002771):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4198) -> q_gen_4198
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4197) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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]) -> 13
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 13
}
Sat witness: Found: ((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 9, which took 0.020395 s (model generation: 0.018219,  model checking: 0.002176):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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]) -> 13
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 16
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.022355 s (model generation: 0.019777,  model checking: 0.002578):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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)]) -> 19
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.025469 s (model generation: 0.022853,  model checking: 0.002616):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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)]) -> 22
}
Sat witness: Found: ((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.029335 s (model generation: 0.028697,  model checking: 0.000638):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4200, q_gen_4204, q_gen_4205, q_gen_4208},
Q_f={q_gen_4197, q_gen_4200},
Delta=
{
<s>(q_gen_4205) -> q_gen_4205
<z>() -> q_gen_4205
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4200) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4200
<s, z, s>(q_gen_4199) -> q_gen_4200
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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)]) -> 22
}
Sat witness: Found: ((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.027801 s (model generation: 0.026737,  model checking: 0.001064):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4201, q_gen_4202, q_gen_4204, q_gen_4205},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4205) -> q_gen_4205
<z>() -> q_gen_4205
<z, s>(q_gen_4205) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4199) -> q_gen_4201
<s, s, s>(q_gen_4202) -> q_gen_4197
<s, z, s>(q_gen_4201) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4201) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4202
<s, z, s>(q_gen_4199) -> q_gen_4202
<s, s, s>(q_gen_4197) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

}
--
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]) -> 18
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 22
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 14, which took 0.026086 s (model generation: 0.025450,  model checking: 0.000636):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4221) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 17
(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: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(s(z))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 15, which took 0.030390 s (model generation: 0.026895,  model checking: 0.003495):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 18
(plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 22
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 25
}
Sat witness: Found: ((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 16, which took 0.043926 s (model generation: 0.042808,  model checking: 0.001118):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4221) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 25
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 25
}
Sat witness: Found: ((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 17, which took 0.046136 s (model generation: 0.043961,  model checking: 0.002175):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4217, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<s, s>(q_gen_4208) -> q_gen_4217
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4217) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4217) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 25
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 28
}
Sat witness: Found: ((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 18, which took 0.051345 s (model generation: 0.049958,  model checking: 0.001387):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4200, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221},
Q_f={q_gen_4197, q_gen_4200},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4200) -> q_gen_4200
<s, s, s>(q_gen_4204) -> q_gen_4200
<s, z, s>(q_gen_4199) -> q_gen_4200
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 28
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 28
}
Sat witness: Found: ((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 -> s(s(z))
})

-------------------------------------------
Step 19, which took 0.054466 s (model generation: 0.053186,  model checking: 0.001280):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4201, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<z, z>() -> q_gen_4199
<s, s>(q_gen_4199) -> q_gen_4201
<z, s>(q_gen_4221) -> q_gen_4201
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<s, z, s>(q_gen_4201) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, s, s>(q_gen_4201) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 28
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 28
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(s(z)))
})

-------------------------------------------
Step 20, which took 0.059507 s (model generation: 0.057965,  model checking: 0.001542):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4201, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<z, z>() -> q_gen_4199
<s, s>(q_gen_4199) -> q_gen_4201
<s, s>(q_gen_4201) -> q_gen_4201
<z, s>(q_gen_4221) -> q_gen_4201
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<s, z, s>(q_gen_4201) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, s, s>(q_gen_4201) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 28
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 31
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 21, which took 0.062631 s (model generation: 0.061561,  model checking: 0.001070):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<s, z, s>(q_gen_4227) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 31
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 31
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(z)  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.068109 s (model generation: 0.064350,  model checking: 0.003759):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 31
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 34
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.059718 s (model generation: 0.058836,  model checking: 0.000882):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<s, s>(q_gen_4227) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 34
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 34
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 24, which took 0.064095 s (model generation: 0.061543,  model checking: 0.002552):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4203) -> q_gen_4203
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 34
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 37
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 25, which took 0.091399 s (model generation: 0.090863,  model checking: 0.000536):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4200, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197, q_gen_4200},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4200) -> q_gen_4200
<s, s, s>(q_gen_4204) -> q_gen_4200
<s, z, s>(q_gen_4199) -> q_gen_4200
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 37
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 37
}
Sat witness: Found: ((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(s(z))
})

-------------------------------------------
Step 26, which took 0.087437 s (model generation: 0.085893,  model checking: 0.001544):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<s>(q_gen_4221) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4203) -> q_gen_4203
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 40
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 38
}
Sat witness: Found: ((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(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 27, which took 0.086399 s (model generation: 0.085269,  model checking: 0.001130):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4221) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 40
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 41
}
Sat witness: Found: ((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 28, which took 0.041299 s (model generation: 0.039742,  model checking: 0.001557):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4221) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 43
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 41
}
Sat witness: Found: ((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 29, which took 0.064614 s (model generation: 0.063953,  model checking: 0.000661):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<s, s, s>(q_gen_4198) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 43
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 44
}
Sat witness: Found: ((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 30, which took 0.095404 s (model generation: 0.094683,  model checking: 0.000721):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4208
<s, s, s>(q_gen_4203) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 46
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 44
}
Sat witness: Found: ((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(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 31, which took 0.095393 s (model generation: 0.094360,  model checking: 0.001033):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4198) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<s, z, s>(q_gen_4227) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 46
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 47
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 32, which took 0.085837 s (model generation: 0.085427,  model checking: 0.000410):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4243) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 49
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 47
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> z  ;  _vw -> s(s(s(z)))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 33, which took 0.090097 s (model generation: 0.089295,  model checking: 0.000802):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4203) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4203
<z, s, s>(q_gen_4208) -> q_gen_4203
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<s, z, s>(q_gen_4227) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
}

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

}
--
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]) -> 49
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 50
}
Sat witness: Found: ((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 34, which took 0.097625 s (model generation: 0.096840,  model checking: 0.000785):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4213, q_gen_4214, q_gen_4220, q_gen_4221, q_gen_4227},
Q_f={q_gen_4197, q_gen_4213},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4221
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4213) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4214) -> q_gen_4213
<s, s, s>(q_gen_4220) -> q_gen_4214
<z, s, s>(q_gen_4208) -> q_gen_4214
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

}
--
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]) -> 52
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 50
}
Sat witness: Found: ((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 35, which took 0.060596 s (model generation: 0.058681,  model checking: 0.001915):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 52
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 53
}
Sat witness: Found: ((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 36, which took 0.149751 s (model generation: 0.148483,  model checking: 0.001268):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4243) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 55
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 53
}
Sat witness: Found: ((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 37, which took 0.116162 s (model generation: 0.114221,  model checking: 0.001941):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4242) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 55
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 56
}
Sat witness: Found: ((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 38, which took 0.173268 s (model generation: 0.172321,  model checking: 0.000947):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4197) -> q_gen_4204
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4242) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 58
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 56
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 39, which took 0.153203 s (model generation: 0.151906,  model checking: 0.001297):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4198) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4208) -> q_gen_4198
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 58
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 59
}
Sat witness: Found: ((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 40, which took 0.215781 s (model generation: 0.215412,  model checking: 0.000369):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4198) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4208) -> q_gen_4198
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 61
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 59
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(z))  ;  _vw -> s(z)  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 41, which took 0.195275 s (model generation: 0.192668,  model checking: 0.002607):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4198) -> q_gen_4204
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 64
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 60
}
Sat witness: Found: ((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 42, which took 0.204614 s (model generation: 0.203367,  model checking: 0.001247):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 64
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 63
}
Sat witness: Found: ((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 43, which took 0.232294 s (model generation: 0.228935,  model checking: 0.003359):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<s>(q_gen_4243) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4198) -> q_gen_4198
<s, s, s>(q_gen_4204) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 67
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 64
}
Sat witness: Found: ((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 -> s(z)
})

-------------------------------------------
Step 44, which took 0.195418 s (model generation: 0.192221,  model checking: 0.003197):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4243) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 67
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 67
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 45, which took 0.305748 s (model generation: 0.301756,  model checking: 0.003992):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4243) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4198) -> q_gen_4204
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 70
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 68
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 46, which took 0.356547 s (model generation: 0.355202,  model checking: 0.001345):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4243) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 70
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 71
}
Sat witness: Found: ((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 47, which took 0.589739 s (model generation: 0.589025,  model checking: 0.000714):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4243) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<s, s>(q_gen_4256) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 73
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 71
}
Sat witness: Found: ((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 48, which took 0.475033 s (model generation: 0.473762,  model checking: 0.001271):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4203) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 73
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 74
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 49, which took 0.316789 s (model generation: 0.316153,  model checking: 0.000636):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4203) -> q_gen_4203
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 76
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 74
}
Sat witness: Found: ((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(s(z))
})

-------------------------------------------
Step 50, which took 0.336891 s (model generation: 0.332856,  model checking: 0.004035):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4256) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4198) -> q_gen_4204
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4256) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 79
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 75
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 51, which took 0.568942 s (model generation: 0.565743,  model checking: 0.003199):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4198) -> q_gen_4204
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 82
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 76
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(z)))  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 52, which took 0.695674 s (model generation: 0.693408,  model checking: 0.002266):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4262) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 82
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 79
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 53, which took 0.707494 s (model generation: 0.706469,  model checking: 0.001025):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4213, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4213},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4213) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<z, s, s>(q_gen_4208) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4213
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 82
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 82
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 54, which took 0.755561 s (model generation: 0.752118,  model checking: 0.003443):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4206, q_gen_4207, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4206},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4206) -> q_gen_4206
<s, s, s>(q_gen_4207) -> q_gen_4206
<s, s, s>(q_gen_4209) -> q_gen_4207
<s, z, s>(q_gen_4208) -> q_gen_4207
<z, s, s>(q_gen_4208) -> q_gen_4207
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 85
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 83
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(z)))))  ;  _vw -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 55, which took 0.452109 s (model generation: 0.449331,  model checking: 0.002778):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4262) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4262) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 85
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 86
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 56, which took 0.809618 s (model generation: 0.809033,  model checking: 0.000585):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4262) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4262) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, s>(q_gen_4262) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 88
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 86
}
Sat witness: Found: ((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 57, which took 0.520422 s (model generation: 0.519435,  model checking: 0.000987):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4206, q_gen_4207, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4206},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4206) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4207) -> q_gen_4206
<s, s, s>(q_gen_4209) -> q_gen_4207
<s, z, s>(q_gen_4208) -> q_gen_4207
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 88
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 89
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 58, which took 0.992879 s (model generation: 0.991088,  model checking: 0.001791):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4218, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4218
<s, s, s>(q_gen_4218) -> q_gen_4218
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 91
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 89
}
Sat witness: Found: ((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(s(z)))
})

-------------------------------------------
Step 59, which took 0.862753 s (model generation: 0.859430,  model checking: 0.003323):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4203, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4203},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<s, s>(q_gen_4256) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4203
<s, s, s>(q_gen_4203) -> q_gen_4204
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 94
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 90
}
Sat witness: Found: ((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(s(s(z)))
})

-------------------------------------------
Step 60, which took 1.127960 s (model generation: 1.126879,  model checking: 0.001081):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4206, q_gen_4207, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4206},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4206) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4207) -> q_gen_4206
<s, s, s>(q_gen_4210) -> q_gen_4207
<s, z, s>(q_gen_4208) -> q_gen_4207
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 94
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 93
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(s(z))))))
})

-------------------------------------------
Step 61, which took 1.165962 s (model generation: 1.162686,  model checking: 0.003276):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4218, q_gen_4219, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<s, s, s>(q_gen_4218) -> q_gen_4218
<s, s, s>(q_gen_4219) -> q_gen_4218
<s, s, s>(q_gen_4210) -> q_gen_4219
}

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

}
--
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]) -> 97
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 94
}
Sat witness: Found: ((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 62, which took 1.585669 s (model generation: 1.585116,  model checking: 0.000553):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4218, q_gen_4219, q_gen_4221, q_gen_4227, q_gen_4243},
Q_f={q_gen_4197, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4218) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<s, s, s>(q_gen_4219) -> q_gen_4218
<s, s, s>(q_gen_4210) -> q_gen_4219
}

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

}
--
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]) -> 97
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 97
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(s(z))))))
})

-------------------------------------------
Step 63, which took 1.276512 s (model generation: 1.274876,  model checking: 0.001636):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4217, q_gen_4221, q_gen_4227, q_gen_4238, q_gen_4239, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4208) -> q_gen_4217
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4227) -> q_gen_4238
<s, s>(q_gen_4217) -> q_gen_4256
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4256) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<s, z, s>(q_gen_4217) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4217) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4239) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4238) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, z, s>(q_gen_4238) -> q_gen_4239
<z, z, s>(q_gen_4243) -> q_gen_4239
}

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

}
--
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]) -> 97
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 100
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 64, which took 2.948822 s (model generation: 2.947440,  model checking: 0.001382):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4220, q_gen_4221, q_gen_4224, q_gen_4227, q_gen_4242, q_gen_4243},
Q_f={q_gen_4197, q_gen_4224},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4227
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4224) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4220
<s, s, s>(q_gen_4210) -> q_gen_4224
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 100
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 100
}
Sat witness: Found: ((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(s(z)))))  ;  m -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 65, which took 1.194768 s (model generation: 1.192605,  model checking: 0.002163):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256, q_gen_4261, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4262) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4262) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, s, s>(q_gen_4261) -> q_gen_4242
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
<z, z, s>(q_gen_4262) -> q_gen_4261
}

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

}
--
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]) -> 100
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 103
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 66, which took 4.516441 s (model generation: 4.514597,  model checking: 0.001844):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256, q_gen_4261, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4262) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4262) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4209) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4242) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4209
<z, s, s>(q_gen_4227) -> q_gen_4209
<z, z, s>(q_gen_4221) -> q_gen_4209
<s, s, s>(q_gen_4261) -> q_gen_4242
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
<z, z, s>(q_gen_4262) -> q_gen_4261
}

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

}
--
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]) -> 103
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 103
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(s(s(s(s(s(z))))))  ;  _vw -> s(s(s(z)))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 67, which took 1.931410 s (model generation: 1.927416,  model checking: 0.003994):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4261, q_gen_4262},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4262) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, s>(q_gen_4262) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4261) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<z, z, s>(q_gen_4262) -> q_gen_4261
}

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

}
--
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]) -> 106
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 104
}
Sat witness: Found: ((plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]), {
_uw -> s(z)  ;  _vw -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 68, which took 2.341677 s (model generation: 2.340003,  model checking: 0.001674):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4261, q_gen_4262},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4262) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4262) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4261) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4198) -> q_gen_4210
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<z, z, s>(q_gen_4262) -> q_gen_4261
}

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

}
--
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]) -> 106
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 107
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(z))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 69, which took 2.160818 s (model generation: 2.160317,  model checking: 0.000501):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4218, q_gen_4219, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4243) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4218) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4209
<s, s, s>(q_gen_4219) -> q_gen_4218
<s, s, s>(q_gen_4220) -> q_gen_4219
<s, s, s>(q_gen_4242) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 109
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 107
}
Sat witness: Found: ((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(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 70, which took 3.678151 s (model generation: 3.677364,  model checking: 0.000787):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4211, q_gen_4218, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4198, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, s, s>(q_gen_4218) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4256) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4198) -> q_gen_4210
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4211
<s, s, s>(q_gen_4211) -> q_gen_4218
}

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

}
--
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]) -> 109
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 110
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 71, which took 3.019709 s (model generation: 3.016694,  model checking: 0.003015):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4217, q_gen_4221, q_gen_4227, q_gen_4238, q_gen_4243, q_gen_4256, q_gen_4265},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4208) -> q_gen_4217
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4227) -> q_gen_4238
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s>(q_gen_4217) -> q_gen_4265
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4210) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<s, z, s>(q_gen_4217) -> q_gen_4204
<s, z, s>(q_gen_4238) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4217) -> q_gen_4204
<z, s, s>(q_gen_4265) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4265) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<s, z, s>(q_gen_4256) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, s, s>(q_gen_4238) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
}

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

}
--
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]) -> 112
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 110
}
Sat witness: Found: ((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(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 72, which took 2.148678 s (model generation: 2.146216,  model checking: 0.002462):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4218, q_gen_4219, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4242, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, s, s>(q_gen_4218) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4209
<s, s, s>(q_gen_4219) -> q_gen_4218
<s, s, s>(q_gen_4220) -> q_gen_4219
<s, s, s>(q_gen_4242) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
<s, z, s>(q_gen_4256) -> q_gen_4242
<z, s, s>(q_gen_4256) -> q_gen_4242
<z, z, s>(q_gen_4243) -> q_gen_4242
}

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

}
--
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]) -> 112
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 113
}
Sat witness: Found: ((plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]), {
_pw -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 73, which took 2.534244 s (model generation: 2.532808,  model checking: 0.001436):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4211, q_gen_4218, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256},
Q_f={q_gen_4197, q_gen_4198, q_gen_4218},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4243
<s, s>(q_gen_4199) -> q_gen_4199
<s, s>(q_gen_4256) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<z, s>(q_gen_4243) -> q_gen_4256
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4218) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, s, s>(q_gen_4256) -> q_gen_4209
<z, z, s>(q_gen_4243) -> q_gen_4209
<s, s, s>(q_gen_4198) -> q_gen_4210
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4227) -> q_gen_4210
<s, z, s>(q_gen_4256) -> q_gen_4210
<z, s, s>(q_gen_4227) -> q_gen_4210
<z, z, s>(q_gen_4221) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4211
<s, s, s>(q_gen_4211) -> q_gen_4218
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 78
(plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 115
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 113
}
Sat witness: Found: ((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 74, which took 4.400682 s (model generation: 4.399513,  model checking: 0.001169):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4212, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s>(q_gen_4262) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<z, s>(q_gen_4262) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4212) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<z, z, s>(q_gen_4262) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4256) -> q_gen_4210
<z, s, s>(q_gen_4256) -> q_gen_4210
<z, z, s>(q_gen_4243) -> q_gen_4210
<s, s, s>(q_gen_4198) -> q_gen_4212
<s, s, s>(q_gen_4210) -> q_gen_4212
<s, z, s>(q_gen_4227) -> q_gen_4212
<z, s, s>(q_gen_4227) -> q_gen_4212
<z, z, s>(q_gen_4221) -> q_gen_4212
}

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

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

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

-------------------------------------------
Step 75, which took 3.531884 s (model generation: 3.530327,  model checking: 0.001557):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262, q_gen_4280},
Q_f={q_gen_4197},
Delta=
{
<s>(q_gen_4262) -> q_gen_4205
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<s, s>(q_gen_4280) -> q_gen_4280
<z, s>(q_gen_4262) -> q_gen_4280
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4280) -> q_gen_4209
<z, s, s>(q_gen_4280) -> q_gen_4209
<z, z, s>(q_gen_4262) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4256) -> q_gen_4210
<z, s, s>(q_gen_4256) -> q_gen_4210
<z, z, s>(q_gen_4243) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

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

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

-------------------------------------------
Step 76, which took 3.657124 s (model generation: 3.655155,  model checking: 0.001969):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4210, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4243, q_gen_4256, q_gen_4262, q_gen_4280},
Q_f={q_gen_4197},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4262) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<s, s>(q_gen_4208) -> q_gen_4208
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4227) -> q_gen_4227
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4256) -> q_gen_4256
<s, s>(q_gen_4280) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<z, s>(q_gen_4262) -> q_gen_4280
<s, s, s>(q_gen_4204) -> q_gen_4197
<s, z, s>(q_gen_4199) -> q_gen_4197
<z, s, s>(q_gen_4199) -> q_gen_4197
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, z, s>(q_gen_4280) -> q_gen_4209
<z, s, s>(q_gen_4280) -> q_gen_4209
<z, z, s>(q_gen_4262) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4210
<s, z, s>(q_gen_4256) -> q_gen_4210
<z, s, s>(q_gen_4256) -> q_gen_4210
<z, z, s>(q_gen_4243) -> q_gen_4210
<s, s, s>(q_gen_4210) -> q_gen_4220
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 81
(plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 118
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 119
}
Sat witness: Found: ((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(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 77, which took 4.020213 s (model generation: 4.017834,  model checking: 0.002379):

Model:
|_
{
plus -> 
{{{
Q={q_gen_4197, q_gen_4198, q_gen_4199, q_gen_4204, q_gen_4205, q_gen_4208, q_gen_4209, q_gen_4217, q_gen_4220, q_gen_4221, q_gen_4227, q_gen_4228, q_gen_4237, q_gen_4238, q_gen_4239, q_gen_4243, q_gen_4256, q_gen_4259, q_gen_4262, q_gen_4265},
Q_f={q_gen_4197, q_gen_4198},
Delta=
{
<z>() -> q_gen_4205
<s>(q_gen_4205) -> q_gen_4221
<s>(q_gen_4262) -> q_gen_4221
<s>(q_gen_4221) -> q_gen_4243
<s>(q_gen_4243) -> q_gen_4262
<s, s>(q_gen_4199) -> q_gen_4199
<z, z>() -> q_gen_4199
<z, s>(q_gen_4205) -> q_gen_4208
<s, s>(q_gen_4208) -> q_gen_4217
<z, s>(q_gen_4221) -> q_gen_4227
<s, s>(q_gen_4227) -> q_gen_4238
<s, s>(q_gen_4256) -> q_gen_4256
<z, s>(q_gen_4243) -> q_gen_4256
<z, s>(q_gen_4262) -> q_gen_4256
<s, s>(q_gen_4217) -> q_gen_4265
<z, z, z>() -> q_gen_4197
<s, s, s>(q_gen_4204) -> q_gen_4198
<s, z, s>(q_gen_4199) -> q_gen_4198
<z, s, s>(q_gen_4199) -> q_gen_4198
<s, s, s>(q_gen_4220) -> q_gen_4204
<s, s, s>(q_gen_4228) -> q_gen_4204
<s, s, s>(q_gen_4237) -> q_gen_4204
<s, z, s>(q_gen_4208) -> q_gen_4204
<s, z, s>(q_gen_4217) -> q_gen_4204
<z, s, s>(q_gen_4208) -> q_gen_4204
<z, s, s>(q_gen_4217) -> q_gen_4204
<z, s, s>(q_gen_4265) -> q_gen_4204
<z, z, s>(q_gen_4205) -> q_gen_4204
<s, s, s>(q_gen_4197) -> q_gen_4209
<s, s, s>(q_gen_4198) -> q_gen_4209
<s, s, s>(q_gen_4209) -> q_gen_4209
<s, z, s>(q_gen_4265) -> q_gen_4209
<s, z, s>(q_gen_4227) -> q_gen_4220
<z, z, s>(q_gen_4221) -> q_gen_4220
<z, s, s>(q_gen_4227) -> q_gen_4228
<s, s, s>(q_gen_4239) -> q_gen_4237
<s, z, s>(q_gen_4256) -> q_gen_4237
<z, s, s>(q_gen_4238) -> q_gen_4237
<s, z, s>(q_gen_4238) -> q_gen_4239
<z, s, s>(q_gen_4256) -> q_gen_4239
<z, z, s>(q_gen_4243) -> q_gen_4239
<s, s, s>(q_gen_4259) -> q_gen_4259
<z, z, s>(q_gen_4262) -> q_gen_4259
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 82
(plus([m, n, _vw]) /\ plus([n, m, _uw])) -> eq_nat([_uw, _vw]) -> 121
(plus([n, mm, _pw])) -> plus([n, s(mm), s(_pw)]) -> 119
}
Sat witness: Found: ((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(s(z)))  ;  n -> s(s(z))
})

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