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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(minus, F:
{() -> minus([s(u), z, s(u)])
() -> minus([z, y, z])
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw])}
(minus([_ow, _pw, _qw]) /\ minus([_ow, _pw, _rw])) -> eq_nat([_qw, _rw])
)
}

properties:
{(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw])}


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

Clause system for inference is:

{
() -> minus([s(u), z, s(u)]) -> 0
() -> minus([z, y, z]) -> 0
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 0
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 0
}


Solving took 66.622492 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5973, q_gen_5974, q_gen_5975, q_gen_5976, q_gen_5977, q_gen_5978, q_gen_5979, q_gen_5980, q_gen_5981, q_gen_5982, q_gen_5983, q_gen_5984, q_gen_5985, q_gen_5986, q_gen_5987, q_gen_5988, q_gen_5989, q_gen_5990, q_gen_5991, q_gen_5992, q_gen_5993, q_gen_5994, q_gen_5995, q_gen_5996, q_gen_5997, q_gen_5998, q_gen_5999, q_gen_6000, q_gen_6001, q_gen_6002, q_gen_6003, q_gen_6004, q_gen_6005, q_gen_6006, q_gen_6007, q_gen_6008, q_gen_6009, q_gen_6010, q_gen_6011, q_gen_6012, q_gen_6013, q_gen_6014, q_gen_6015, q_gen_6016, q_gen_6017, q_gen_6018, q_gen_6019, q_gen_6020, q_gen_6021, q_gen_6022, q_gen_6023, q_gen_6024, q_gen_6025, q_gen_6026, q_gen_6027, q_gen_6028, q_gen_6029, q_gen_6030, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6035, q_gen_6036, q_gen_6037, q_gen_6038, q_gen_6039, q_gen_6040, q_gen_6041, q_gen_6042, q_gen_6043, q_gen_6044, q_gen_6045, q_gen_6046, q_gen_6047, q_gen_6048, q_gen_6049, q_gen_6050, q_gen_6051, q_gen_6052, q_gen_6053, q_gen_6054, q_gen_6055, q_gen_6056, q_gen_6057, q_gen_6058, q_gen_6059, q_gen_6060, q_gen_6061, q_gen_6062, q_gen_6063, q_gen_6064, q_gen_6065, q_gen_6066, q_gen_6067, q_gen_6068, q_gen_6069, q_gen_6070, q_gen_6071, q_gen_6072, q_gen_6073, q_gen_6074, q_gen_6075, q_gen_6076, q_gen_6077, q_gen_6078, q_gen_6079, q_gen_6080, q_gen_6081, q_gen_6082, q_gen_6083, q_gen_6084, q_gen_6085, q_gen_6086, q_gen_6087, q_gen_6088, q_gen_6089, q_gen_6090, q_gen_6091},
Q_f={},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_6064
<z, z>() -> q_gen_5972
<s, s>(q_gen_5972) -> q_gen_5977
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5988
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_6014
<s, s>(q_gen_6022) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6022
<s, s>(q_gen_5977) -> q_gen_6027
<s, s>(q_gen_5984) -> q_gen_6029
<s, z>(q_gen_5993) -> q_gen_6037
<s, s>(q_gen_5988) -> q_gen_6040
<s, s>(q_gen_6052) -> q_gen_6051
<z, s>(q_gen_5993) -> q_gen_6052
<s, s>(q_gen_6037) -> q_gen_6081
<s, s>(q_gen_6014) -> q_gen_6085
<z, z, z>() -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5972) -> q_gen_5973
<z, s, z>(q_gen_5975) -> q_gen_5974
<s, z, s>(q_gen_5977) -> q_gen_5976
<s, s, s>(q_gen_5979) -> q_gen_5978
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<z, s, z>(q_gen_5982) -> q_gen_5981
<s, s, z>(q_gen_5984) -> q_gen_5983
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, s, s>(q_gen_5987) -> q_gen_5986
<s, z, s>(q_gen_5988) -> q_gen_5987
<s, s, s>(q_gen_5990) -> q_gen_5989
<s, s, s>(q_gen_5985) -> q_gen_5990
<s, z, z>(q_gen_5982) -> q_gen_5991
<z, s, z>(q_gen_5993) -> q_gen_5992
<s, s, s>(q_gen_5995) -> q_gen_5994
<s, s, z>(q_gen_5996) -> q_gen_5995
<s, s, s>(q_gen_5994) -> q_gen_5997
<s, s, s>(q_gen_5999) -> q_gen_5998
<s, s, z>(q_gen_5977) -> q_gen_5999
<s, s, s>(q_gen_5973) -> q_gen_6000
<s, s, s>(q_gen_5980) -> q_gen_6001
<s, s, s>(q_gen_6000) -> q_gen_6002
<s, s, s>(q_gen_5991) -> q_gen_6003
<s, s, s>(q_gen_6005) -> q_gen_6004
<s, z, s>(q_gen_5996) -> q_gen_6005
<s, s, s>(q_gen_6003) -> q_gen_6006
<s, s, s>(q_gen_6008) -> q_gen_6007
<s, s, s>(q_gen_5974) -> q_gen_6008
<s, s, s>(q_gen_6010) -> q_gen_6009
<s, s, s>(q_gen_5971) -> q_gen_6010
<s, s, s>(q_gen_6012) -> q_gen_6011
<s, s, s>(q_gen_5978) -> q_gen_6012
<s, s, z>(q_gen_6014) -> q_gen_6013
<s, s, s>(q_gen_6016) -> q_gen_6015
<s, z, z>(q_gen_5993) -> q_gen_6016
<s, s, s>(q_gen_5986) -> q_gen_6017
<s, s, s>(q_gen_5989) -> q_gen_6018
<s, s, s>(q_gen_6020) -> q_gen_6019
<s, z, s>(q_gen_6021) -> q_gen_6020
<s, s, s>(q_gen_6024) -> q_gen_6023
<s, z, s>(q_gen_6014) -> q_gen_6024
<s, s, s>(q_gen_6013) -> q_gen_6025
<s, z, s>(q_gen_6027) -> q_gen_6026
<s, z, s>(q_gen_6029) -> q_gen_6028
<s, s, s>(q_gen_5976) -> q_gen_6030
<s, s, z>(q_gen_6022) -> q_gen_6031
<s, z, s>(q_gen_6022) -> q_gen_6032
<s, s, s>(q_gen_6034) -> q_gen_6033
<s, s, s>(q_gen_6031) -> q_gen_6034
<s, s, s>(q_gen_6036) -> q_gen_6035
<s, z, s>(q_gen_6037) -> q_gen_6036
<s, s, s>(q_gen_6039) -> q_gen_6038
<s, z, s>(q_gen_6040) -> q_gen_6039
<s, s, s>(q_gen_5983) -> q_gen_6041
<s, s, z>(q_gen_6021) -> q_gen_6042
<s, s, s>(q_gen_6044) -> q_gen_6043
<s, s, s>(q_gen_6045) -> q_gen_6044
<s, s, s>(q_gen_5981) -> q_gen_6045
<s, s, s>(q_gen_6047) -> q_gen_6046
<s, s, s>(q_gen_6048) -> q_gen_6047
<s, s, s>(q_gen_6049) -> q_gen_6048
<s, s, z>(q_gen_5988) -> q_gen_6049
<s, s, z>(q_gen_6051) -> q_gen_6050
<s, s, s>(q_gen_6054) -> q_gen_6053
<s, s, s>(q_gen_6009) -> q_gen_6054
<s, s, s>(q_gen_6028) -> q_gen_6055
<s, s, s>(q_gen_6057) -> q_gen_6056
<s, s, s>(q_gen_6032) -> q_gen_6057
<s, s, s>(q_gen_6059) -> q_gen_6058
<s, s, s>(q_gen_6015) -> q_gen_6059
<s, s, z>(q_gen_6027) -> q_gen_6060
<s, s, z>(q_gen_6029) -> q_gen_6061
<s, s, s>(q_gen_6019) -> q_gen_6062
<z, s, z>(q_gen_6064) -> q_gen_6063
<s, s, s>(q_gen_6066) -> q_gen_6065
<s, s, s>(q_gen_6067) -> q_gen_6066
<s, z, s>(q_gen_6052) -> q_gen_6067
<s, s, s>(q_gen_6017) -> q_gen_6068
<s, s, s>(q_gen_6070) -> q_gen_6069
<s, s, s>(q_gen_6035) -> q_gen_6070
<s, s, s>(q_gen_6072) -> q_gen_6071
<s, s, s>(q_gen_6073) -> q_gen_6072
<s, s, s>(q_gen_6074) -> q_gen_6073
<s, s, s>(q_gen_6075) -> q_gen_6074
<s, z, z>(q_gen_6064) -> q_gen_6075
<s, s, s>(q_gen_6077) -> q_gen_6076
<s, s, s>(q_gen_6078) -> q_gen_6077
<s, s, z>(q_gen_6037) -> q_gen_6078
<s, s, z>(q_gen_6052) -> q_gen_6079
<s, s, z>(q_gen_6081) -> q_gen_6080
<s, s, z>(q_gen_6040) -> q_gen_6082
<s, s, s>(q_gen_6084) -> q_gen_6083
<s, z, s>(q_gen_6085) -> q_gen_6084
<s, s, s>(q_gen_6087) -> q_gen_6086
<s, s, s>(q_gen_5992) -> q_gen_6087
<s, s, s>(q_gen_6089) -> q_gen_6088
<s, s, z>(q_gen_6085) -> q_gen_6089
<s, s, s>(q_gen_6002) -> q_gen_6090
<s, s, s>(q_gen_6018) -> q_gen_6091
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008516 s (model generation: 0.008365,  model checking: 0.000151):

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

}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 1
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 1
}
Sat witness: Found: (() -> minus([z, y, z]), {
y -> z
})

-------------------------------------------
Step 1, which took 0.010790 s (model generation: 0.010584,  model checking: 0.000206):

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

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 1
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 1
}
Sat witness: Found: (() -> minus([s(u), z, s(u)]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.010395 s (model generation: 0.010251,  model checking: 0.000144):

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

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 1
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 4
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> z  ;  x2 -> z
})

-------------------------------------------
Step 3, which took 0.009581 s (model generation: 0.009411,  model checking: 0.000170):

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

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 2
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 4
}
Sat witness: Found: (() -> minus([z, y, z]), {
y -> s(z)
})

-------------------------------------------
Step 4, which took 0.014341 s (model generation: 0.014057,  model checking: 0.000284):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<z, z>() -> q_gen_5972
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 3
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 4
}
Sat witness: Found: (() -> minus([s(u), z, s(u)]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.013174 s (model generation: 0.012749,  model checking: 0.000425):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 4
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 7
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(z)  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 6, which took 0.012543 s (model generation: 0.011819,  model checking: 0.000724):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s, s>(q_gen_5970) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 7
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 7
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> s(z)  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 7, which took 0.012021 s (model generation: 0.011901,  model checking: 0.000120):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 7
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 7
}
Sat witness: Found: (() -> minus([z, y, z]), {
y -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.017407 s (model generation: 0.016965,  model checking: 0.000442):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 7
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 10
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> z  ;  x2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.012615 s (model generation: 0.012048,  model checking: 0.000567):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 10
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 10
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(z)  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 10, which took 0.012664 s (model generation: 0.012196,  model checking: 0.000468):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5984},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 10
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 13
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(z))))  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 11, which took 0.016210 s (model generation: 0.015510,  model checking: 0.000700):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5980, q_gen_5984},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, z>(q_gen_5972) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 13
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 13
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.014621 s (model generation: 0.014309,  model checking: 0.000312):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5982, q_gen_5984},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, z>(q_gen_5982) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 13
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 13
}
Sat witness: Found: (() -> minus([z, y, z]), {
y -> s(s(s(z)))
})

-------------------------------------------
Step 13, which took 0.016639 s (model generation: 0.016134,  model checking: 0.000505):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5984, q_gen_5985},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 13
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 16
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(z)  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 14, which took 0.020833 s (model generation: 0.019226,  model checking: 0.001607):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5973, q_gen_5975, q_gen_5979, q_gen_5984},
Q_f={q_gen_5970, q_gen_5973},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5973) -> q_gen_5973
<s, s, s>(q_gen_5979) -> q_gen_5973
<s, s, z>(q_gen_5972) -> q_gen_5973
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 16
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 16
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(z)  ;  _uw -> s(z)  ;  _vw -> z  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 15, which took 0.025246 s (model generation: 0.024807,  model checking: 0.000439):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5973, q_gen_5975, q_gen_5979, q_gen_5984},
Q_f={q_gen_5970, q_gen_5973},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5973) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5973
<s, s, z>(q_gen_5972) -> q_gen_5973
<z, s, z>(q_gen_5975) -> q_gen_5973
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 16
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 19
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(z))  ;  u -> s(s(z))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 16, which took 0.028941 s (model generation: 0.028466,  model checking: 0.000475):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5978, q_gen_5979, q_gen_5984},
Q_f={q_gen_5970, q_gen_5978},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5978) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5978
<s, s, z>(q_gen_5984) -> q_gen_5978
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 19
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 19
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> z  ;  _uw -> s(s(s(z)))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 17, which took 0.035399 s (model generation: 0.034855,  model checking: 0.000544):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 19
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 22
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(z))  ;  u -> s(s(z))  ;  x2 -> z
})

-------------------------------------------
Step 18, which took 0.041210 s (model generation: 0.040343,  model checking: 0.000867):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s, s>(q_gen_5971) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 22
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 22
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> z  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.039838 s (model generation: 0.039089,  model checking: 0.000749):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5984, q_gen_5985, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 22
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 25
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(z))  ;  u -> s(s(s(z)))  ;  x2 -> s(z)
})

-------------------------------------------
Step 20, which took 0.040426 s (model generation: 0.038224,  model checking: 0.002202):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5978, q_gen_5979, q_gen_5984, q_gen_5985, q_gen_5996},
Q_f={q_gen_5970, q_gen_5978},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5978) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5978
<s, s, z>(q_gen_5996) -> q_gen_5978
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, s, s>(q_gen_5985) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 25
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 25
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(s(z))  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 21, which took 0.044692 s (model generation: 0.044083,  model checking: 0.000609):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5974, q_gen_5975, q_gen_5979, q_gen_5984, q_gen_5985, q_gen_5996},
Q_f={q_gen_5970, q_gen_5974},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5974) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5974
<s, s, z>(q_gen_5996) -> q_gen_5974
<z, s, z>(q_gen_5975) -> q_gen_5974
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, s, s>(q_gen_5985) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 25
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 28
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 22, which took 0.063831 s (model generation: 0.061745,  model checking: 0.002086):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5974, q_gen_5975, q_gen_5979, q_gen_5982, q_gen_5984, q_gen_5991},
Q_f={q_gen_5970, q_gen_5974},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5974) -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5974
<z, s, z>(q_gen_5975) -> q_gen_5974
<s, s, s>(q_gen_5970) -> q_gen_5979
<s, s, s>(q_gen_5991) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, z>(q_gen_5982) -> q_gen_5991
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 28
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 28
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(s(z))  ;  _uw -> z  ;  _vw -> z  ;  k -> s(z)  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.058207 s (model generation: 0.057474,  model checking: 0.000733):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5973, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985},
Q_f={q_gen_5970, q_gen_5973},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5973) -> q_gen_5970
<s, s, s>(q_gen_5985) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5973
<s, s, z>(q_gen_5984) -> q_gen_5973
<s, z, z>(q_gen_5975) -> q_gen_5973
<z, s, z>(q_gen_5982) -> q_gen_5973
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 28
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 31
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 24, which took 0.063242 s (model generation: 0.061401,  model checking: 0.001841):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5973, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985},
Q_f={q_gen_5970, q_gen_5973},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5973) -> q_gen_5970
<s, s, s>(q_gen_5985) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5973
<s, s, z>(q_gen_5984) -> q_gen_5973
<s, z, z>(q_gen_5975) -> q_gen_5973
<z, s, z>(q_gen_5975) -> q_gen_5973
<z, s, z>(q_gen_5982) -> q_gen_5973
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 31
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 31
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 25, which took 0.065085 s (model generation: 0.064368,  model checking: 0.000717):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5985) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 31
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 34
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(z))  ;  x2 -> s(z)
})

-------------------------------------------
Step 26, which took 0.071166 s (model generation: 0.066611,  model checking: 0.004555):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, s>(q_gen_5985) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 34
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 34
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(z)  ;  _uw -> s(z)  ;  _vw -> z  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 27, which took 0.060441 s (model generation: 0.059174,  model checking: 0.001267):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 34
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 37
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 28, which took 0.060710 s (model generation: 0.058625,  model checking: 0.002085):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 37
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 37
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(z))))  ;  _tw -> s(z)  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 29, which took 0.068679 s (model generation: 0.067853,  model checking: 0.000826):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5978, q_gen_5979, q_gen_5980, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5978},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5996) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5978) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5978
<s, s, z>(q_gen_5996) -> q_gen_5978
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 37
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 40
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(z))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 30, which took 0.067855 s (model generation: 0.065784,  model checking: 0.002071):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5975) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5988) -> q_gen_5979
<s, z, s>(q_gen_5988) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 40
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 40
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(s(s(s(z))))  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 31, which took 0.066451 s (model generation: 0.065550,  model checking: 0.000901):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 40
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 43
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(s(z)))))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 32, which took 0.073213 s (model generation: 0.072665,  model checking: 0.000548):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5978, q_gen_5979, q_gen_5980, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5978},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5978) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5978
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 43
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 43
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(z)))  ;  _tw -> s(z)  ;  _uw -> s(s(s(z)))  ;  _vw -> s(s(z))  ;  k -> s(z)  ;  m -> s(s(s(s(z))))  ;  n -> s(z)
})

-------------------------------------------
Step 33, which took 0.101592 s (model generation: 0.101001,  model checking: 0.000591):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5996) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 31
() -> minus([z, y, z]) -> 32
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 43
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 46
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(z)  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 34, which took 0.104695 s (model generation: 0.103864,  model checking: 0.000831):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5996) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 32
() -> minus([z, y, z]) -> 33
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 46
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 46
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(z)))  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 35, which took 0.112853 s (model generation: 0.112363,  model checking: 0.000490):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5977, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, z>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5972) -> q_gen_5977
<z, s>(q_gen_5982) -> q_gen_5977
<s, s>(q_gen_5977) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_5977) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_5977) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 46
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 46
}
Sat witness: Found: (() -> minus([s(u), z, s(u)]), {
u -> s(s(z))
})

-------------------------------------------
Step 36, which took 0.122635 s (model generation: 0.121051,  model checking: 0.001584):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5977, q_gen_5979, q_gen_5980, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5975) -> q_gen_5975
<z>() -> q_gen_5975
<z, z>() -> q_gen_5972
<s, s>(q_gen_5972) -> q_gen_5977
<s, s>(q_gen_5977) -> q_gen_5977
<s, s>(q_gen_5996) -> q_gen_5977
<z, s>(q_gen_5975) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5977) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5977) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 46
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 49
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(s(z)))  ;  x2 -> z
})

-------------------------------------------
Step 37, which took 0.129667 s (model generation: 0.127904,  model checking: 0.001763):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<s, z>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 49
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 49
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(z)))  ;  _tw -> s(s(s(s(z))))  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 38, which took 0.122001 s (model generation: 0.120733,  model checking: 0.001268):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, z>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 49
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 52
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(z))  ;  x2 -> z
})

-------------------------------------------
Step 39, which took 0.136646 s (model generation: 0.134239,  model checking: 0.002407):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<s, z>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 52
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 52
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 40, which took 0.176179 s (model generation: 0.175348,  model checking: 0.000831):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5977, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5977) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5972) -> q_gen_5977
<s, z>(q_gen_5982) -> q_gen_5977
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5972) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, z, s>(q_gen_5977) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_5977) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 52
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 55
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> s(z)  ;  x2 -> s(z)
})

-------------------------------------------
Step 41, which took 0.152189 s (model generation: 0.147046,  model checking: 0.005143):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_6021) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, s, z>(q_gen_6021) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 55
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 55
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 42, which took 0.140908 s (model generation: 0.139179,  model checking: 0.001729):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5988
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5988) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 55
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 58
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(z))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 43, which took 0.190721 s (model generation: 0.189162,  model checking: 0.001559):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996, q_gen_6014},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_6014) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_6014
<s, z>(q_gen_5982) -> q_gen_6014
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, s, z>(q_gen_6014) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_6014) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, z>(q_gen_5982) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 58
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 58
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(s(z)))))  ;  _tw -> s(s(z))  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 44, which took 0.370537 s (model generation: 0.369831,  model checking: 0.000706):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996, q_gen_6014},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<s, s>(q_gen_6014) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_6014
<s, z>(q_gen_5982) -> q_gen_6014
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, s, z>(q_gen_6014) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_6014) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, z>(q_gen_5982) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 58
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 61
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(z)  ;  u -> s(z)  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 45, which took 0.391976 s (model generation: 0.391089,  model checking: 0.000887):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<s, s>(q_gen_5988) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5972) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_5988) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 61
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 61
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 46, which took 0.295028 s (model generation: 0.292903,  model checking: 0.002125):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_5988) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 61
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 64
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 47, which took 0.523719 s (model generation: 0.518957,  model checking: 0.004762):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_5988) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 64
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 64
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(z)  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 48, which took 0.526435 s (model generation: 0.524819,  model checking: 0.001616):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 48
() -> minus([z, y, z]) -> 46
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 64
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 67
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(s(z)))))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 49, which took 0.571945 s (model generation: 0.568614,  model checking: 0.003331):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 49
() -> minus([z, y, z]) -> 47
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 67
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 67
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(z))))  ;  _tw -> s(z)  ;  _uw -> s(z)  ;  _vw -> s(s(s(z)))  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 50, which took 0.524147 s (model generation: 0.522619,  model checking: 0.001528):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 50
() -> minus([z, y, z]) -> 48
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 67
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 70
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(s(s(s(z)))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 51, which took 0.723296 s (model generation: 0.720855,  model checking: 0.002441):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, z, s>(q_gen_6021) -> q_gen_5985
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 51
() -> minus([z, y, z]) -> 49
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 70
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 70
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(z))))  ;  _tw -> s(z)  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 52, which took 0.863622 s (model generation: 0.862812,  model checking: 0.000810):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5982) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5984) -> q_gen_6021
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5975) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 52
() -> minus([z, y, z]) -> 50
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 70
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 73
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> s(z)  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 53, which took 0.842606 s (model generation: 0.840932,  model checking: 0.001674):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, z>(q_gen_5988) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, z, z>(q_gen_5982) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 53
() -> minus([z, y, z]) -> 51
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 73
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 73
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(z)
})

-------------------------------------------
Step 54, which took 0.709708 s (model generation: 0.709085,  model checking: 0.000623):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5988, q_gen_5996},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5988) -> q_gen_5988
<s, z>(q_gen_5982) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_5988) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 54
() -> minus([z, y, z]) -> 52
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 73
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 76
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> z  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 55, which took 0.958387 s (model generation: 0.954382,  model checking: 0.004005):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 55
() -> minus([z, y, z]) -> 53
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 76
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 76
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(s(z)))))  ;  _tw -> s(s(z))  ;  _uw -> z  ;  _vw -> z  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 56, which took 1.025237 s (model generation: 1.024549,  model checking: 0.000688):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, z, s>(q_gen_6021) -> q_gen_5985
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 56
() -> minus([z, y, z]) -> 54
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 76
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 79
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(z)))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(z)
})

-------------------------------------------
Step 57, which took 1.001448 s (model generation: 0.999670,  model checking: 0.001778):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5991, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5982
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, s>(q_gen_5991) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5991
<s, z, s>(q_gen_6021) -> q_gen_5991
<s, z, z>(q_gen_5982) -> q_gen_5991
}

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

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

Teacher's answer:
New clause system:
{
() -> minus([s(u), z, s(u)]) -> 57
() -> minus([z, y, z]) -> 55
(minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 79
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 79
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(z))))  ;  _tw -> s(s(s(z)))  ;  _uw -> s(s(z))  ;  _vw -> s(s(z))  ;  k -> z  ;  m -> s(s(s(s(s(z)))))  ;  n -> s(s(z))
})

-------------------------------------------
Step 58, which took 1.034731 s (model generation: 1.034487,  model checking: 0.000244):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, z>(q_gen_5993) -> q_gen_5996
<z, s>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 79
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 79
}
Sat witness: Found: (() -> minus([z, y, z]), {
y -> s(s(s(s(z))))
})

-------------------------------------------
Step 59, which took 1.350833 s (model generation: 1.349975,  model checking: 0.000858):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5993) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<z, s>(q_gen_5993) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 79
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 82
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(s(s(z))))))  ;  u -> s(s(s(z)))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 60, which took 1.021433 s (model generation: 1.019653,  model checking: 0.001780):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5993) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5993) -> q_gen_5972
<z, s>(q_gen_5982) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<z, s>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5984) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 82
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 82
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(z))))  ;  _tw -> s(z)  ;  _uw -> s(z)  ;  _vw -> z  ;  k -> s(s(z))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 61, which took 1.454356 s (model generation: 1.453201,  model checking: 0.001155):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5993) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<s, z>(q_gen_5993) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<z, s>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 82
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 85
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(s(s(z)))))))  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 62, which took 1.947969 s (model generation: 1.934597,  model checking: 0.013372):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 85
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 85
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(s(z)))))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 63, which took 2.437404 s (model generation: 2.436347,  model checking: 0.001057):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5993) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<z, s>(q_gen_5993) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 85
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 88
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> z  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 64, which took 2.072872 s (model generation: 2.069174,  model checking: 0.003698):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<s, z>(q_gen_5993) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 88
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 88
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(s(z))  ;  k -> z  ;  m -> s(s(s(s(z))))  ;  n -> s(s(z))
})

-------------------------------------------
Step 65, which took 2.016862 s (model generation: 2.015847,  model checking: 0.001015):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, s>(q_gen_5993) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, z>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 88
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 91
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(z))))  ;  u -> s(z)  ;  x2 -> z
})

-------------------------------------------
Step 66, which took 1.793953 s (model generation: 1.787234,  model checking: 0.006719):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, z>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 91
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 91
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(s(z)))))  ;  _tw -> s(s(z))  ;  _uw -> z  ;  _vw -> z  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 67, which took 2.102849 s (model generation: 2.100866,  model checking: 0.001983):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5993) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, z>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 91
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 94
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> s(s(s(z)))  ;  x2 -> z
})

-------------------------------------------
Step 68, which took 3.777910 s (model generation: 3.776371,  model checking: 0.001539):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5988, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5988
<s, z>(q_gen_5993) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5988) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_5988) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, s, z>(q_gen_5972) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5993) -> q_gen_5971
<s, s, s>(q_gen_5971) -> q_gen_5979
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5984) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_5988) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 94
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 94
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(s(s(z)))  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 69, which took 2.199205 s (model generation: 2.197945,  model checking: 0.001260):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5987, q_gen_5988, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, z>(q_gen_5993) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5988) -> q_gen_6021
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_5988) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5987) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5987
<s, s, z>(q_gen_6021) -> q_gen_5987
<s, z, s>(q_gen_5988) -> q_gen_5987
<s, z, s>(q_gen_6021) -> q_gen_5987
<s, z, z>(q_gen_5982) -> q_gen_5987
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 94
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 97
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> z  ;  u -> s(z)  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 70, which took 1.648017 s (model generation: 1.641899,  model checking: 0.006118):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5989, q_gen_5993, q_gen_5996, q_gen_6021},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, z>(q_gen_5993) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5989) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, z, z>(q_gen_5993) -> q_gen_5986
<s, s, s>(q_gen_5986) -> q_gen_5989
<s, s, z>(q_gen_6021) -> q_gen_5989
<s, z, s>(q_gen_6021) -> q_gen_5989
<s, z, z>(q_gen_5982) -> q_gen_5989
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 97
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 97
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(z)  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(z)  ;  k -> s(z)  ;  m -> s(s(s(s(z))))  ;  n -> s(s(z))
})

-------------------------------------------
Step 71, which took 2.405513 s (model generation: 2.404377,  model checking: 0.001136):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5993, q_gen_5996, q_gen_6021, q_gen_6029},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, s>(q_gen_6029) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, s>(q_gen_5984) -> q_gen_6029
<s, z>(q_gen_5993) -> q_gen_6029
<z, s>(q_gen_5993) -> q_gen_6029
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_6029) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, z, s>(q_gen_6029) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 97
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 100
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(s(z))))))  ;  x2 -> s(s(z))
})

-------------------------------------------
Step 72, which took 2.942931 s (model generation: 2.932928,  model checking: 0.010003):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5993, q_gen_5996, q_gen_6021, q_gen_6037},
Q_f={q_gen_5970},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, s>(q_gen_6037) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6037
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_6037) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_6037) -> q_gen_5970
<s, z, z>(q_gen_5993) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 100
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 100
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> z  ;  _tw -> z  ;  _uw -> s(s(z))  ;  _vw -> s(s(z))  ;  k -> z  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 73, which took 2.397872 s (model generation: 2.396332,  model checking: 0.001540):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021, q_gen_6022},
Q_f={q_gen_5970},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5993) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6022) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6022
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<s, z, s>(q_gen_6021) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6022) -> q_gen_5986
<s, z, s>(q_gen_6022) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 100
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 103
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(z))))  ;  u -> s(s(s(s(s(z)))))  ;  x2 -> s(z)
})

-------------------------------------------
Step 74, which took 2.816795 s (model generation: 2.813313,  model checking: 0.003482):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5993, q_gen_5996, q_gen_6021, q_gen_6022},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5993) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6022) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6022
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5971) -> q_gen_5971
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5993) -> q_gen_5971
<s, s, s>(q_gen_5980) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_6022) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5985) -> q_gen_5980
<s, s, z>(q_gen_6022) -> q_gen_5980
<s, z, s>(q_gen_6021) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5985
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, z, z>(q_gen_5993) -> q_gen_5985
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 103
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 103
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(z))  ;  _tw -> s(s(z))  ;  _uw -> s(z)  ;  _vw -> s(z)  ;  k -> s(s(s(s(z))))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 75, which took 3.824018 s (model generation: 3.821932,  model checking: 0.002086):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5971, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5991, q_gen_5993, q_gen_5996, q_gen_6014, q_gen_6021},
Q_f={q_gen_5970, q_gen_5971},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_6021) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_5996) -> q_gen_6014
<s, z>(q_gen_5982) -> q_gen_6014
<s, s>(q_gen_6014) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6021
<s, s, s>(q_gen_5971) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, z, s>(q_gen_6021) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5971
<s, z, s>(q_gen_5972) -> q_gen_5971
<z, s, z>(q_gen_5982) -> q_gen_5971
<s, s, s>(q_gen_5991) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, s, z>(q_gen_6014) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_6014) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, s, s>(q_gen_5980) -> q_gen_5980
<s, s, z>(q_gen_6021) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, z>(q_gen_5982) -> q_gen_5991
<s, z, z>(q_gen_5993) -> q_gen_5991
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 103
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 106
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(z)  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(s(z)))
})

-------------------------------------------
Step 76, which took 5.043770 s (model generation: 5.033239,  model checking: 0.010531):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5973, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5986, q_gen_5993, q_gen_5996, q_gen_6021, q_gen_6037},
Q_f={q_gen_5970, q_gen_5973},
Delta=
{
<s>(q_gen_5993) -> q_gen_5975
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5984) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5982) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5996) -> q_gen_5996
<s, s>(q_gen_6037) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6037
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_6037) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, s, s>(q_gen_5979) -> q_gen_5973
<s, s, z>(q_gen_5972) -> q_gen_5973
<z, s, z>(q_gen_5993) -> q_gen_5973
<s, s, s>(q_gen_5986) -> q_gen_5979
<s, s, z>(q_gen_5996) -> q_gen_5979
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5980
<s, z, s>(q_gen_6037) -> q_gen_5980
<s, z, z>(q_gen_5993) -> q_gen_5980
<s, s, s>(q_gen_5973) -> q_gen_5986
<s, s, s>(q_gen_5980) -> q_gen_5986
<s, s, z>(q_gen_6021) -> q_gen_5986
<s, z, s>(q_gen_6021) -> q_gen_5986
<s, z, z>(q_gen_5982) -> q_gen_5986
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 106
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 106
}
Sat witness: Found: ((minus([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]), {
_sw -> s(s(s(s(s(z)))))  ;  _tw -> s(z)  ;  _uw -> s(s(s(z)))  ;  _vw -> z  ;  k -> s(s(s(z)))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 77, which took 3.034063 s (model generation: 3.030371,  model checking: 0.003692):

Model:
|_
{
minus -> 
{{{
Q={q_gen_5970, q_gen_5972, q_gen_5975, q_gen_5979, q_gen_5980, q_gen_5982, q_gen_5984, q_gen_5985, q_gen_5986, q_gen_5987, q_gen_5988, q_gen_5989, q_gen_5990, q_gen_5991, q_gen_5993, q_gen_5995, q_gen_5996, q_gen_6003, q_gen_6017, q_gen_6018, q_gen_6021, q_gen_6034, q_gen_6037, q_gen_6047},
Q_f={q_gen_5970, q_gen_6018, q_gen_6034},
Delta=
{
<z>() -> q_gen_5975
<s>(q_gen_5975) -> q_gen_5982
<s>(q_gen_5982) -> q_gen_5993
<s>(q_gen_5993) -> q_gen_5993
<s, s>(q_gen_5972) -> q_gen_5972
<z, z>() -> q_gen_5972
<s, s>(q_gen_5988) -> q_gen_5984
<z, s>(q_gen_5975) -> q_gen_5984
<z, s>(q_gen_5993) -> q_gen_5984
<s, s>(q_gen_5984) -> q_gen_5988
<z, s>(q_gen_5982) -> q_gen_5988
<s, s>(q_gen_5996) -> q_gen_5996
<s, s>(q_gen_6037) -> q_gen_5996
<s, z>(q_gen_5975) -> q_gen_5996
<s, s>(q_gen_6021) -> q_gen_6021
<s, z>(q_gen_5982) -> q_gen_6021
<s, z>(q_gen_5993) -> q_gen_6037
<s, s, s>(q_gen_5979) -> q_gen_5970
<s, s, s>(q_gen_5995) -> q_gen_5970
<s, s, s>(q_gen_6003) -> q_gen_5970
<s, s, z>(q_gen_5972) -> q_gen_5970
<s, s, z>(q_gen_5984) -> q_gen_5970
<s, s, z>(q_gen_6037) -> q_gen_5970
<s, z, s>(q_gen_5972) -> q_gen_5970
<z, s, z>(q_gen_5975) -> q_gen_5970
<z, s, z>(q_gen_5982) -> q_gen_5970
<z, s, z>(q_gen_5993) -> q_gen_5970
<z, z, z>() -> q_gen_5970
<s, z, s>(q_gen_5996) -> q_gen_5979
<s, z, z>(q_gen_5975) -> q_gen_5979
<s, s, s>(q_gen_5970) -> q_gen_5980
<s, z, s>(q_gen_5984) -> q_gen_5985
<s, s, s>(q_gen_5987) -> q_gen_5986
<s, z, s>(q_gen_5988) -> q_gen_5987
<s, z, s>(q_gen_6037) -> q_gen_5987
<s, z, z>(q_gen_5993) -> q_gen_5987
<s, s, s>(q_gen_5990) -> q_gen_5989
<s, s, s>(q_gen_5980) -> q_gen_5990
<s, s, s>(q_gen_5985) -> q_gen_5990
<s, z, s>(q_gen_6021) -> q_gen_5990
<s, z, z>(q_gen_5982) -> q_gen_5991
<s, s, z>(q_gen_5996) -> q_gen_5995
<s, s, s>(q_gen_5991) -> q_gen_6003
<s, s, s>(q_gen_5986) -> q_gen_6017
<s, s, z>(q_gen_6021) -> q_gen_6017
<s, s, s>(q_gen_5989) -> q_gen_6018
<s, s, s>(q_gen_6034) -> q_gen_6018
<s, s, s>(q_gen_6017) -> q_gen_6034
<s, s, s>(q_gen_6047) -> q_gen_6034
<s, s, z>(q_gen_5988) -> q_gen_6034
<s, s, s>(q_gen_6018) -> q_gen_6047
}

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

}
--
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([_sw, s(k), _tw]) /\ minus([_uw, k, _vw]) /\ minus([m, n, _uw]) /\ minus([s(m), n, _sw])) -> eq_nat([_tw, _vw]) -> 106
(minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]) -> 109
}
Sat witness: Found: ((minus([u, x2, _nw])) -> minus([s(u), s(x2), _nw]), {
_nw -> s(s(s(s(s(s(z))))))  ;  u -> s(s(s(s(z))))  ;  x2 -> s(s(s(z)))
})

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