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


Learning problem is:

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

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


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

Clause system for inference is:

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


Solving took 63.184236 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5393, q_gen_5394, q_gen_5395, q_gen_5396, q_gen_5397, q_gen_5398, q_gen_5399, q_gen_5400, q_gen_5401, q_gen_5402, q_gen_5403, q_gen_5404, q_gen_5405, q_gen_5406, q_gen_5407, q_gen_5408, q_gen_5409, q_gen_5410, q_gen_5411, q_gen_5412, q_gen_5413, q_gen_5414, q_gen_5415, q_gen_5416, q_gen_5417, q_gen_5418, q_gen_5419, q_gen_5420, q_gen_5421, q_gen_5422, q_gen_5423, q_gen_5424, q_gen_5425, q_gen_5426, q_gen_5427, q_gen_5428, q_gen_5429, q_gen_5430, q_gen_5431, q_gen_5432, q_gen_5433, q_gen_5434, q_gen_5435, q_gen_5436, q_gen_5437, q_gen_5438, q_gen_5439, q_gen_5440, q_gen_5441, q_gen_5442, q_gen_5443, q_gen_5444, q_gen_5445, q_gen_5446, q_gen_5447, q_gen_5448, q_gen_5449, q_gen_5450, q_gen_5451, q_gen_5452, q_gen_5453, q_gen_5454, q_gen_5455, q_gen_5456, q_gen_5457, q_gen_5458, q_gen_5459, q_gen_5460, q_gen_5461, q_gen_5462, q_gen_5463, q_gen_5464, q_gen_5465, q_gen_5466, q_gen_5467, q_gen_5468, q_gen_5469, q_gen_5470, q_gen_5471, q_gen_5472, q_gen_5473, q_gen_5474, q_gen_5475, q_gen_5476, q_gen_5477, q_gen_5478, q_gen_5479, q_gen_5480, q_gen_5481, q_gen_5482, q_gen_5483, q_gen_5484, q_gen_5485, q_gen_5486, q_gen_5487, q_gen_5488, q_gen_5489, q_gen_5490, q_gen_5491, q_gen_5492, q_gen_5493, q_gen_5494, q_gen_5495, q_gen_5496, q_gen_5497, q_gen_5498, q_gen_5499, q_gen_5500, q_gen_5501, q_gen_5502, q_gen_5503, q_gen_5504, q_gen_5505, q_gen_5506, q_gen_5507, q_gen_5508, q_gen_5509, q_gen_5510},
Q_f={},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5478
<s>(q_gen_5478) -> q_gen_5507
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5408
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5397) -> q_gen_5442
<z, s>(q_gen_5413) -> q_gen_5444
<s, z>(q_gen_5402) -> q_gen_5448
<s, s>(q_gen_5434) -> q_gen_5464
<s, s>(q_gen_5448) -> q_gen_5468
<s, s>(q_gen_5496) -> q_gen_5495
<s, s>(q_gen_5442) -> q_gen_5496
<z, z, z>() -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, z>(q_gen_5392) -> q_gen_5393
<z, s, z>(q_gen_5395) -> q_gen_5394
<s, z, s>(q_gen_5397) -> q_gen_5396
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<z, s, z>(q_gen_5402) -> q_gen_5401
<s, s, z>(q_gen_5404) -> q_gen_5403
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, s, s>(q_gen_5407) -> q_gen_5406
<s, z, s>(q_gen_5408) -> q_gen_5407
<s, s, s>(q_gen_5410) -> q_gen_5409
<s, s, s>(q_gen_5405) -> q_gen_5410
<s, z, z>(q_gen_5402) -> q_gen_5411
<z, s, z>(q_gen_5413) -> q_gen_5412
<s, s, s>(q_gen_5415) -> q_gen_5414
<s, s, z>(q_gen_5416) -> q_gen_5415
<s, s, s>(q_gen_5414) -> q_gen_5417
<s, s, s>(q_gen_5419) -> q_gen_5418
<s, s, z>(q_gen_5397) -> q_gen_5419
<s, s, s>(q_gen_5393) -> q_gen_5420
<s, s, s>(q_gen_5400) -> q_gen_5421
<s, s, s>(q_gen_5420) -> q_gen_5422
<s, s, s>(q_gen_5411) -> q_gen_5423
<s, s, s>(q_gen_5425) -> q_gen_5424
<s, z, s>(q_gen_5416) -> q_gen_5425
<s, s, s>(q_gen_5423) -> q_gen_5426
<s, s, s>(q_gen_5428) -> q_gen_5427
<s, s, s>(q_gen_5394) -> q_gen_5428
<s, s, s>(q_gen_5430) -> q_gen_5429
<s, s, s>(q_gen_5391) -> q_gen_5430
<s, s, s>(q_gen_5432) -> q_gen_5431
<s, s, s>(q_gen_5398) -> q_gen_5432
<s, s, z>(q_gen_5434) -> q_gen_5433
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, s, z>(q_gen_5408) -> q_gen_5437
<s, s, s>(q_gen_5439) -> q_gen_5438
<s, z, s>(q_gen_5434) -> q_gen_5439
<s, s, s>(q_gen_5433) -> q_gen_5440
<s, z, s>(q_gen_5442) -> q_gen_5441
<s, z, s>(q_gen_5444) -> q_gen_5443
<s, s, s>(q_gen_5446) -> q_gen_5445
<s, s, s>(q_gen_5447) -> q_gen_5446
<s, s, z>(q_gen_5448) -> q_gen_5447
<s, s, s>(q_gen_5450) -> q_gen_5449
<s, s, z>(q_gen_5442) -> q_gen_5450
<s, s, s>(q_gen_5452) -> q_gen_5451
<s, z, s>(q_gen_5448) -> q_gen_5452
<s, s, s>(q_gen_5427) -> q_gen_5453
<s, s, s>(q_gen_5455) -> q_gen_5454
<s, s, s>(q_gen_5456) -> q_gen_5455
<s, s, s>(q_gen_5403) -> q_gen_5456
<s, s, s>(q_gen_5437) -> q_gen_5457
<s, s, s>(q_gen_5459) -> q_gen_5458
<s, s, s>(q_gen_5443) -> q_gen_5459
<s, s, s>(q_gen_5461) -> q_gen_5460
<s, s, s>(q_gen_5406) -> q_gen_5461
<s, s, s>(q_gen_5463) -> q_gen_5462
<s, z, s>(q_gen_5464) -> q_gen_5463
<s, s, s>(q_gen_5466) -> q_gen_5465
<s, s, s>(q_gen_5467) -> q_gen_5466
<s, z, s>(q_gen_5468) -> q_gen_5467
<s, s, s>(q_gen_5451) -> q_gen_5469
<s, s, s>(q_gen_5471) -> q_gen_5470
<s, s, s>(q_gen_5472) -> q_gen_5471
<s, s, s>(q_gen_5473) -> q_gen_5472
<s, z, z>(q_gen_5413) -> q_gen_5473
<s, s, z>(q_gen_5468) -> q_gen_5474
<s, s, s>(q_gen_5469) -> q_gen_5475
<s, s, s>(q_gen_5470) -> q_gen_5476
<z, s, z>(q_gen_5478) -> q_gen_5477
<s, s, s>(q_gen_5409) -> q_gen_5479
<s, s, s>(q_gen_5481) -> q_gen_5480
<s, s, s>(q_gen_5438) -> q_gen_5481
<s, s, s>(q_gen_5429) -> q_gen_5482
<s, s, z>(q_gen_5444) -> q_gen_5483
<s, s, s>(q_gen_5485) -> q_gen_5484
<s, s, s>(q_gen_5486) -> q_gen_5485
<s, s, s>(q_gen_5435) -> q_gen_5486
<s, s, s>(q_gen_5488) -> q_gen_5487
<s, s, s>(q_gen_5474) -> q_gen_5488
<s, s, s>(q_gen_5490) -> q_gen_5489
<s, s, z>(q_gen_5464) -> q_gen_5490
<s, s, s>(q_gen_5479) -> q_gen_5491
<s, s, s>(q_gen_5493) -> q_gen_5492
<s, z, z>(q_gen_5478) -> q_gen_5493
<s, z, s>(q_gen_5495) -> q_gen_5494
<s, z, s>(q_gen_5496) -> q_gen_5497
<s, s, s>(q_gen_5458) -> q_gen_5498
<s, s, s>(q_gen_5460) -> q_gen_5499
<s, s, s>(q_gen_5492) -> q_gen_5500
<s, s, s>(q_gen_5482) -> q_gen_5501
<s, s, z>(q_gen_5496) -> q_gen_5502
<s, s, s>(q_gen_5491) -> q_gen_5503
<s, s, s>(q_gen_5500) -> q_gen_5504
<s, z, s>(q_gen_5436) -> q_gen_5505
<z, s, z>(q_gen_5507) -> q_gen_5506
<s, s, s>(q_gen_5505) -> q_gen_5508
<s, s, s>(q_gen_5510) -> q_gen_5509
<s, s, s>(q_gen_5508) -> q_gen_5510
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005638 s (model generation: 0.005463,  model checking: 0.000175):

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.005016 s (model generation: 0.004750,  model checking: 0.000266):

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

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

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

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

-------------------------------------------
Step 2, which took 0.005602 s (model generation: 0.005122,  model checking: 0.000480):

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

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

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

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

-------------------------------------------
Step 3, which took 0.005173 s (model generation: 0.004665,  model checking: 0.000508):

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

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

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

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

-------------------------------------------
Step 4, which took 0.007893 s (model generation: 0.005184,  model checking: 0.002709):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<z, z>() -> q_gen_5392
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
}

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

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

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

-------------------------------------------
Step 5, which took 0.006360 s (model generation: 0.006078,  model checking: 0.000282):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
}

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

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

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

-------------------------------------------
Step 6, which took 0.010466 s (model generation: 0.008599,  model checking: 0.001867):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s, s>(q_gen_5390) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
}

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

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

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

-------------------------------------------
Step 7, which took 0.013596 s (model generation: 0.013295,  model checking: 0.000301):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 8, which took 0.015869 s (model generation: 0.014158,  model checking: 0.001711):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 9, which took 0.015730 s (model generation: 0.014139,  model checking: 0.001591):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 10, which took 0.015596 s (model generation: 0.014715,  model checking: 0.000881):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5404},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 11, which took 0.020865 s (model generation: 0.019384,  model checking: 0.001481):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5400, q_gen_5404},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5391) -> q_gen_5391
<s, s, z>(q_gen_5392) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, z, z>(q_gen_5395) -> q_gen_5391
<z, s, z>(q_gen_5395) -> q_gen_5391
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 12, which took 0.023164 s (model generation: 0.022405,  model checking: 0.000759):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, s>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, z>(q_gen_5402) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 13, which took 0.014115 s (model generation: 0.012799,  model checking: 0.001316):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5404, q_gen_5405},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 14, which took 0.015999 s (model generation: 0.012562,  model checking: 0.003437):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5393, q_gen_5395, q_gen_5399, q_gen_5404},
Q_f={q_gen_5390, q_gen_5393},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5393) -> q_gen_5393
<s, s, s>(q_gen_5399) -> q_gen_5393
<s, s, z>(q_gen_5392) -> q_gen_5393
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 15, which took 0.018158 s (model generation: 0.017361,  model checking: 0.000797):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5393, q_gen_5395, q_gen_5399, q_gen_5404},
Q_f={q_gen_5390, q_gen_5393},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5393) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5393
<s, s, z>(q_gen_5392) -> q_gen_5393
<z, s, z>(q_gen_5395) -> q_gen_5393
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 16, which took 0.018194 s (model generation: 0.017405,  model checking: 0.000789):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5398, q_gen_5399, q_gen_5404},
Q_f={q_gen_5390, q_gen_5398},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5398) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, s, z>(q_gen_5404) -> q_gen_5398
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
}

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

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

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

-------------------------------------------
Step 17, which took 0.020046 s (model generation: 0.019598,  model checking: 0.000448):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5400, q_gen_5402, q_gen_5404},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s, z>(q_gen_5392) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5391) -> q_gen_5391
<s, s, z>(q_gen_5404) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, z, z>(q_gen_5395) -> q_gen_5391
<z, s, z>(q_gen_5395) -> q_gen_5391
<z, s, z>(q_gen_5402) -> q_gen_5391
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 18, which took 0.023242 s (model generation: 0.021268,  model checking: 0.001974):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5400, q_gen_5402, q_gen_5404},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s, s>(q_gen_5391) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5391
<s, s, z>(q_gen_5404) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, z, z>(q_gen_5395) -> q_gen_5391
<z, s, z>(q_gen_5402) -> q_gen_5391
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 19, which took 0.022819 s (model generation: 0.021840,  model checking: 0.000979):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 20, which took 0.025162 s (model generation: 0.022672,  model checking: 0.002490):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5398, q_gen_5399, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390, q_gen_5398},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5398) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, s, z>(q_gen_5416) -> q_gen_5398
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 21, which took 0.033707 s (model generation: 0.033118,  model checking: 0.000589):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5394, q_gen_5395, q_gen_5399, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390, q_gen_5394},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5394) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5394
<s, s, z>(q_gen_5416) -> q_gen_5394
<z, s, z>(q_gen_5395) -> q_gen_5394
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 22, which took 0.042875 s (model generation: 0.034017,  model checking: 0.008858):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5398, q_gen_5399, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390, q_gen_5398},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5398) -> q_gen_5398
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 23, which took 0.043239 s (model generation: 0.042306,  model checking: 0.000933):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5394, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404, q_gen_5411},
Q_f={q_gen_5390, q_gen_5394},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, s>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5394) -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5394
<z, s, z>(q_gen_5395) -> q_gen_5394
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 24, which took 0.042015 s (model generation: 0.040672,  model checking: 0.001343):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5394, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404, q_gen_5411},
Q_f={q_gen_5390, q_gen_5394},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<s, s>(q_gen_5404) -> q_gen_5392
<z, s>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<s, s, s>(q_gen_5394) -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5394
<z, s, z>(q_gen_5395) -> q_gen_5394
<z, s, z>(q_gen_5402) -> q_gen_5394
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 25, which took 0.051431 s (model generation: 0.050544,  model checking: 0.000887):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5408},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s>(q_gen_5408) -> q_gen_5408
<s, z>(q_gen_5395) -> q_gen_5408
<z, s>(q_gen_5402) -> q_gen_5408
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, s, z>(q_gen_5408) -> q_gen_5399
<s, z, s>(q_gen_5408) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, z>(q_gen_5402) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 26, which took 0.046474 s (model generation: 0.045021,  model checking: 0.001453):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 27, which took 0.062140 s (model generation: 0.061084,  model checking: 0.001056):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<s, s>(q_gen_5416) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, z>(q_gen_5402) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 28, which took 0.101639 s (model generation: 0.100807,  model checking: 0.000832):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s>(q_gen_5416) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, s, z>(q_gen_5404) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 29, which took 0.096137 s (model generation: 0.095210,  model checking: 0.000927):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, s>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 30, which took 0.104695 s (model generation: 0.103099,  model checking: 0.001596):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, s>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 31, which took 0.097892 s (model generation: 0.097367,  model checking: 0.000525):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 32, which took 0.138503 s (model generation: 0.136879,  model checking: 0.001624):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<s, z>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5390) -> q_gen_5399
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, z>(q_gen_5402) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 33, which took 0.152730 s (model generation: 0.152193,  model checking: 0.000537):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<s, s>(q_gen_5416) -> q_gen_5397
<s, s>(q_gen_5397) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5397) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, z>(q_gen_5397) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 34, which took 0.083361 s (model generation: 0.082723,  model checking: 0.000638):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5397) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<s, s>(q_gen_5416) -> q_gen_5397
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5397) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, z>(q_gen_5397) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 35, which took 0.112421 s (model generation: 0.111826,  model checking: 0.000595):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5404, q_gen_5416, q_gen_5434},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5395) -> q_gen_5395
<z>() -> q_gen_5395
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5434) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 36, which took 0.112831 s (model generation: 0.111581,  model checking: 0.001250):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, z>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, s, z>(q_gen_5404) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5391) -> q_gen_5399
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 37, which took 0.162274 s (model generation: 0.161490,  model checking: 0.000784):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5403, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5403},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, z>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, s, s>(q_gen_5403) -> q_gen_5403
<s, s, z>(q_gen_5404) -> q_gen_5403
}

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

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

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

-------------------------------------------
Step 38, which took 0.198345 s (model generation: 0.197463,  model checking: 0.000882):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5397) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<s, z>(q_gen_5402) -> q_gen_5397
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5397) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5397) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 39, which took 0.214949 s (model generation: 0.213693,  model checking: 0.001256):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<s, z>(q_gen_5402) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, s, z>(q_gen_5392) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<z, s, z>(q_gen_5395) -> q_gen_5391
<s, s, s>(q_gen_5391) -> q_gen_5399
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 40, which took 0.188706 s (model generation: 0.187693,  model checking: 0.001013):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 41, which took 0.268346 s (model generation: 0.265285,  model checking: 0.003061):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5416, q_gen_5434},
Q_f={q_gen_5390, q_gen_5399},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, z>(q_gen_5402) -> q_gen_5434
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5434) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, z>(q_gen_5416) -> q_gen_5411
<s, s, z>(q_gen_5434) -> q_gen_5411
<s, z, s>(q_gen_5416) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 42, which took 0.211717 s (model generation: 0.209732,  model checking: 0.001985):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5436},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5391) -> q_gen_5391
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 43, which took 0.388992 s (model generation: 0.384580,  model checking: 0.004412):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5408, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5408
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, s, z>(q_gen_5408) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5404) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5408) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 44, which took 0.253816 s (model generation: 0.252634,  model checking: 0.001182):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s>(q_gen_5448) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 45, which took 0.600991 s (model generation: 0.593822,  model checking: 0.007169):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5408, q_gen_5416, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<s, s>(q_gen_5436) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5408
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, s, z>(q_gen_5408) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5408) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 46, which took 0.361217 s (model generation: 0.360440,  model checking: 0.000777):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5436},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5436) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, s>(q_gen_5391) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 47, which took 0.466084 s (model generation: 0.451691,  model checking: 0.014393):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5436},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5436) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5391) -> q_gen_5391
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 48, which took 0.478600 s (model generation: 0.477981,  model checking: 0.000619):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5413, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<z, s>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 49, which took 0.402010 s (model generation: 0.400573,  model checking: 0.001437):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5413, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<z, s>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 50, which took 0.552775 s (model generation: 0.544503,  model checking: 0.008272):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5398, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5416, q_gen_5436},
Q_f={q_gen_5390, q_gen_5398},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5436) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5398) -> q_gen_5398
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
}

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

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

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

-------------------------------------------
Step 51, which took 0.611991 s (model generation: 0.611263,  model checking: 0.000728):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5406, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390, q_gen_5399},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5448) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5406) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<z, s, z>(q_gen_5402) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5406
<s, s, z>(q_gen_5416) -> q_gen_5406
<s, z, s>(q_gen_5416) -> q_gen_5406
}

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

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

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

-------------------------------------------
Step 52, which took 0.653303 s (model generation: 0.647352,  model checking: 0.005951):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5416, q_gen_5434, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5448
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5448) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, s>(q_gen_5434) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 53, which took 0.564846 s (model generation: 0.563582,  model checking: 0.001264):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5413, q_gen_5416, q_gen_5444},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5444) -> q_gen_5444
<s, z>(q_gen_5402) -> q_gen_5444
<z, s>(q_gen_5413) -> q_gen_5444
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5400
<s, s, z>(q_gen_5444) -> q_gen_5400
<s, z, s>(q_gen_5444) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 54, which took 0.709126 s (model generation: 0.702379,  model checking: 0.006747):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390, q_gen_5391},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<z, s, z>(q_gen_5402) -> q_gen_5391
<s, s, s>(q_gen_5391) -> q_gen_5399
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 55, which took 0.571673 s (model generation: 0.569651,  model checking: 0.002022):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5413, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 56, which took 0.747126 s (model generation: 0.743801,  model checking: 0.003325):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5413, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5400) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5402) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, z>(q_gen_5413) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 57, which took 0.706305 s (model generation: 0.704928,  model checking: 0.001377):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5398, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390, q_gen_5398},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5398) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5448) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5398
<s, s, z>(q_gen_5404) -> q_gen_5398
<s, s, s>(q_gen_5405) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, z>(q_gen_5402) -> q_gen_5405
}

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

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

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

-------------------------------------------
Step 58, which took 0.681282 s (model generation: 0.672368,  model checking: 0.008914):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5416, q_gen_5434, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5402) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5448
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5434) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 59, which took 1.110899 s (model generation: 1.109972,  model checking: 0.000927):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5406, q_gen_5413, q_gen_5416, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5406) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5406
<s, s, z>(q_gen_5448) -> q_gen_5406
<s, z, s>(q_gen_5448) -> q_gen_5406
<s, z, z>(q_gen_5402) -> q_gen_5406
}

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

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

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

-------------------------------------------
Step 60, which took 0.669730 s (model generation: 0.664482,  model checking: 0.005248):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5436) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5434) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 61, which took 0.728520 s (model generation: 0.726974,  model checking: 0.001546):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5416, q_gen_5436, q_gen_5468},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5402) -> q_gen_5436
<s, s>(q_gen_5436) -> q_gen_5468
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5468) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5468) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 62, which took 1.125928 s (model generation: 1.115549,  model checking: 0.010379):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5402
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5436
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5434) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 63, which took 1.221634 s (model generation: 1.219986,  model checking: 0.001648):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<s, s>(q_gen_5434) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5434) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 64, which took 0.858958 s (model generation: 0.846542,  model checking: 0.012416):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5413) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, z>(q_gen_5413) -> q_gen_5434
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5434) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 65, which took 1.122888 s (model generation: 1.120832,  model checking: 0.002056):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5434) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 66, which took 1.070025 s (model generation: 1.057386,  model checking: 0.012639):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5434) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 67, which took 0.872081 s (model generation: 0.869874,  model checking: 0.002207):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5448) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5436) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 68, which took 1.146673 s (model generation: 1.131105,  model checking: 0.015568):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5402) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5434) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 69, which took 0.842240 s (model generation: 0.840515,  model checking: 0.001725):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5406, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5406) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5406
<s, s, z>(q_gen_5448) -> q_gen_5406
<s, z, s>(q_gen_5448) -> q_gen_5406
<s, z, z>(q_gen_5402) -> q_gen_5406
}

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

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

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

-------------------------------------------
Step 70, which took 0.915612 s (model generation: 0.888596,  model checking: 0.027016):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5413) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5434) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 71, which took 1.383499 s (model generation: 1.382226,  model checking: 0.001273):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5407, q_gen_5408, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5408
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, s, z>(q_gen_5408) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5407) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5407
<s, s, z>(q_gen_5448) -> q_gen_5407
<s, z, s>(q_gen_5408) -> q_gen_5407
<s, z, s>(q_gen_5448) -> q_gen_5407
<s, z, z>(q_gen_5402) -> q_gen_5407
}

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

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

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

-------------------------------------------
Step 72, which took 0.872293 s (model generation: 0.855375,  model checking: 0.016918):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5434, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5416) -> q_gen_5434
<s, s>(q_gen_5434) -> q_gen_5434
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, s, z>(q_gen_5434) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5434) -> q_gen_5400
<s, z, s>(q_gen_5448) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 73, which took 2.012518 s (model generation: 1.998078,  model checking: 0.014440):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5413) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 74, which took 2.969813 s (model generation: 2.960215,  model checking: 0.009598):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, s, s>(q_gen_5400) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 75, which took 2.640538 s (model generation: 2.638541,  model checking: 0.001997):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5406, q_gen_5409, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5409) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5406
<s, s, z>(q_gen_5436) -> q_gen_5406
<s, z, z>(q_gen_5413) -> q_gen_5406
<s, s, s>(q_gen_5406) -> q_gen_5409
<s, s, z>(q_gen_5448) -> q_gen_5409
<s, z, s>(q_gen_5448) -> q_gen_5409
<s, z, z>(q_gen_5402) -> q_gen_5409
}

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

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

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

-------------------------------------------
Step 76, which took 1.895230 s (model generation: 1.877590,  model checking: 0.017640):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5413
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 77, which took 2.042578 s (model generation: 2.041564,  model checking: 0.001014):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5413
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5397) -> q_gen_5436
<s, s>(q_gen_5436) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5397) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5397) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, s, s>(q_gen_5400) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 78, which took 1.941508 s (model generation: 1.941212,  model checking: 0.000296):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5405, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5436, q_gen_5448},
Q_f={q_gen_5390},
Delta=
{
<s>(q_gen_5413) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, s>(q_gen_5436) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5397) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5397) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, s>(q_gen_5397) -> q_gen_5390
<s, z, s>(q_gen_5436) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, z>(q_gen_5413) -> q_gen_5400
<s, s, s>(q_gen_5405) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, s, s>(q_gen_5400) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
}

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

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

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

-------------------------------------------
Step 79, which took 4.470855 s (model generation: 4.470546,  model checking: 0.000309):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448, q_gen_5478},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5478
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5478) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5478) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5436) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 80, which took 4.315929 s (model generation: 4.299757,  model checking: 0.016172):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448, q_gen_5478},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5478) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5478
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5478) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5436) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, z>(q_gen_5478) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 81, which took 3.816936 s (model generation: 3.815432,  model checking: 0.001504):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448, q_gen_5478},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5478
<s>(q_gen_5478) -> q_gen_5478
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5478) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5478) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, z, s>(q_gen_5436) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 82, which took 4.177210 s (model generation: 4.170784,  model checking: 0.006426):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5392, q_gen_5395, q_gen_5399, q_gen_5400, q_gen_5402, q_gen_5404, q_gen_5411, q_gen_5413, q_gen_5416, q_gen_5435, q_gen_5436, q_gen_5448, q_gen_5478},
Q_f={q_gen_5390},
Delta=
{
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<s>(q_gen_5413) -> q_gen_5478
<s>(q_gen_5478) -> q_gen_5478
<s, s>(q_gen_5392) -> q_gen_5392
<z, z>() -> q_gen_5392
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5404
<z, s>(q_gen_5413) -> q_gen_5404
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5399) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5404) -> q_gen_5390
<s, z, s>(q_gen_5392) -> q_gen_5390
<s, z, z>(q_gen_5478) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, s, z>(q_gen_5402) -> q_gen_5390
<z, s, z>(q_gen_5413) -> q_gen_5390
<z, s, z>(q_gen_5478) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5411) -> q_gen_5399
<s, s, z>(q_gen_5416) -> q_gen_5399
<s, z, s>(q_gen_5416) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, s>(q_gen_5400) -> q_gen_5400
<s, z, s>(q_gen_5404) -> q_gen_5400
<s, s, s>(q_gen_5435) -> q_gen_5411
<s, s, z>(q_gen_5448) -> q_gen_5411
<s, z, s>(q_gen_5448) -> q_gen_5411
<s, z, z>(q_gen_5402) -> q_gen_5411
<s, s, z>(q_gen_5436) -> q_gen_5435
<s, z, s>(q_gen_5436) -> q_gen_5435
<s, z, z>(q_gen_5413) -> q_gen_5435
}

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

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

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

-------------------------------------------
Step 83, which took 4.013766 s (model generation: 4.013391,  model checking: 0.000375):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5390, q_gen_5391, q_gen_5392, q_gen_5395, q_gen_5397, q_gen_5399, q_gen_5400, q_gen_5401, q_gen_5402, q_gen_5403, q_gen_5404, q_gen_5405, q_gen_5407, q_gen_5408, q_gen_5413, q_gen_5415, q_gen_5416, q_gen_5419, q_gen_5424, q_gen_5425, q_gen_5436, q_gen_5444, q_gen_5448, q_gen_5458, q_gen_5459, q_gen_5481},
Q_f={q_gen_5390, q_gen_5391, q_gen_5401, q_gen_5403, q_gen_5419, q_gen_5424},
Delta=
{
<s>(q_gen_5413) -> q_gen_5395
<z>() -> q_gen_5395
<s>(q_gen_5395) -> q_gen_5402
<s>(q_gen_5402) -> q_gen_5413
<z, z>() -> q_gen_5392
<s, s>(q_gen_5392) -> q_gen_5397
<s, s>(q_gen_5444) -> q_gen_5404
<z, s>(q_gen_5395) -> q_gen_5404
<z, s>(q_gen_5402) -> q_gen_5408
<s, s>(q_gen_5416) -> q_gen_5416
<s, z>(q_gen_5395) -> q_gen_5416
<s, s>(q_gen_5397) -> q_gen_5436
<s, z>(q_gen_5413) -> q_gen_5436
<s, s>(q_gen_5436) -> q_gen_5444
<z, s>(q_gen_5413) -> q_gen_5444
<s, s>(q_gen_5448) -> q_gen_5448
<s, z>(q_gen_5402) -> q_gen_5448
<s, s, s>(q_gen_5415) -> q_gen_5390
<s, s, z>(q_gen_5392) -> q_gen_5390
<s, s, z>(q_gen_5408) -> q_gen_5390
<s, s, z>(q_gen_5444) -> q_gen_5390
<z, s, z>(q_gen_5395) -> q_gen_5390
<z, z, z>() -> q_gen_5390
<s, s, s>(q_gen_5399) -> q_gen_5391
<s, z, s>(q_gen_5392) -> q_gen_5391
<s, z, s>(q_gen_5397) -> q_gen_5391
<s, s, s>(q_gen_5403) -> q_gen_5399
<s, z, z>(q_gen_5395) -> q_gen_5399
<s, s, s>(q_gen_5390) -> q_gen_5400
<s, s, z>(q_gen_5436) -> q_gen_5400
<s, z, s>(q_gen_5444) -> q_gen_5401
<z, s, z>(q_gen_5402) -> q_gen_5401
<z, s, z>(q_gen_5413) -> q_gen_5401
<s, s, s>(q_gen_5407) -> q_gen_5403
<s, s, z>(q_gen_5404) -> q_gen_5403
<s, s, s>(q_gen_5391) -> q_gen_5405
<s, s, s>(q_gen_5400) -> q_gen_5405
<s, s, s>(q_gen_5419) -> q_gen_5405
<s, s, z>(q_gen_5448) -> q_gen_5405
<s, z, s>(q_gen_5404) -> q_gen_5405
<s, z, s>(q_gen_5448) -> q_gen_5405
<s, z, z>(q_gen_5402) -> q_gen_5405
<s, s, s>(q_gen_5405) -> q_gen_5407
<s, z, s>(q_gen_5408) -> q_gen_5407
<s, s, s>(q_gen_5458) -> q_gen_5415
<s, s, z>(q_gen_5416) -> q_gen_5415
<s, s, z>(q_gen_5397) -> q_gen_5419
<s, z, s>(q_gen_5436) -> q_gen_5419
<s, s, s>(q_gen_5425) -> q_gen_5424
<s, z, s>(q_gen_5416) -> q_gen_5425
<s, s, s>(q_gen_5459) -> q_gen_5458
<s, s, s>(q_gen_5401) -> q_gen_5459
<s, s, s>(q_gen_5481) -> q_gen_5459
<s, z, z>(q_gen_5413) -> q_gen_5459
<s, s, s>(q_gen_5424) -> q_gen_5481
}

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

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

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

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