Solving ../../benchmarks/true/plus_succ1_le.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)])}
(plus([_sba, _tba, _uba]) /\ plus([_sba, _tba, _vba])) -> eq_nat([_uba, _vba])
)
(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, _wba])) -> le([m, _wba])}


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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 0  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 0
}


Solving took 0.200708 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5063},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<s>(q_gen_5055) -> q_gen_5055
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<s, s>(q_gen_5063) -> q_gen_5063
<z, s>(q_gen_5055) -> q_gen_5063
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5063) -> q_gen_5050
<z, s, s>(q_gen_5063) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009027 s (model generation: 0.008701,  model checking: 0.000326):

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}
--
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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 1  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.009743 s (model generation: 0.009618,  model checking: 0.000125):

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

}

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

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

}
--
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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 1  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 1
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.012012 s (model generation: 0.011577,  model checking: 0.000435):

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

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

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

}
--
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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 4  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 2
}
Sat witness: Yes: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.012359 s (model generation: 0.012084,  model checking: 0.000275):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048},
Q_f={q_gen_5044},
Delta=
{
<z, z>() -> q_gen_5048
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

}
--
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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 4  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 2
}
Sat witness: Yes: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.013043 s (model generation: 0.011742,  model checking: 0.001301):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048},
Q_f={q_gen_5044},
Delta=
{
<z, z>() -> q_gen_5048
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

}
--
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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 4  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 3
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 5, which took 0.013259 s (model generation: 0.012746,  model checking: 0.000513):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048},
Q_f={q_gen_5044},
Delta=
{
<z, z>() -> q_gen_5048
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 4  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 4
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 6, which took 0.007539 s (model generation: 0.007302,  model checking: 0.000237):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048},
Q_f={q_gen_5044},
Delta=
{
<z, z>() -> q_gen_5048
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 7  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 5
}
Sat witness: Yes: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.007097 s (model generation: 0.006931,  model checking: 0.000166):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5055},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5044) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, s>(q_gen_5055) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 7  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 8
}
Sat witness: Yes: ((plus([s(n), m, _wba])) -> le([m, _wba]), {
_wba -> s(z)  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.004631 s (model generation: 0.004620,  model checking: 0.000011):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5055},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5044) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, s>(q_gen_5055) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 7  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 8
}
Sat witness: Yes: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 9, which took 0.004353 s (model generation: 0.004303,  model checking: 0.000050):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5058},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<s, s>(q_gen_5058) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<z, z>() -> q_gen_5058
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5055},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5044) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, s>(q_gen_5055) -> q_gen_5044
<z, z, z>() -> q_gen_5044
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 7  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 8
}
Sat witness: Yes: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.004479 s (model generation: 0.004132,  model checking: 0.000347):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5054, q_gen_5055},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5054) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5044) -> q_gen_5054
<z, z, s>(q_gen_5055) -> q_gen_5054
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (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, _rba])) -> plus([n, s(mm), s(_rba)]) -> 7  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 8
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 11, which took 0.004645 s (model generation: 0.004359,  model checking: 0.000286):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5054, q_gen_5055},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5054) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5044) -> q_gen_5054
<z, z, s>(q_gen_5055) -> q_gen_5054
}

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

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

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

-------------------------------------------
Step 12, which took 0.005182 s (model generation: 0.005047,  model checking: 0.000135):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5047, q_gen_5048, q_gen_5055, q_gen_5056},
Q_f={q_gen_5044, q_gen_5047},
Delta=
{
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5048
<z, z>() -> q_gen_5048
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5047) -> q_gen_5047
<s, z, s>(q_gen_5048) -> q_gen_5047
<z, s, s>(q_gen_5048) -> q_gen_5047
<z, z, s>(q_gen_5055) -> q_gen_5047
<s, s, s>(q_gen_5044) -> q_gen_5056
}

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

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

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

-------------------------------------------
Step 13, which took 0.006251 s (model generation: 0.005704,  model checking: 0.000547):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5054, q_gen_5055, q_gen_5063},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5063
<s, s, s>(q_gen_5054) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5044) -> q_gen_5054
<z, s, s>(q_gen_5063) -> q_gen_5054
<z, z, s>(q_gen_5055) -> q_gen_5054
}

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

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

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

-------------------------------------------
Step 14, which took 0.007695 s (model generation: 0.007304,  model checking: 0.000391):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5054, q_gen_5055, q_gen_5063},
Q_f={q_gen_5044},
Delta=
{
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5063
<s, s, s>(q_gen_5054) -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5044) -> q_gen_5054
<s, z, s>(q_gen_5063) -> q_gen_5054
<z, s, s>(q_gen_5063) -> q_gen_5054
<z, z, s>(q_gen_5055) -> q_gen_5054
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10  ;  (le([s(nn1), z])) -> BOT -> 10  ;  (le([z, z])) -> BOT -> 10  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 13  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 14
}
Sat witness: Yes: ((plus([s(n), m, _wba])) -> le([m, _wba]), {
_wba -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.007122 s (model generation: 0.007024,  model checking: 0.000098):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057, q_gen_5058},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5058) -> q_gen_5057
<z, z>() -> q_gen_5058
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5047, q_gen_5048, q_gen_5055, q_gen_5056},
Q_f={q_gen_5044, q_gen_5047},
Delta=
{
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5048
<z, z>() -> q_gen_5048
<s, s, s>(q_gen_5056) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5047) -> q_gen_5047
<s, z, s>(q_gen_5048) -> q_gen_5047
<z, s, s>(q_gen_5048) -> q_gen_5047
<z, z, s>(q_gen_5055) -> q_gen_5047
<s, s, s>(q_gen_5044) -> q_gen_5056
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 11  ;  (le([z, z])) -> BOT -> 11  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 13  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 14
}
Sat witness: Yes: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> s(z)
})

-------------------------------------------
Step 16, which took 0.007135 s (model generation: 0.006333,  model checking: 0.000802):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5060},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s>(q_gen_5048) -> q_gen_5060
<z, s>(q_gen_5055) -> q_gen_5060
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5060) -> q_gen_5050
<z, s, s>(q_gen_5060) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

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

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

-------------------------------------------
Step 17, which took 0.008621 s (model generation: 0.007956,  model checking: 0.000665):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5060},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s>(q_gen_5048) -> q_gen_5060
<s, s>(q_gen_5060) -> q_gen_5060
<z, s>(q_gen_5055) -> q_gen_5060
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5060) -> q_gen_5050
<z, s, s>(q_gen_5060) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

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

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

-------------------------------------------
Step 18, which took 0.009830 s (model generation: 0.009383,  model checking: 0.000447):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5060},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<s>(q_gen_5055) -> q_gen_5055
<z>() -> q_gen_5055
<z, z>() -> q_gen_5048
<s, s>(q_gen_5048) -> q_gen_5060
<s, s>(q_gen_5060) -> q_gen_5060
<z, s>(q_gen_5055) -> q_gen_5060
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5060) -> q_gen_5050
<z, s, s>(q_gen_5060) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

}
--
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]) -> 14  ;  (le([s(nn1), z])) -> BOT -> 14  ;  (le([z, z])) -> BOT -> 14  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 16  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 17
}
Sat witness: Yes: ((plus([s(n), m, _wba])) -> le([m, _wba]), {
_wba -> s(s(s(z)))  ;  m -> s(s(s(z)))  ;  n -> z
})

-------------------------------------------
Step 19, which took 0.009869 s (model generation: 0.009244,  model checking: 0.000625):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5063},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<s>(q_gen_5055) -> q_gen_5055
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5063
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5063) -> q_gen_5050
<z, s, s>(q_gen_5063) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

}
--
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]) -> 15  ;  (le([s(nn1), z])) -> BOT -> 15  ;  (le([z, z])) -> BOT -> 15  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 19  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 17
}
Sat witness: Yes: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.010420 s (model generation: 0.009730,  model checking: 0.000690):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5063},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<s>(q_gen_5055) -> q_gen_5055
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<s, s>(q_gen_5063) -> q_gen_5048
<z, z>() -> q_gen_5048
<z, s>(q_gen_5055) -> q_gen_5063
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, s, s>(q_gen_5050) -> q_gen_5050
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5063) -> q_gen_5050
<z, s, s>(q_gen_5063) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

}
--
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]) -> 16  ;  (le([s(nn1), z])) -> BOT -> 16  ;  (le([z, z])) -> BOT -> 16  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 22  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 18
}
Sat witness: Yes: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 21, which took 0.010674 s (model generation: 0.009900,  model checking: 0.000774):

Model:
|_
{
le -> 
{{{
Q={q_gen_5045, q_gen_5046, q_gen_5057},
Q_f={q_gen_5045},
Delta=
{
<s>(q_gen_5046) -> q_gen_5046
<z>() -> q_gen_5046
<s, s>(q_gen_5045) -> q_gen_5045
<z, s>(q_gen_5046) -> q_gen_5045
<s, s>(q_gen_5057) -> q_gen_5057
<z, z>() -> q_gen_5057
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_5044, q_gen_5048, q_gen_5050, q_gen_5055, q_gen_5056, q_gen_5063},
Q_f={q_gen_5044, q_gen_5050},
Delta=
{
<s>(q_gen_5055) -> q_gen_5055
<z>() -> q_gen_5055
<s, s>(q_gen_5048) -> q_gen_5048
<z, z>() -> q_gen_5048
<s, s>(q_gen_5063) -> q_gen_5063
<z, s>(q_gen_5055) -> q_gen_5063
<s, s, s>(q_gen_5050) -> q_gen_5044
<z, s, s>(q_gen_5048) -> q_gen_5044
<z, z, z>() -> q_gen_5044
<s, z, s>(q_gen_5048) -> q_gen_5050
<s, z, s>(q_gen_5063) -> q_gen_5050
<z, s, s>(q_gen_5063) -> q_gen_5050
<z, z, s>(q_gen_5055) -> q_gen_5050
<s, s, s>(q_gen_5044) -> q_gen_5056
<s, s, s>(q_gen_5056) -> q_gen_5056
}

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

}
--
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]) -> 17  ;  (le([s(nn1), z])) -> BOT -> 17  ;  (le([z, z])) -> BOT -> 17  ;  (plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]) -> 25  ;  (plus([s(n), m, _wba])) -> le([m, _wba]) -> 19
}
Sat witness: Yes: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

Total time: 0.200708
Reason for stopping: Proved