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, _xr])) -> plus([n, s(mm), s(_xr)])}
(plus([_yr, _zr, _as]) /\ plus([_yr, _zr, _bs])) -> eq_nat([_as, _bs])
)
(le, P:
{() -> le([z, s(nn2)])
(le([nn1, nn2])) -> le([s(nn1), s(nn2)])
(le([s(nn1), s(nn2)])) -> le([nn1, nn2])
(le([s(nn1), z])) -> BOT
(le([z, z])) -> BOT}
)
}

properties:
{(plus([s(n), m, _cs])) -> le([m, _cs])}


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

Clause system for inference is:

{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 0
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0
(le([s(nn1), z])) -> BOT -> 0
(le([z, z])) -> BOT -> 0
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 0
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 0
}


Solving took 0.374021 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4854, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4854},
Delta=
{
<s>(q_gen_4856) -> q_gen_4856
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4862
<z, s>(q_gen_4856) -> q_gen_4862
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4854) -> q_gen_4854
<s, z, s>(q_gen_4862) -> q_gen_4854
<z, s, s>(q_gen_4862) -> q_gen_4854
<z, z, s>(q_gen_4856) -> q_gen_4854
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011496 s (model generation: 0.010628,  model checking: 0.000868):

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

}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  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:
{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 1
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.008819 s (model generation: 0.008757,  model checking: 0.000062):

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

}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843},
Q_f={q_gen_4843},
Delta=
{
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 1
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 1
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.008570 s (model generation: 0.008439,  model checking: 0.000131):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<z>() -> q_gen_4845
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843},
Q_f={q_gen_4843},
Delta=
{
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 4
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 2
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.008448 s (model generation: 0.008327,  model checking: 0.000121):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<z>() -> q_gen_4845
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847},
Q_f={q_gen_4843},
Delta=
{
<z, z>() -> q_gen_4847
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2
(le([s(nn1), z])) -> BOT -> 2
(le([z, z])) -> BOT -> 2
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 4
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 2
}
Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.012100 s (model generation: 0.010508,  model checking: 0.001592):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847},
Q_f={q_gen_4843},
Delta=
{
<z, z>() -> q_gen_4847
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 4
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 3
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.008719 s (model generation: 0.008628,  model checking: 0.000091):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847},
Q_f={q_gen_4843},
Delta=
{
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 4
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 6
}
Sat witness: Found: ((plus([s(n), m, _cs])) -> le([m, _cs]), {
_cs -> s(s(z))  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 6, which took 0.009455 s (model generation: 0.009166,  model checking: 0.000289):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847},
Q_f={q_gen_4843},
Delta=
{
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 4
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 4
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 7
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 6
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.010389 s (model generation: 0.010173,  model checking: 0.000216):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s, s>(q_gen_4843) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, s>(q_gen_4856) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 5
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 7
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 9
}
Sat witness: Found: ((plus([s(n), m, _cs])) -> le([m, _cs]), {
_cs -> s(z)  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.012081 s (model generation: 0.012063,  model checking: 0.000018):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<z, z>() -> q_gen_4844
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s, s>(q_gen_4843) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, s>(q_gen_4856) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 8
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 7
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 9
}
Sat witness: Found: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 9, which took 0.010828 s (model generation: 0.010754,  model checking: 0.000074):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4859},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<s, s>(q_gen_4859) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<z, z>() -> q_gen_4859
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s, s>(q_gen_4843) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, s>(q_gen_4856) -> q_gen_4843
<z, z, z>() -> q_gen_4843
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 6
(le([z, z])) -> BOT -> 8
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 7
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 9
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.013284 s (model generation: 0.011895,  model checking: 0.001389):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4855, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s, s>(q_gen_4855) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4843) -> q_gen_4855
<z, z, s>(q_gen_4856) -> q_gen_4855
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6
() -> plus([n, z, n]) -> 7
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 7
(le([z, z])) -> BOT -> 8
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 10
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 9
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.012374 s (model generation: 0.011970,  model checking: 0.000404):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4846, q_gen_4847, q_gen_4856, q_gen_4857},
Q_f={q_gen_4843, q_gen_4846},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4846) -> q_gen_4846
<s, z, s>(q_gen_4847) -> q_gen_4846
<z, s, s>(q_gen_4847) -> q_gen_4846
<z, z, s>(q_gen_4856) -> q_gen_4846
<s, s, s>(q_gen_4843) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 7
() -> plus([n, z, n]) -> 8
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9
(le([s(nn1), z])) -> BOT -> 8
(le([z, z])) -> BOT -> 9
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 10
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 12
}
Sat witness: Found: ((plus([s(n), m, _cs])) -> le([m, _cs]), {
_cs -> s(s(z))  ;  m -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.014160 s (model generation: 0.013925,  model checking: 0.000235):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4850, q_gen_4853, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<z, s>(q_gen_4856) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s>(q_gen_4847) -> q_gen_4850
<s, z, s>(q_gen_4850) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4843) -> q_gen_4853
<s, s, s>(q_gen_4853) -> q_gen_4853
<s, z, s>(q_gen_4847) -> q_gen_4853
<z, z, s>(q_gen_4856) -> q_gen_4853
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 8
() -> plus([n, z, n]) -> 11
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9
(le([s(nn1), z])) -> BOT -> 9
(le([z, z])) -> BOT -> 9
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 10
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 12
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 13, which took 0.016175 s (model generation: 0.014434,  model checking: 0.001741):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4850, q_gen_4855, q_gen_4856},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<z, z>() -> q_gen_4847
<s, s>(q_gen_4847) -> q_gen_4850
<z, s>(q_gen_4856) -> q_gen_4850
<s, s, s>(q_gen_4855) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<s, z, s>(q_gen_4850) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4843) -> q_gen_4855
<z, s, s>(q_gen_4850) -> q_gen_4855
<z, z, s>(q_gen_4856) -> q_gen_4855
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 9
() -> plus([n, z, n]) -> 11
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10
(le([s(nn1), z])) -> BOT -> 10
(le([z, z])) -> BOT -> 10
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 13
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 12
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 14, which took 0.015178 s (model generation: 0.014755,  model checking: 0.000423):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4855, q_gen_4856, q_gen_4862},
Q_f={q_gen_4843},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4862
<s, s, s>(q_gen_4855) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4843) -> q_gen_4855
<z, s, s>(q_gen_4862) -> q_gen_4855
<z, z, s>(q_gen_4856) -> q_gen_4855
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10
() -> plus([n, z, n]) -> 12
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11
(le([s(nn1), z])) -> BOT -> 11
(le([z, z])) -> BOT -> 11
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 13
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 15
}
Sat witness: Found: ((plus([s(n), m, _cs])) -> le([m, _cs]), {
_cs -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.014166 s (model generation: 0.013884,  model checking: 0.000282):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858, q_gen_4859},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4859) -> q_gen_4858
<z, z>() -> q_gen_4859
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4846, q_gen_4847, q_gen_4856, q_gen_4857},
Q_f={q_gen_4843, q_gen_4846},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4846) -> q_gen_4846
<s, z, s>(q_gen_4847) -> q_gen_4846
<z, s, s>(q_gen_4847) -> q_gen_4846
<z, z, s>(q_gen_4856) -> q_gen_4846
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 11
() -> plus([n, z, n]) -> 12
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 14
(le([s(nn1), z])) -> BOT -> 12
(le([z, z])) -> BOT -> 12
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 13
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 15
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> s(z)
})

-------------------------------------------
Step 16, which took 0.014783 s (model generation: 0.013595,  model checking: 0.001188):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4849, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4849},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4862
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4849) -> q_gen_4849
<s, z, s>(q_gen_4847) -> q_gen_4849
<z, s, s>(q_gen_4862) -> q_gen_4849
<z, z, s>(q_gen_4856) -> q_gen_4849
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 12
() -> plus([n, z, n]) -> 13
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 14
(le([s(nn1), z])) -> BOT -> 13
(le([z, z])) -> BOT -> 13
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 16
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 15
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 17, which took 0.016339 s (model generation: 0.015635,  model checking: 0.000704):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4850, q_gen_4853, q_gen_4856, q_gen_4857},
Q_f={q_gen_4843, q_gen_4853},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4850) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s>(q_gen_4847) -> q_gen_4850
<z, s>(q_gen_4856) -> q_gen_4850
<s, z, s>(q_gen_4850) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4853) -> q_gen_4853
<s, z, s>(q_gen_4847) -> q_gen_4853
<z, s, s>(q_gen_4850) -> q_gen_4853
<z, z, s>(q_gen_4856) -> q_gen_4853
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 13
() -> plus([n, z, n]) -> 14
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15
(le([s(nn1), z])) -> BOT -> 14
(le([z, z])) -> BOT -> 14
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 16
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 18
}
Sat witness: Found: ((plus([s(n), m, _cs])) -> le([m, _cs]), {
_cs -> s(s(s(z)))  ;  m -> s(s(s(z)))  ;  n -> z
})

-------------------------------------------
Step 18, which took 0.018733 s (model generation: 0.017793,  model checking: 0.000940):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4849, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4849},
Delta=
{
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4862
<z, s>(q_gen_4856) -> q_gen_4862
<s, s, s>(q_gen_4849) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4849
<s, z, s>(q_gen_4862) -> q_gen_4849
<z, s, s>(q_gen_4862) -> q_gen_4849
<z, z, s>(q_gen_4856) -> q_gen_4849
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 14
() -> plus([n, z, n]) -> 15
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 14
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16
(le([s(nn1), z])) -> BOT -> 15
(le([z, z])) -> BOT -> 15
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 19
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 18
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 19, which took 0.021062 s (model generation: 0.020454,  model checking: 0.000608):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4849, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4849},
Delta=
{
<s>(q_gen_4856) -> q_gen_4856
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4862
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4849) -> q_gen_4849
<s, z, s>(q_gen_4847) -> q_gen_4849
<z, s, s>(q_gen_4862) -> q_gen_4849
<z, z, s>(q_gen_4856) -> q_gen_4849
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
<s, z, s>(q_gen_4862) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 15
() -> plus([n, z, n]) -> 16
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 15
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 17
(le([s(nn1), z])) -> BOT -> 16
(le([z, z])) -> BOT -> 16
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 22
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 19
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 20, which took 0.023710 s (model generation: 0.022569,  model checking: 0.001141):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4849, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4849},
Delta=
{
<s>(q_gen_4856) -> q_gen_4856
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4862
<s, s, s>(q_gen_4849) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4849
<s, z, s>(q_gen_4862) -> q_gen_4849
<z, s, s>(q_gen_4862) -> q_gen_4849
<z, z, s>(q_gen_4856) -> q_gen_4849
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 16
() -> plus([n, z, n]) -> 17
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 16
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 18
(le([s(nn1), z])) -> BOT -> 17
(le([z, z])) -> BOT -> 17
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 25
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 20
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.029768 s (model generation: 0.028823,  model checking: 0.000945):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4849, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843, q_gen_4849},
Delta=
{
<s>(q_gen_4856) -> q_gen_4856
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4847
<z, z>() -> q_gen_4847
<z, s>(q_gen_4856) -> q_gen_4862
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, s, s>(q_gen_4849) -> q_gen_4849
<s, z, s>(q_gen_4847) -> q_gen_4849
<s, z, s>(q_gen_4862) -> q_gen_4849
<z, s, s>(q_gen_4862) -> q_gen_4849
<z, z, s>(q_gen_4856) -> q_gen_4849
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 17
() -> plus([n, z, n]) -> 18
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 17
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 19
(le([s(nn1), z])) -> BOT -> 18
(le([z, z])) -> BOT -> 18
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 28
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 21
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.030178 s (model generation: 0.029141,  model checking: 0.001037):

Model:
|_
{
le -> 
{{{
Q={q_gen_4844, q_gen_4845, q_gen_4858},
Q_f={q_gen_4844},
Delta=
{
<s>(q_gen_4845) -> q_gen_4845
<z>() -> q_gen_4845
<s, s>(q_gen_4844) -> q_gen_4844
<z, s>(q_gen_4845) -> q_gen_4844
<s, s>(q_gen_4858) -> q_gen_4858
<z, z>() -> q_gen_4858
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_4843, q_gen_4847, q_gen_4855, q_gen_4856, q_gen_4857, q_gen_4862},
Q_f={q_gen_4843},
Delta=
{
<s>(q_gen_4856) -> q_gen_4856
<z>() -> q_gen_4856
<s, s>(q_gen_4847) -> q_gen_4847
<z, z>() -> q_gen_4847
<s, s>(q_gen_4862) -> q_gen_4862
<z, s>(q_gen_4856) -> q_gen_4862
<s, s, s>(q_gen_4855) -> q_gen_4843
<s, z, s>(q_gen_4847) -> q_gen_4843
<z, s, s>(q_gen_4847) -> q_gen_4843
<z, z, z>() -> q_gen_4843
<s, z, s>(q_gen_4862) -> q_gen_4855
<z, s, s>(q_gen_4862) -> q_gen_4855
<z, z, s>(q_gen_4856) -> q_gen_4855
<s, s, s>(q_gen_4843) -> q_gen_4857
<s, s, s>(q_gen_4857) -> q_gen_4857
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 18
() -> plus([n, z, n]) -> 19
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 18
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 20
(le([s(nn1), z])) -> BOT -> 19
(le([z, z])) -> BOT -> 19
(plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]) -> 31
(plus([s(n), m, _cs])) -> le([m, _cs]) -> 22
}
Sat witness: Found: ((plus([n, mm, _xr])) -> plus([n, s(mm), s(_xr)]), {
_xr -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

Total time: 0.374021
Reason for stopping: Proved