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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)])}
(plus([_gh, _hh, _ih]) /\ plus([_gh, _hh, _jh])) -> eq_nat([_ih, _jh])
)
}

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


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

Clause system for inference is:

{
() -> plus([n, z, n]) -> 0
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 0
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 0
}


Solving took 64.414257 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1936, q_gen_1937, q_gen_1938, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1947, q_gen_1948, q_gen_1949, q_gen_1950, q_gen_1951, q_gen_1952, q_gen_1953, q_gen_1954, q_gen_1955, q_gen_1956, q_gen_1957, q_gen_1958, q_gen_1959, q_gen_1960, q_gen_1961, q_gen_1962, q_gen_1963, q_gen_1964, q_gen_1965, q_gen_1966, q_gen_1967, q_gen_1968, q_gen_1969, q_gen_1970, q_gen_1971, q_gen_1972, q_gen_1973, q_gen_1974, q_gen_1975, q_gen_1976, q_gen_1977, q_gen_1978, q_gen_1979, q_gen_1980, q_gen_1981, q_gen_1982, q_gen_1983, q_gen_1984, q_gen_1985, q_gen_1986, q_gen_1987, q_gen_1988, q_gen_1989, q_gen_1990, q_gen_1991, q_gen_1992, q_gen_1993, q_gen_1994, q_gen_1995, q_gen_1996, q_gen_1997, q_gen_1998, q_gen_1999, q_gen_2000, q_gen_2001, q_gen_2002, q_gen_2003, q_gen_2004, q_gen_2005, q_gen_2006, q_gen_2007, q_gen_2008, q_gen_2009, q_gen_2010, q_gen_2011, q_gen_2012, q_gen_2013, q_gen_2014, q_gen_2015, q_gen_2016, q_gen_2017, q_gen_2018, q_gen_2019, q_gen_2020, q_gen_2021, q_gen_2022, q_gen_2023, q_gen_2024, q_gen_2025, q_gen_2026, q_gen_2027, q_gen_2028, q_gen_2029, q_gen_2030, q_gen_2031, q_gen_2032, q_gen_2033, q_gen_2034, q_gen_2035, q_gen_2036, q_gen_2037, q_gen_2038, q_gen_2039, q_gen_2040, q_gen_2041, q_gen_2042, q_gen_2043, q_gen_2044, q_gen_2045, q_gen_2046, q_gen_2047, q_gen_2048},
Q_f={},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<z, z>() -> q_gen_1935
<s, s>(q_gen_1935) -> q_gen_1937
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1944) -> q_gen_1953
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1937) -> q_gen_1981
<s, s>(q_gen_1961) -> q_gen_1983
<z, s>(q_gen_1970) -> q_gen_1990
<s, s>(q_gen_1990) -> q_gen_2001
<z, s>(q_gen_1994) -> q_gen_2005
<s, s>(q_gen_1953) -> q_gen_2018
<s, s>(q_gen_1983) -> q_gen_2037
<z, z, z>() -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, z, s>(q_gen_1937) -> q_gen_1936
<s, z, s>(q_gen_1935) -> q_gen_1938
<s, s, s>(q_gen_1940) -> q_gen_1939
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1943) -> q_gen_1942
<s, z, s>(q_gen_1944) -> q_gen_1943
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, s, s>(q_gen_1948) -> q_gen_1947
<s, s, s>(q_gen_1934) -> q_gen_1948
<s, s, s>(q_gen_1950) -> q_gen_1949
<z, s, s>(q_gen_1944) -> q_gen_1950
<s, s, s>(q_gen_1952) -> q_gen_1951
<z, s, s>(q_gen_1953) -> q_gen_1952
<s, s, s>(q_gen_1955) -> q_gen_1954
<s, s, s>(q_gen_1956) -> q_gen_1955
<z, z, s>(q_gen_1957) -> q_gen_1956
<s, s, s>(q_gen_1959) -> q_gen_1958
<s, s, s>(q_gen_1960) -> q_gen_1959
<z, s, s>(q_gen_1961) -> q_gen_1960
<s, z, s>(q_gen_1961) -> q_gen_1962
<s, s, s>(q_gen_1964) -> q_gen_1963
<s, z, s>(q_gen_1953) -> q_gen_1964
<s, s, s>(q_gen_1966) -> q_gen_1965
<s, s, s>(q_gen_1962) -> q_gen_1966
<s, s, s>(q_gen_1968) -> q_gen_1967
<s, s, s>(q_gen_1969) -> q_gen_1968
<z, z, s>(q_gen_1970) -> q_gen_1969
<s, s, s>(q_gen_1939) -> q_gen_1971
<s, s, s>(q_gen_1967) -> q_gen_1972
<s, s, s>(q_gen_1938) -> q_gen_1973
<s, s, s>(q_gen_1975) -> q_gen_1974
<s, s, s>(q_gen_1976) -> q_gen_1975
<s, s, s>(q_gen_1936) -> q_gen_1976
<s, s, s>(q_gen_1978) -> q_gen_1977
<s, s, s>(q_gen_1979) -> q_gen_1978
<s, s, s>(q_gen_1942) -> q_gen_1979
<s, z, s>(q_gen_1981) -> q_gen_1980
<z, s, s>(q_gen_1983) -> q_gen_1982
<s, s, s>(q_gen_1985) -> q_gen_1984
<s, s, s>(q_gen_1982) -> q_gen_1985
<s, s, s>(q_gen_1987) -> q_gen_1986
<s, s, s>(q_gen_1988) -> q_gen_1987
<s, s, s>(q_gen_1989) -> q_gen_1988
<z, s, s>(q_gen_1990) -> q_gen_1989
<s, z, s>(q_gen_1990) -> q_gen_1991
<s, s, s>(q_gen_1993) -> q_gen_1992
<z, z, s>(q_gen_1994) -> q_gen_1993
<z, s, s>(q_gen_1937) -> q_gen_1995
<s, s, s>(q_gen_1946) -> q_gen_1996
<s, s, s>(q_gen_1947) -> q_gen_1997
<s, s, s>(q_gen_1992) -> q_gen_1998
<s, s, s>(q_gen_2000) -> q_gen_1999
<s, z, s>(q_gen_2001) -> q_gen_2000
<s, s, s>(q_gen_2003) -> q_gen_2002
<s, s, s>(q_gen_2004) -> q_gen_2003
<s, z, s>(q_gen_2005) -> q_gen_2004
<s, s, s>(q_gen_2007) -> q_gen_2006
<s, s, s>(q_gen_2008) -> q_gen_2007
<s, s, s>(q_gen_1991) -> q_gen_2008
<s, s, s>(q_gen_2010) -> q_gen_2009
<s, s, s>(q_gen_1998) -> q_gen_2010
<s, s, s>(q_gen_2012) -> q_gen_2011
<s, s, s>(q_gen_2013) -> q_gen_2012
<s, z, s>(q_gen_1983) -> q_gen_2013
<s, s, s>(q_gen_1996) -> q_gen_2014
<s, s, s>(q_gen_1997) -> q_gen_2015
<s, s, s>(q_gen_2017) -> q_gen_2016
<s, z, s>(q_gen_2018) -> q_gen_2017
<s, s, s>(q_gen_2020) -> q_gen_2019
<s, s, s>(q_gen_2021) -> q_gen_2020
<s, s, s>(q_gen_1973) -> q_gen_2021
<s, s, s>(q_gen_2023) -> q_gen_2022
<s, s, s>(q_gen_2024) -> q_gen_2023
<s, s, s>(q_gen_1971) -> q_gen_2024
<s, s, s>(q_gen_2026) -> q_gen_2025
<s, s, s>(q_gen_2027) -> q_gen_2026
<s, s, s>(q_gen_2028) -> q_gen_2027
<s, s, s>(q_gen_2029) -> q_gen_2028
<z, s, s>(q_gen_2005) -> q_gen_2029
<s, s, s>(q_gen_2031) -> q_gen_2030
<s, s, s>(q_gen_2032) -> q_gen_2031
<s, s, s>(q_gen_2033) -> q_gen_2032
<s, s, s>(q_gen_1949) -> q_gen_2033
<s, s, s>(q_gen_2035) -> q_gen_2034
<s, s, s>(q_gen_2036) -> q_gen_2035
<s, z, s>(q_gen_2037) -> q_gen_2036
<s, s, s>(q_gen_2039) -> q_gen_2038
<s, s, s>(q_gen_1999) -> q_gen_2039
<s, s, s>(q_gen_2041) -> q_gen_2040
<s, s, s>(q_gen_1954) -> q_gen_2041
<s, s, s>(q_gen_1977) -> q_gen_2042
<s, s, s>(q_gen_2044) -> q_gen_2043
<s, s, s>(q_gen_2040) -> q_gen_2044
<s, s, s>(q_gen_2014) -> q_gen_2045
<s, s, s>(q_gen_2015) -> q_gen_2046
<s, s, s>(q_gen_2048) -> q_gen_2047
<s, s, s>(q_gen_2002) -> q_gen_2048
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007287 s (model generation: 0.007135,  model checking: 0.000152):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 3
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 1
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.007163 s (model generation: 0.007068,  model checking: 0.000095):

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

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 3
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 1
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 2, which took 0.009176 s (model generation: 0.008989,  model checking: 0.000187):

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

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 2
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 3, which took 0.007730 s (model generation: 0.007512,  model checking: 0.000218):

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

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 3
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 4, which took 0.009135 s (model generation: 0.008722,  model checking: 0.000413):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1941},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s, s>(q_gen_1933) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, s>(q_gen_1941) -> q_gen_1933
<z, z, z>() -> q_gen_1933
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 6
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 6
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 7
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> z  ;  _lh -> s(z)  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.008898 s (model generation: 0.008389,  model checking: 0.000509):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 7
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 7
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 6, which took 0.009140 s (model generation: 0.008859,  model checking: 0.000281):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s, s>(q_gen_1933) -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 7
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 10
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 10
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(z))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.010871 s (model generation: 0.010564,  model checking: 0.000307):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s, s>(q_gen_1934) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1933) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 8
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 10
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.012018 s (model generation: 0.011570,  model checking: 0.000448):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1933) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 9
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 13
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 13
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(z))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.012001 s (model generation: 0.011413,  model checking: 0.000588):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 10
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 13
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 16
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.013723 s (model generation: 0.012984,  model checking: 0.000739):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 11
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 14
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 19
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.015817 s (model generation: 0.014984,  model checking: 0.000833):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 12
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 15
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 22
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.019771 s (model generation: 0.019481,  model checking: 0.000290):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1936, q_gen_1940, q_gen_1941, q_gen_1944},
Q_f={q_gen_1933, q_gen_1936},
Delta=
{
<s>(q_gen_1941) -> q_gen_1941
<z>() -> q_gen_1941
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1936) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1936
<s, z, s>(q_gen_1935) -> q_gen_1936
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 13
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 18
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 22
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.018160 s (model generation: 0.018039,  model checking: 0.000121):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1937, q_gen_1938, q_gen_1940, q_gen_1941},
Q_f={q_gen_1933},
Delta=
{
<s>(q_gen_1941) -> q_gen_1941
<z>() -> q_gen_1941
<z, s>(q_gen_1941) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1935) -> q_gen_1937
<s, s, s>(q_gen_1938) -> q_gen_1933
<s, z, s>(q_gen_1937) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1937) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1938
<s, z, s>(q_gen_1935) -> q_gen_1938
<s, s, s>(q_gen_1933) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 16
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 18
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 22
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 14, which took 0.018415 s (model generation: 0.018111,  model checking: 0.000304):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1957},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, s>(q_gen_1957) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 17
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 21
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 22
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> z  ;  _lh -> s(s(z))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 15, which took 0.018764 s (model generation: 0.017425,  model checking: 0.001339):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 18
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 22
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 25
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(z))))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 16, which took 0.023586 s (model generation: 0.023163,  model checking: 0.000423):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1956, q_gen_1957},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1957) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 19
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 25
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 25
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(s(z)))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 17, which took 0.023979 s (model generation: 0.023276,  model checking: 0.000703):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<s, z, s>(q_gen_1961) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 20
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 25
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 28
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(z))))  ;  mm -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 18, which took 0.032425 s (model generation: 0.031909,  model checking: 0.000516):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1944) -> q_gen_1934
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 21
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 28
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 28
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(z)  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.033284 s (model generation: 0.032334,  model checking: 0.000950):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<s, s, s>(q_gen_1940) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 22
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 28
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 31
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(z))))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 20, which took 0.040253 s (model generation: 0.039550,  model checking: 0.000703):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1956, q_gen_1957},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<s>(q_gen_1957) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 23
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 31
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 31
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.043667 s (model generation: 0.042686,  model checking: 0.000981):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1956, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, z, s>(q_gen_1961) -> q_gen_1956
<z, s, s>(q_gen_1961) -> q_gen_1956
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 24
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 31
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 34
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 22, which took 0.049243 s (model generation: 0.048587,  model checking: 0.000656):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1956, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933},
Delta=
{
<s>(q_gen_1957) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1933) -> q_gen_1940
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, z, s>(q_gen_1961) -> q_gen_1956
<z, s, s>(q_gen_1961) -> q_gen_1956
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 25
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 34
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 34
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.048744 s (model generation: 0.047534,  model checking: 0.001210):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1936, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1936},
Delta=
{
<s>(q_gen_1957) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1936) -> q_gen_1936
<s, s, s>(q_gen_1940) -> q_gen_1936
<s, z, s>(q_gen_1935) -> q_gen_1936
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 26
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 37
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 35
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 24, which took 0.049833 s (model generation: 0.048497,  model checking: 0.001336):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1939},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1939) -> q_gen_1939
<s, s, s>(q_gen_1940) -> q_gen_1939
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 27
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 40
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 36
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(z)))  ;  _lh -> s(s(s(s(s(z)))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 25, which took 0.050627 s (model generation: 0.049747,  model checking: 0.000880):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1942},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, s, s>(q_gen_1942) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1943) -> q_gen_1942
<s, s, s>(q_gen_1945) -> q_gen_1943
<s, z, s>(q_gen_1944) -> q_gen_1943
<z, s, s>(q_gen_1944) -> q_gen_1943
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 28
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 40
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 39
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 26, which took 0.079968 s (model generation: 0.079072,  model checking: 0.000896):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1935
<z, z>() -> q_gen_1935
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<s, s, s>(q_gen_1946) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<z, s, s>(q_gen_1944) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 29
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 40
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 42
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 27, which took 0.086552 s (model generation: 0.086094,  model checking: 0.000458):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, s>(q_gen_1970) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 30
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 43
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 42
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> z  ;  _lh -> s(s(s(z)))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 28, which took 0.087646 s (model generation: 0.087453,  model checking: 0.000193):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1937, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<z, z>() -> q_gen_1935
<s, s>(q_gen_1935) -> q_gen_1937
<s, s>(q_gen_1944) -> q_gen_1937
<s, s>(q_gen_1937) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<s, z, s>(q_gen_1937) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<s, z, s>(q_gen_1961) -> q_gen_1940
<z, s, s>(q_gen_1937) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 33
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 43
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 42
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(s(z)))
})

-------------------------------------------
Step 29, which took 0.078846 s (model generation: 0.076389,  model checking: 0.002457):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1957},
Q_f={q_gen_1933, q_gen_1942},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1944
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1942) -> q_gen_1942
<s, s, s>(q_gen_1943) -> q_gen_1942
<s, s, s>(q_gen_1945) -> q_gen_1943
<s, z, s>(q_gen_1944) -> q_gen_1943
<z, s, s>(q_gen_1944) -> q_gen_1943
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 34
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 46
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 43
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(z)))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 30, which took 0.075446 s (model generation: 0.074008,  model checking: 0.001438):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1936, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933, q_gen_1936},
Delta=
{
<s>(q_gen_1957) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1936
<s, z, s>(q_gen_1935) -> q_gen_1936
<z, s, s>(q_gen_1961) -> q_gen_1936
<s, s, s>(q_gen_1936) -> q_gen_1940
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 35
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 46
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 46
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 31, which took 0.085965 s (model generation: 0.083814,  model checking: 0.002151):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1936, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933, q_gen_1936},
Delta=
{
<s>(q_gen_1957) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1936
<s, z, s>(q_gen_1935) -> q_gen_1936
<s, s, s>(q_gen_1936) -> q_gen_1940
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 36
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 49
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 47
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 32, which took 0.081781 s (model generation: 0.080371,  model checking: 0.001410):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 37
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 49
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 50
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(z))
})

-------------------------------------------
Step 33, which took 0.092989 s (model generation: 0.090388,  model checking: 0.002601):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 38
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 50
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 53
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 34, which took 0.121400 s (model generation: 0.119882,  model checking: 0.001518):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1949, q_gen_1957, q_gen_1961},
Q_f={q_gen_1933, q_gen_1949},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1957
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<z, s, s>(q_gen_1944) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<s, s, s>(q_gen_1946) -> q_gen_1949
<s, s, s>(q_gen_1949) -> q_gen_1949
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 39
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 53
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 53
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(s(z)))))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 35, which took 0.166825 s (model generation: 0.164750,  model checking: 0.002075):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1970) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 40
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 53
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 56
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(z))))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 36, which took 0.147804 s (model generation: 0.146892,  model checking: 0.000912):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<s>(q_gen_1970) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1970) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 41
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 56
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 56
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(s(s(z))))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 37, which took 0.156228 s (model generation: 0.154058,  model checking: 0.002170):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<s>(q_gen_1970) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1934) -> q_gen_1934
<s, s, s>(q_gen_1940) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1961) -> q_gen_1934
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 42
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 59
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 57
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 38, which took 0.143703 s (model generation: 0.143272,  model checking: 0.000431):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1937, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933},
Delta=
{
<s>(q_gen_1970) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1937) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1935) -> q_gen_1937
<z, s>(q_gen_1970) -> q_gen_1937
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<s, z, s>(q_gen_1937) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, s, s>(q_gen_1937) -> q_gen_1969
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 43
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 59
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 60
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 39, which took 0.158912 s (model generation: 0.157901,  model checking: 0.001011):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1961) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1961) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 44
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 62
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 60
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(s(z)))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 40, which took 0.170145 s (model generation: 0.169084,  model checking: 0.001061):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<s>(q_gen_1970) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1961) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 45
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 62
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 63
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(z)))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 41, which took 0.148406 s (model generation: 0.147259,  model checking: 0.001147):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1970) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 46
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 65
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 63
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(z))))  ;  _lh -> s(s(s(s(s(s(z))))))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 42, which took 0.207568 s (model generation: 0.205869,  model checking: 0.001699):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 47
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 65
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 66
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(z))))))  ;  mm -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 43, which took 0.558028 s (model generation: 0.556978,  model checking: 0.001050):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1957, q_gen_1961, q_gen_1969, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1945) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1969) -> q_gen_1945
<s, z, s>(q_gen_1961) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1961) -> q_gen_1945
<z, z, s>(q_gen_1957) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1969
<z, z, s>(q_gen_1970) -> q_gen_1969
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 48
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 68
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 66
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(s(s(z))))))  ;  _lh -> s(s(s(z)))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 44, which took 0.364597 s (model generation: 0.363174,  model checking: 0.001423):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 49
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 68
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 69
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 45, which took 0.458801 s (model generation: 0.457951,  model checking: 0.000850):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<s, z, s>(q_gen_1990) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 50
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 71
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 69
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(s(s(z))))))  ;  _lh -> s(s(s(s(s(z)))))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 46, which took 0.394682 s (model generation: 0.393694,  model checking: 0.000988):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<s, z, s>(q_gen_1990) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 51
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 71
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 72
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 47, which took 0.529693 s (model generation: 0.528554,  model checking: 0.001139):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1994},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, s>(q_gen_1994) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, z, s>(q_gen_1994) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 52
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 74
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 72
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(z)  ;  _lh -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 48, which took 0.841854 s (model generation: 0.840814,  model checking: 0.001040):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1961) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1990) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<s, z, s>(q_gen_1990) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 53
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 74
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 75
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(z))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 49, which took 0.899689 s (model generation: 0.898816,  model checking: 0.000873):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<s>(q_gen_1970) -> q_gen_1941
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1961) -> q_gen_1935
<s, s>(q_gen_1990) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, z, s>(q_gen_1935) -> q_gen_1933
<s, z, s>(q_gen_1990) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 54
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 77
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 75
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(z))  ;  _lh -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 50, which took 0.839118 s (model generation: 0.838352,  model checking: 0.000766):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1994},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1961) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1970) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1994) -> q_gen_1961
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, z, s>(q_gen_1994) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 55
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 77
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 78
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 51, which took 0.526838 s (model generation: 0.526164,  model checking: 0.000674):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990, q_gen_1994},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1994) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, s>(q_gen_1994) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 56
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 80
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 78
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> z  ;  _lh -> s(s(s(s(z))))  ;  m -> z  ;  n -> z
})

-------------------------------------------
Step 52, which took 0.643111 s (model generation: 0.641885,  model checking: 0.001226):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1983},
Q_f={q_gen_1933, q_gen_1939},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1961) -> q_gen_1983
<s, s>(q_gen_1983) -> q_gen_1983
<z, s>(q_gen_1970) -> q_gen_1983
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1939) -> q_gen_1939
<s, s, s>(q_gen_1940) -> q_gen_1939
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1983) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1983) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 57
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 80
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 81
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(z)  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 53, which took 4.080426 s (model generation: 4.079766,  model checking: 0.000660):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1939},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1990) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1939) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1939
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1961) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 58
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 83
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 81
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(z)))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 54, which took 0.821021 s (model generation: 0.819402,  model checking: 0.001619):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1939},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1939) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1939
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 59
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 83
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 84
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 55, which took 1.751513 s (model generation: 1.750251,  model checking: 0.001262):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1939, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1939},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1939) -> q_gen_1939
<s, s, s>(q_gen_1940) -> q_gen_1939
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 60
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 86
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 84
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(z))))  ;  _lh -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 56, which took 1.168475 s (model generation: 1.166627,  model checking: 0.001848):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1956, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990, q_gen_1994},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1994) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1994) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1990) -> q_gen_1946
<z, s, s>(q_gen_1990) -> q_gen_1946
<z, z, s>(q_gen_1970) -> q_gen_1946
<s, s, s>(q_gen_1946) -> q_gen_1956
<s, z, s>(q_gen_1961) -> q_gen_1956
<z, s, s>(q_gen_1961) -> q_gen_1956
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 61
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 86
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 87
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 57, which took 2.831518 s (model generation: 2.829054,  model checking: 0.002464):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1942},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1942) -> q_gen_1942
<s, s, s>(q_gen_1943) -> q_gen_1942
<s, s, s>(q_gen_1946) -> q_gen_1943
<s, z, s>(q_gen_1944) -> q_gen_1943
<z, s, s>(q_gen_1990) -> q_gen_1943
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 62
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 89
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 87
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(z)))  ;  _lh -> s(s(s(s(s(z)))))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 58, which took 1.844171 s (model generation: 1.842914,  model checking: 0.001257):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1949, q_gen_1950, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1949},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1990) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, s, s>(q_gen_1949) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, s, s>(q_gen_1950) -> q_gen_1949
<s, s, s>(q_gen_1946) -> q_gen_1950
<z, s, s>(q_gen_1944) -> q_gen_1950
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 63
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 89
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 90
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(z))))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 59, which took 2.700475 s (model generation: 2.698064,  model checking: 0.002411):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1949, q_gen_1950, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1949},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1990) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, s, s>(q_gen_1949) -> q_gen_1949
<s, s, s>(q_gen_1950) -> q_gen_1949
<s, s, s>(q_gen_1946) -> q_gen_1950
<z, s, s>(q_gen_1944) -> q_gen_1950
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 64
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 92
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 90
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(s(z)))))  ;  _lh -> s(s(s(s(z))))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 60, which took 3.615278 s (model generation: 3.613861,  model checking: 0.001417):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1954, q_gen_1955, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1954},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<s, s>(q_gen_1990) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1990) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, s, s>(q_gen_1954) -> q_gen_1954
<s, s, s>(q_gen_1955) -> q_gen_1954
<s, s, s>(q_gen_1946) -> q_gen_1955
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 65
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 92
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 93
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(z))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 61, which took 4.607345 s (model generation: 4.605477,  model checking: 0.001868):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1954, q_gen_1955, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1954},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1990) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, s, s>(q_gen_1954) -> q_gen_1954
<s, s, s>(q_gen_1955) -> q_gen_1954
<s, s, s>(q_gen_1946) -> q_gen_1955
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 66
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 95
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 93
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(z))))  ;  _lh -> s(s(s(s(s(s(z))))))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 62, which took 4.005426 s (model generation: 4.004533,  model checking: 0.000893):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1954, q_gen_1955, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1954},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, s, s>(q_gen_1954) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, s, s>(q_gen_1955) -> q_gen_1954
<s, s, s>(q_gen_1946) -> q_gen_1955
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 67
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 95
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 96
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(s(z)))))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(s(z))))))
})

-------------------------------------------
Step 63, which took 8.383405 s (model generation: 8.382413,  model checking: 0.000992):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990},
Q_f={q_gen_1933, q_gen_1942},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1970
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, s, s>(q_gen_1942) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1943) -> q_gen_1942
<s, s, s>(q_gen_1946) -> q_gen_1943
<s, z, s>(q_gen_1944) -> q_gen_1943
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 68
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 98
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 96
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(s(s(z))))))  ;  _lh -> s(s(s(s(s(s(s(z)))))))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 64, which took 4.277415 s (model generation: 4.274942,  model checking: 0.002473):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1934, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1956, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990, q_gen_1994},
Q_f={q_gen_1933, q_gen_1934},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<s, s>(q_gen_1990) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<z, s>(q_gen_1994) -> q_gen_1961
<z, s>(q_gen_1970) -> q_gen_1990
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1940) -> q_gen_1934
<s, z, s>(q_gen_1935) -> q_gen_1934
<z, s, s>(q_gen_1935) -> q_gen_1934
<s, s, s>(q_gen_1934) -> q_gen_1940
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, z, s>(q_gen_1994) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1990) -> q_gen_1946
<z, s, s>(q_gen_1990) -> q_gen_1946
<z, z, s>(q_gen_1970) -> q_gen_1946
<s, s, s>(q_gen_1946) -> q_gen_1956
<s, z, s>(q_gen_1961) -> q_gen_1956
<z, s, s>(q_gen_1961) -> q_gen_1956
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 69
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 98
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 99
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(z)))))  ;  mm -> s(s(s(s(s(z)))))  ;  n -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 65, which took 6.029442 s (model generation: 6.028373,  model checking: 0.001069):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990, q_gen_1993, q_gen_1994, q_gen_2005},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<z, s>(q_gen_1994) -> q_gen_2005
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1946) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<s, s, s>(q_gen_1993) -> q_gen_1945
<s, z, s>(q_gen_1990) -> q_gen_1945
<z, s, s>(q_gen_1990) -> q_gen_1945
<z, z, s>(q_gen_1970) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1961) -> q_gen_1946
<z, s, s>(q_gen_1961) -> q_gen_1946
<z, z, s>(q_gen_1957) -> q_gen_1946
<s, z, s>(q_gen_2005) -> q_gen_1993
<z, s, s>(q_gen_2005) -> q_gen_1993
<z, z, s>(q_gen_1994) -> q_gen_1993
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 70
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 101
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 99
}
Sat witness: Found: ((plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]), {
_kh -> s(s(s(s(z))))  ;  _lh -> s(s(s(s(s(s(s(s(z))))))))  ;  m -> s(s(s(s(z))))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 66, which took 4.718968 s (model generation: 4.715702,  model checking: 0.003266):

Model:
|_
{
plus -> 
{{{
Q={q_gen_1933, q_gen_1935, q_gen_1940, q_gen_1941, q_gen_1944, q_gen_1945, q_gen_1946, q_gen_1956, q_gen_1957, q_gen_1961, q_gen_1970, q_gen_1990, q_gen_1994, q_gen_2005},
Q_f={q_gen_1933},
Delta=
{
<z>() -> q_gen_1941
<s>(q_gen_1941) -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1970
<s>(q_gen_1970) -> q_gen_1994
<s, s>(q_gen_1935) -> q_gen_1935
<z, z>() -> q_gen_1935
<s, s>(q_gen_1944) -> q_gen_1944
<z, s>(q_gen_1941) -> q_gen_1944
<s, s>(q_gen_1961) -> q_gen_1961
<z, s>(q_gen_1957) -> q_gen_1961
<s, s>(q_gen_1990) -> q_gen_1990
<z, s>(q_gen_1970) -> q_gen_1990
<z, s>(q_gen_1994) -> q_gen_2005
<s, s, s>(q_gen_1940) -> q_gen_1933
<s, z, s>(q_gen_1935) -> q_gen_1933
<z, s, s>(q_gen_1935) -> q_gen_1933
<z, z, z>() -> q_gen_1933
<s, s, s>(q_gen_1956) -> q_gen_1940
<s, z, s>(q_gen_1944) -> q_gen_1940
<z, s, s>(q_gen_1944) -> q_gen_1940
<z, z, s>(q_gen_1941) -> q_gen_1940
<s, s, s>(q_gen_1933) -> q_gen_1945
<z, s, s>(q_gen_2005) -> q_gen_1945
<z, z, s>(q_gen_1994) -> q_gen_1945
<s, s, s>(q_gen_1945) -> q_gen_1946
<s, z, s>(q_gen_1990) -> q_gen_1946
<s, z, s>(q_gen_2005) -> q_gen_1946
<z, s, s>(q_gen_1990) -> q_gen_1946
<z, z, s>(q_gen_1970) -> q_gen_1946
<s, s, s>(q_gen_1946) -> q_gen_1956
<s, z, s>(q_gen_1961) -> q_gen_1956
<z, s, s>(q_gen_1961) -> q_gen_1956
<z, z, s>(q_gen_1957) -> q_gen_1956
}

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

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

Teacher's answer:
New clause system:
{
() -> plus([n, z, n]) -> 71
(plus([m, n, _lh]) /\ plus([n, m, _kh])) -> eq_nat([_kh, _lh]) -> 101
(plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]) -> 102
}
Sat witness: Found: ((plus([n, mm, _fh])) -> plus([n, s(mm), s(_fh)]), {
_fh -> s(s(s(s(s(s(s(s(z))))))))  ;  mm -> s(s(s(z)))  ;  n -> s(s(s(s(s(z)))))
})

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