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


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.476228 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5559, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5559},
Delta=
{
<s>(q_gen_5561) -> q_gen_5561
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5567
<z, s>(q_gen_5561) -> q_gen_5567
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5559) -> q_gen_5559
<s, z, s>(q_gen_5567) -> q_gen_5559
<z, s, s>(q_gen_5567) -> q_gen_5559
<z, z, s>(q_gen_5561) -> q_gen_5559
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010205 s (model generation: 0.009813,  model checking: 0.000392):

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

}

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

}

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010129 s (model generation: 0.010017,  model checking: 0.000112):

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

}

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

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

}
--
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: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.010465 s (model generation: 0.010210,  model checking: 0.000255):

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

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

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

}
--
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: Found: ((plus([n, mm, _rba])) -> plus([n, s(mm), s(_rba)]), {
_rba -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.013423 s (model generation: 0.010505,  model checking: 0.002918):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552},
Q_f={q_gen_5548},
Delta=
{
<z, z>() -> q_gen_5552
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

}
--
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: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.011098 s (model generation: 0.010608,  model checking: 0.000490):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552},
Q_f={q_gen_5548},
Delta=
{
<z, z>() -> q_gen_5552
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.011179 s (model generation: 0.010921,  model checking: 0.000258):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552},
Q_f={q_gen_5548},
Delta=
{
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

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

-------------------------------------------
Step 6, which took 0.011789 s (model generation: 0.011273,  model checking: 0.000516):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552},
Q_f={q_gen_5548},
Delta=
{
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

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

-------------------------------------------
Step 7, which took 0.015008 s (model generation: 0.014593,  model checking: 0.000415):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s, s>(q_gen_5548) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, s>(q_gen_5561) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

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

-------------------------------------------
Step 8, which took 0.013566 s (model generation: 0.013539,  model checking: 0.000027):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s, s>(q_gen_5548) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, s>(q_gen_5561) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

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

})

-------------------------------------------
Step 9, which took 0.013625 s (model generation: 0.013478,  model checking: 0.000147):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5564},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<s, s>(q_gen_5564) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<z, z>() -> q_gen_5564
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s, s>(q_gen_5548) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, s>(q_gen_5561) -> q_gen_5548
<z, z, z>() -> q_gen_5548
}

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

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

-------------------------------------------
Step 10, which took 0.016200 s (model generation: 0.015191,  model checking: 0.001009):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5560, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s, s>(q_gen_5560) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5548) -> q_gen_5560
<z, z, s>(q_gen_5561) -> q_gen_5560
}

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

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

-------------------------------------------
Step 11, which took 0.015957 s (model generation: 0.014770,  model checking: 0.001187):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5551, q_gen_5552, q_gen_5561, q_gen_5562},
Q_f={q_gen_5548, q_gen_5551},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5551) -> q_gen_5551
<s, z, s>(q_gen_5552) -> q_gen_5551
<z, s, s>(q_gen_5552) -> q_gen_5551
<z, z, s>(q_gen_5561) -> q_gen_5551
<s, s, s>(q_gen_5548) -> q_gen_5562
}

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

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

-------------------------------------------
Step 12, which took 0.016535 s (model generation: 0.016089,  model checking: 0.000446):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5555, q_gen_5558, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<z, s>(q_gen_5561) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s>(q_gen_5552) -> q_gen_5555
<s, z, s>(q_gen_5555) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5548) -> q_gen_5558
<s, s, s>(q_gen_5558) -> q_gen_5558
<s, z, s>(q_gen_5552) -> q_gen_5558
<z, z, s>(q_gen_5561) -> q_gen_5558
}

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

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

-------------------------------------------
Step 13, which took 0.017331 s (model generation: 0.016507,  model checking: 0.000824):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5555, q_gen_5560, q_gen_5561},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<z, z>() -> q_gen_5552
<s, s>(q_gen_5552) -> q_gen_5555
<z, s>(q_gen_5561) -> q_gen_5555
<s, s, s>(q_gen_5560) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<s, z, s>(q_gen_5555) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5548) -> q_gen_5560
<z, s, s>(q_gen_5555) -> q_gen_5560
<z, z, s>(q_gen_5561) -> q_gen_5560
}

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

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

-------------------------------------------
Step 14, which took 0.018656 s (model generation: 0.016888,  model checking: 0.001768):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5560, q_gen_5561, q_gen_5567},
Q_f={q_gen_5548},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5567
<s, s, s>(q_gen_5560) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5548) -> q_gen_5560
<z, s, s>(q_gen_5567) -> q_gen_5560
<z, z, s>(q_gen_5561) -> q_gen_5560
}

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

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

-------------------------------------------
Step 15, which took 0.018368 s (model generation: 0.017875,  model checking: 0.000493):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563, q_gen_5564},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5564) -> q_gen_5563
<z, z>() -> q_gen_5564
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5551, q_gen_5552, q_gen_5561, q_gen_5562},
Q_f={q_gen_5548, q_gen_5551},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5551) -> q_gen_5551
<s, z, s>(q_gen_5552) -> q_gen_5551
<z, s, s>(q_gen_5552) -> q_gen_5551
<z, z, s>(q_gen_5561) -> q_gen_5551
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 16, which took 0.019038 s (model generation: 0.017934,  model checking: 0.001104):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5554, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5554},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5567
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5554) -> q_gen_5554
<s, z, s>(q_gen_5552) -> q_gen_5554
<z, s, s>(q_gen_5567) -> q_gen_5554
<z, z, s>(q_gen_5561) -> q_gen_5554
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 17, which took 0.022799 s (model generation: 0.022015,  model checking: 0.000784):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5555, q_gen_5558, q_gen_5561, q_gen_5562},
Q_f={q_gen_5548, q_gen_5558},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5555) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s>(q_gen_5552) -> q_gen_5555
<z, s>(q_gen_5561) -> q_gen_5555
<s, z, s>(q_gen_5555) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5558) -> q_gen_5558
<s, z, s>(q_gen_5552) -> q_gen_5558
<z, s, s>(q_gen_5555) -> q_gen_5558
<z, z, s>(q_gen_5561) -> q_gen_5558
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 18, which took 0.025219 s (model generation: 0.023492,  model checking: 0.001727):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5554, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5554},
Delta=
{
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5567
<z, s>(q_gen_5561) -> q_gen_5567
<s, s, s>(q_gen_5554) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5554
<s, z, s>(q_gen_5567) -> q_gen_5554
<z, s, s>(q_gen_5567) -> q_gen_5554
<z, z, s>(q_gen_5561) -> q_gen_5554
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 19, which took 0.029892 s (model generation: 0.028155,  model checking: 0.001737):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5554, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5554},
Delta=
{
<s>(q_gen_5561) -> q_gen_5561
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5567
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5554) -> q_gen_5554
<s, z, s>(q_gen_5552) -> q_gen_5554
<z, s, s>(q_gen_5567) -> q_gen_5554
<z, z, s>(q_gen_5561) -> q_gen_5554
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
<s, z, s>(q_gen_5567) -> q_gen_5562
}

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

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

-------------------------------------------
Step 20, which took 0.032349 s (model generation: 0.030741,  model checking: 0.001608):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5554, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5554},
Delta=
{
<s>(q_gen_5561) -> q_gen_5561
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5567
<s, s, s>(q_gen_5554) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5554
<s, z, s>(q_gen_5567) -> q_gen_5554
<z, s, s>(q_gen_5567) -> q_gen_5554
<z, z, s>(q_gen_5561) -> q_gen_5554
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 21, which took 0.036590 s (model generation: 0.034764,  model checking: 0.001826):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5554, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548, q_gen_5554},
Delta=
{
<s>(q_gen_5561) -> q_gen_5561
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5552
<z, z>() -> q_gen_5552
<z, s>(q_gen_5561) -> q_gen_5567
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, s, s>(q_gen_5554) -> q_gen_5554
<s, z, s>(q_gen_5552) -> q_gen_5554
<s, z, s>(q_gen_5567) -> q_gen_5554
<z, s, s>(q_gen_5567) -> q_gen_5554
<z, z, s>(q_gen_5561) -> q_gen_5554
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

-------------------------------------------
Step 22, which took 0.041501 s (model generation: 0.039797,  model checking: 0.001704):

Model:
|_
{
le -> 
{{{
Q={q_gen_5549, q_gen_5550, q_gen_5563},
Q_f={q_gen_5549},
Delta=
{
<s>(q_gen_5550) -> q_gen_5550
<z>() -> q_gen_5550
<s, s>(q_gen_5549) -> q_gen_5549
<z, s>(q_gen_5550) -> q_gen_5549
<s, s>(q_gen_5563) -> q_gen_5563
<z, z>() -> q_gen_5563
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_5548, q_gen_5552, q_gen_5560, q_gen_5561, q_gen_5562, q_gen_5567},
Q_f={q_gen_5548},
Delta=
{
<s>(q_gen_5561) -> q_gen_5561
<z>() -> q_gen_5561
<s, s>(q_gen_5552) -> q_gen_5552
<z, z>() -> q_gen_5552
<s, s>(q_gen_5567) -> q_gen_5567
<z, s>(q_gen_5561) -> q_gen_5567
<s, s, s>(q_gen_5560) -> q_gen_5548
<s, z, s>(q_gen_5552) -> q_gen_5548
<z, s, s>(q_gen_5552) -> q_gen_5548
<z, z, z>() -> q_gen_5548
<s, z, s>(q_gen_5567) -> q_gen_5560
<z, s, s>(q_gen_5567) -> q_gen_5560
<z, z, s>(q_gen_5561) -> q_gen_5560
<s, s, s>(q_gen_5548) -> q_gen_5562
<s, s, s>(q_gen_5562) -> q_gen_5562
}

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

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

Total time: 0.476228
Reason for stopping: Proved