Solving ../../benchmarks/true/mult_leq_succ.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, _xp])) -> plus([n, s(mm), s(_xp)])}
(plus([_yp, _zp, _aq]) /\ plus([_yp, _zp, _bq])) -> eq_nat([_aq, _bq])
)
(mult, F:
{() -> mult([n, z, z])
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq])}
(mult([_eq, _fq, _gq]) /\ mult([_eq, _fq, _hq])) -> eq_nat([_gq, _hq])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
}

properties:
{(mult([n, s(m), _iq])) -> leq([n, _iq])}


over-approximation: {mult, plus}
under-approximation: {leq}

Clause system for inference is:

{
() -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 0  ;  () -> mult([n, z, z]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0  ;  (leq([s(nn1), z])) -> BOT -> 0  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 0  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 0  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 0
}


Solving took 0.584657 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4681},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, s>(q_gen_4662) -> q_gen_4662
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, s>(q_gen_4681) -> q_gen_4681
<s, z>(q_gen_4652) -> q_gen_4681
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4681) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, s>(q_gen_4681) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003756 s (model generation: 0.003319,  model checking: 0.000437):

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

}

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

}

Datatype: <nat, 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:
{
() -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 0  ;  () -> mult([n, z, z]) -> 0  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 1  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 1  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003703 s (model generation: 0.003636,  model checking: 0.000067):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 0  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 1  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 1  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 1
}
Sat witness: Yes: (() -> mult([n, z, z]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.005321 s (model generation: 0.005272,  model checking: 0.000049):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 1  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 1  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 1
}
Sat witness: Yes: (() -> leq([z, z]), {

})

-------------------------------------------
Step 3, which took 0.007448 s (model generation: 0.007302,  model checking: 0.000146):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 1  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 1  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 1
}
Sat witness: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 4, which took 0.009100 s (model generation: 0.008904,  model checking: 0.000196):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 1  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 1  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.009729 s (model generation: 0.009425,  model checking: 0.000304):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 2  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.014855 s (model generation: 0.014556,  model checking: 0.000299):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 2  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.012280 s (model generation: 0.011638,  model checking: 0.000642):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 3  ;  () -> plus([n, z, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3  ;  (leq([s(nn1), z])) -> BOT -> 3  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 3  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 8, which took 0.014020 s (model generation: 0.011713,  model checking: 0.002307):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  () -> mult([n, z, z]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 4  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: (() -> mult([n, z, z]), {
n -> s(z)
})

-------------------------------------------
Step 9, which took 0.011952 s (model generation: 0.011747,  model checking: 0.000205):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  () -> mult([n, z, z]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 4  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 4
}
Sat witness: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 10, which took 0.012464 s (model generation: 0.012162,  model checking: 0.000302):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  () -> mult([n, z, z]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 4  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 4  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.014448 s (model generation: 0.012307,  model checking: 0.002141):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  () -> mult([n, z, z]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 7  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 5  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 7
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.013645 s (model generation: 0.012984,  model checking: 0.000661):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 5  ;  () -> mult([n, z, z]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 5  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 7  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 6  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.015274 s (model generation: 0.014723,  model checking: 0.000551):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 6  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6  ;  (leq([s(nn1), z])) -> BOT -> 6  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 7  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 7  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 7
}
Sat witness: Yes: (() -> mult([n, z, z]), {
n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.014933 s (model generation: 0.013713,  model checking: 0.001220):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 7  ;  () -> leq([z, z]) -> 7  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7  ;  (leq([s(nn1), z])) -> BOT -> 7  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 7  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 7  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 15, which took 0.014985 s (model generation: 0.014413,  model checking: 0.000572):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 7  ;  () -> leq([z, z]) -> 7  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7  ;  (leq([s(nn1), z])) -> BOT -> 7  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 8  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 16, which took 0.017609 s (model generation: 0.017136,  model checking: 0.000473):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8  ;  (leq([s(nn1), z])) -> BOT -> 8  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 11  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Yes: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(z)  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 17, which took 0.015794 s (model generation: 0.015758,  model checking: 0.000036):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<s, z>(q_gen_4648) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 11  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Yes: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 18, which took 0.015071 s (model generation: 0.014889,  model checking: 0.000182):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4674},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<s, s>(q_gen_4674) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, z>(q_gen_4648) -> q_gen_4674
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  () -> mult([n, z, z]) -> 9  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 11  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 19, which took 0.019399 s (model generation: 0.017203,  model checking: 0.002196):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662, q_gen_4671},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4671) -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4671
<z, z, s>(q_gen_4652) -> q_gen_4671
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 9  ;  () -> leq([z, z]) -> 9  ;  () -> mult([n, z, z]) -> 10  ;  () -> plus([n, z, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 11  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 20, which took 0.019333 s (model generation: 0.018170,  model checking: 0.001163):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4662, q_gen_4671},
Q_f={q_gen_4645},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4671) -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4671
<z, z, s>(q_gen_4652) -> q_gen_4671
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 10  ;  () -> leq([z, z]) -> 10  ;  () -> mult([n, z, z]) -> 10  ;  () -> plus([n, z, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 13  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 11  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 21, which took 0.020945 s (model generation: 0.018933,  model checking: 0.002012):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<z, s, s>(q_gen_4662) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 11  ;  () -> leq([z, z]) -> 11  ;  () -> mult([n, z, z]) -> 11  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12  ;  (leq([s(nn1), z])) -> BOT -> 12  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 16  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 12  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 14
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(z)  ;  _dq -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.021213 s (model generation: 0.019614,  model checking: 0.001599):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4651, q_gen_4652, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4651},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4645) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4651
<z, s, z>(q_gen_4652) -> q_gen_4651
<s, s, s>(q_gen_4651) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 12  ;  () -> leq([z, z]) -> 12  ;  () -> mult([n, z, z]) -> 12  ;  () -> plus([n, z, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 19  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 13  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 15
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 23, which took 0.019898 s (model generation: 0.019124,  model checking: 0.000774):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4651, q_gen_4652, q_gen_4662, q_gen_4671},
Q_f={q_gen_4645, q_gen_4651},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4671) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4651
<s, z, z>(q_gen_4652) -> q_gen_4651
<z, s, z>(q_gen_4652) -> q_gen_4651
<s, s, s>(q_gen_4651) -> q_gen_4671
<z, z, s>(q_gen_4652) -> q_gen_4671
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 13  ;  () -> leq([z, z]) -> 13  ;  () -> mult([n, z, z]) -> 13  ;  () -> plus([n, z, n]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 19  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 16  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 15
}
Sat witness: Yes: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 24, which took 0.020278 s (model generation: 0.018717,  model checking: 0.001561):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4651, q_gen_4652, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4651},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4651
<s, s, s>(q_gen_4672) -> q_gen_4651
<s, z, z>(q_gen_4652) -> q_gen_4651
<z, s, z>(q_gen_4652) -> q_gen_4651
<s, s, s>(q_gen_4651) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 14  ;  () -> leq([z, z]) -> 14  ;  () -> mult([n, z, z]) -> 14  ;  () -> plus([n, z, n]) -> 14  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14  ;  (leq([s(nn1), z])) -> BOT -> 14  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 19  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 19  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 16
}
Sat witness: Yes: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 25, which took 0.023725 s (model generation: 0.022338,  model checking: 0.001387):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4651, q_gen_4652, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4651},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4651
<s, z, z>(q_gen_4652) -> q_gen_4651
<z, s, z>(q_gen_4652) -> q_gen_4651
<s, s, s>(q_gen_4651) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 15  ;  () -> leq([z, z]) -> 15  ;  () -> mult([n, z, z]) -> 15  ;  () -> plus([n, z, n]) -> 15  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15  ;  (leq([s(nn1), z])) -> BOT -> 15  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 22  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 20  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 17
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(z)  ;  _dq -> s(z)  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 26, which took 0.024846 s (model generation: 0.023850,  model checking: 0.000996):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 16  ;  () -> leq([z, z]) -> 16  ;  () -> mult([n, z, z]) -> 16  ;  () -> plus([n, z, n]) -> 16  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16  ;  (leq([s(nn1), z])) -> BOT -> 16  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 25  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 21  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 18
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 27, which took 0.025197 s (model generation: 0.024301,  model checking: 0.000896):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 17  ;  () -> leq([z, z]) -> 17  ;  () -> mult([n, z, z]) -> 17  ;  () -> plus([n, z, n]) -> 17  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17  ;  (leq([s(nn1), z])) -> BOT -> 17  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 25  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 24  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 19
}
Sat witness: Yes: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(z))  ;  m -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 28, which took 0.025088 s (model generation: 0.024685,  model checking: 0.000403):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673, q_gen_4674},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4674) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4674
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4671},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, s, s>(q_gen_4671) -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4671
<z, z, s>(q_gen_4652) -> q_gen_4671
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 17  ;  () -> leq([z, z]) -> 17  ;  () -> mult([n, z, z]) -> 17  ;  () -> plus([n, z, n]) -> 17  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20  ;  (leq([s(nn1), z])) -> BOT -> 18  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 25  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 24  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 19
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 29, which took 0.020098 s (model generation: 0.019224,  model checking: 0.000874):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4681},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, z>(q_gen_4652) -> q_gen_4681
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<z, s, s>(q_gen_4681) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
<s, z, s>(q_gen_4681) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 18  ;  () -> leq([z, z]) -> 18  ;  () -> mult([n, z, z]) -> 18  ;  () -> plus([n, z, n]) -> 18  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21  ;  (leq([s(nn1), z])) -> BOT -> 19  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 28  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 25  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 20
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(z)  ;  _dq -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 30, which took 0.021247 s (model generation: 0.020163,  model checking: 0.001084):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4692},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, z>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<z, s>(q_gen_4652) -> q_gen_4692
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, s>(q_gen_4692) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 19  ;  () -> leq([z, z]) -> 19  ;  () -> mult([n, z, z]) -> 19  ;  () -> plus([n, z, n]) -> 19  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22  ;  (leq([s(nn1), z])) -> BOT -> 20  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 31  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 26  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 21
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 31, which took 0.024766 s (model generation: 0.024142,  model checking: 0.000624):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4681},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, z>(q_gen_4652) -> q_gen_4681
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4681) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, s, s>(q_gen_4645) -> q_gen_4655
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
<s, z, s>(q_gen_4681) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 20  ;  () -> leq([z, z]) -> 20  ;  () -> mult([n, z, z]) -> 20  ;  () -> plus([n, z, n]) -> 20  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23  ;  (leq([s(nn1), z])) -> BOT -> 21  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 34  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 27  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 22
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(s(z))  ;  _dq -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 32, which took 0.022558 s (model generation: 0.021610,  model checking: 0.000948):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4681},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, z>(q_gen_4652) -> q_gen_4681
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4681) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
<s, z, s>(q_gen_4681) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 21  ;  () -> leq([z, z]) -> 21  ;  () -> mult([n, z, z]) -> 21  ;  () -> plus([n, z, n]) -> 21  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24  ;  (leq([s(nn1), z])) -> BOT -> 22  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 37  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 28  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 23
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 33, which took 0.024451 s (model generation: 0.023280,  model checking: 0.001171):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4646, q_gen_4648, q_gen_4673},
Q_f={q_gen_4646},
Delta=
{
<s>(q_gen_4648) -> q_gen_4648
<z>() -> q_gen_4648
<s, s>(q_gen_4646) -> q_gen_4646
<z, s>(q_gen_4648) -> q_gen_4646
<z, z>() -> q_gen_4646
<s, s>(q_gen_4673) -> q_gen_4673
<s, z>(q_gen_4648) -> q_gen_4673
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4645, q_gen_4652, q_gen_4655, q_gen_4662, q_gen_4672, q_gen_4681},
Q_f={q_gen_4645, q_gen_4655},
Delta=
{
<s>(q_gen_4652) -> q_gen_4652
<z>() -> q_gen_4652
<s, s>(q_gen_4662) -> q_gen_4662
<z, s>(q_gen_4652) -> q_gen_4662
<z, z>() -> q_gen_4662
<s, z>(q_gen_4652) -> q_gen_4681
<s, s, s>(q_gen_4645) -> q_gen_4645
<s, z, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4662) -> q_gen_4645
<z, s, s>(q_gen_4681) -> q_gen_4645
<z, s, z>(q_gen_4652) -> q_gen_4645
<z, z, s>(q_gen_4652) -> q_gen_4645
<z, z, z>() -> q_gen_4645
<s, z, z>(q_gen_4652) -> q_gen_4655
<s, s, s>(q_gen_4655) -> q_gen_4672
<s, s, s>(q_gen_4672) -> q_gen_4672
<s, z, s>(q_gen_4681) -> q_gen_4672
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 22  ;  () -> leq([z, z]) -> 22  ;  () -> mult([n, z, z]) -> 22  ;  () -> plus([n, z, n]) -> 22  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25  ;  (leq([s(nn1), z])) -> BOT -> 23  ;  (mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 40  ;  (mult([n, s(m), _iq])) -> leq([n, _iq]) -> 29  ;  (plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 24
}
Sat witness: Yes: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> z  ;  _dq -> s(s(z))  ;  mm -> s(s(z))  ;  n -> z
})

Total time: 0.584657
Reason for stopping: Proved