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, _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.659274 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s>(q_gen_3140) -> q_gen_3140
<s, z>(q_gen_3110) -> q_gen_3140
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3140) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
<s, z, s>(q_gen_3140) -> q_gen_3130
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010251 s (model generation: 0.009770,  model checking: 0.000481):

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

}

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

}

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

-------------------------------------------
Step 1, which took 0.010156 s (model generation: 0.009986,  model checking: 0.000170):

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

}

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

}

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

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

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

-------------------------------------------
Step 2, which took 0.010369 s (model generation: 0.010284,  model checking: 0.000085):

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

}

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

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

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

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

})

-------------------------------------------
Step 3, which took 0.010379 s (model generation: 0.010255,  model checking: 0.000124):

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

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

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

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

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

-------------------------------------------
Step 4, which took 0.011730 s (model generation: 0.010573,  model checking: 0.001157):

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

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

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

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

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

-------------------------------------------
Step 5, which took 0.011165 s (model generation: 0.010896,  model checking: 0.000269):

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

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

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

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

}
--
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: Found: ((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.011296 s (model generation: 0.010962,  model checking: 0.000334):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3110
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 7, which took 0.011785 s (model generation: 0.011307,  model checking: 0.000478):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3110
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 8, which took 0.012971 s (model generation: 0.012493,  model checking: 0.000478):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3110
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 9, which took 0.012315 s (model generation: 0.012026,  model checking: 0.000289):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 10, which took 0.012568 s (model generation: 0.012215,  model checking: 0.000353):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 11, which took 0.014074 s (model generation: 0.013711,  model checking: 0.000363):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

}
--
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: Found: ((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.015211 s (model generation: 0.013700,  model checking: 0.001511):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 5
() -> mult([n, z, z]) -> 7
() -> plus([n, z, n]) -> 7
(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)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 13, which took 0.015020 s (model generation: 0.014308,  model checking: 0.000712):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 6
() -> mult([n, z, z]) -> 7
() -> plus([n, z, n]) -> 7
(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]) -> 10
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 7
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Found: ((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 14, which took 0.016767 s (model generation: 0.016254,  model checking: 0.000513):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

}
--
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]) -> 7
() -> plus([n, z, n]) -> 7
(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]) -> 10
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Found: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(z)  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.017382 s (model generation: 0.017312,  model checking: 0.000070):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

}
--
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]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 10
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 10
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 16, which took 0.018333 s (model generation: 0.018161,  model checking: 0.000172):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3132},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<s, s>(q_gen_3132) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, z>(q_gen_3106) -> q_gen_3132
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
}

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

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

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

-------------------------------------------
Step 17, which took 0.018649 s (model generation: 0.017147,  model checking: 0.001502):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123, q_gen_3129},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3129) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3129
<z, z, s>(q_gen_3110) -> q_gen_3129
}

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

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

}
--
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]) -> 8
() -> plus([n, z, n]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 10
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]), {
_xp -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 18, which took 0.019528 s (model generation: 0.018516,  model checking: 0.001012):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123, q_gen_3129},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3129) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3129
<z, z, s>(q_gen_3110) -> q_gen_3129
}

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

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

}
--
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]) -> 9
() -> plus([n, z, n]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 13
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Found: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 19, which took 0.020471 s (model generation: 0.019924,  model checking: 0.000547):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3115, q_gen_3123, q_gen_3126},
Q_f={q_gen_3103},
Delta=
{
<z>() -> q_gen_3110
<s>(q_gen_3110) -> q_gen_3115
<z, z>() -> q_gen_3123
<s, z, z>(q_gen_3115) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3126
<s, s, s>(q_gen_3126) -> q_gen_3126
<s, z, z>(q_gen_3110) -> q_gen_3126
}

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

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

}
--
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]) -> 12
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 10
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 13
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(z)
})

-------------------------------------------
Step 20, which took 0.020860 s (model generation: 0.020257,  model checking: 0.000603):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131, q_gen_3132},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3132) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3132
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3123, q_gen_3129},
Q_f={q_gen_3103},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3129) -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3129
<z, z, s>(q_gen_3110) -> q_gen_3129
}

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

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

}
--
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]) -> 12
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 13
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 13
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 13
}
Sat witness: Found: ((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.022995 s (model generation: 0.021217,  model checking: 0.001778):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3109, q_gen_3110, q_gen_3123, q_gen_3130},
Q_f={q_gen_3103, q_gen_3109},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3109
<z, s, s>(q_gen_3123) -> q_gen_3109
<z, s, z>(q_gen_3110) -> q_gen_3109
<s, s, s>(q_gen_3109) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 13
() -> plus([n, z, n]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(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]) -> 16
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 14
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 14
}
Sat witness: Found: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(z)  ;  _dq -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 22, which took 0.023429 s (model generation: 0.021694,  model checking: 0.001735):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3109, q_gen_3110, q_gen_3123, q_gen_3130},
Q_f={q_gen_3103, q_gen_3109},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, z>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3109
<s, z, z>(q_gen_3110) -> q_gen_3109
<z, s, z>(q_gen_3110) -> q_gen_3109
<s, s, s>(q_gen_3109) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 14
() -> plus([n, z, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(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]) -> 19
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 15
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 15
}
Sat witness: Found: ((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 23, which took 0.025592 s (model generation: 0.023848,  model checking: 0.001744):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, z>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3123) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 15
() -> 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]) -> 22
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 16
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 16
}
Sat witness: Found: ((mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]), {
_cq -> s(z)  ;  _dq -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 24, which took 0.026646 s (model generation: 0.024794,  model checking: 0.001852):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3123) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 16
() -> 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]) -> 25
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 17
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 17
}
Sat witness: Found: ((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 25, which took 0.029724 s (model generation: 0.028315,  model checking: 0.001409):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3123) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 17
() -> 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]) -> 25
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 20
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 18
}
Sat witness: Found: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(z))  ;  m -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 26, which took 0.034555 s (model generation: 0.034254,  model checking: 0.000301):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131, q_gen_3132},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3132) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3132
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3129},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, s, s>(q_gen_3129) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3123) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3129
<s, z, s>(q_gen_3123) -> q_gen_3129
<z, z, s>(q_gen_3110) -> q_gen_3129
}

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

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

}
--
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]) -> 17
() -> plus([n, z, n]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(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]) -> 20
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 18
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 27, which took 0.032844 s (model generation: 0.031001,  model checking: 0.001843):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3149},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3149
<s, z, s>(q_gen_3149) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, z, s>(q_gen_3123) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3123) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 18
() -> plus([n, z, n]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 17
(mult([n, mm, _cq]) /\ plus([n, _cq, _dq])) -> mult([n, s(mm), _dq]) -> 28
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 21
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 19
}
Sat witness: Found: ((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 28, which took 0.035780 s (model generation: 0.034442,  model checking: 0.001338):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3140
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, s>(q_gen_3140) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3140) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 19
() -> 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]) -> 31
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 22
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 20
}
Sat witness: Found: ((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 -> z
})

-------------------------------------------
Step 29, which took 0.014481 s (model generation: 0.013450,  model checking: 0.001031):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3149},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3149
<s, z, s>(q_gen_3149) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
<s, z, s>(q_gen_3123) -> q_gen_3130
}

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

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

}
--
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]) -> 20
() -> 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]) -> 34
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 23
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 21
}
Sat witness: Found: ((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 30, which took 0.017342 s (model generation: 0.015911,  model checking: 0.001431):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<s, s>(q_gen_3140) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, z>(q_gen_3110) -> q_gen_3140
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, z, s>(q_gen_3140) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3140) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 21
() -> 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]) -> 34
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 26
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 22
}
Sat witness: Found: ((mult([n, s(m), _iq])) -> leq([n, _iq]), {
_iq -> s(s(s(z)))  ;  m -> z  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 31, which took 0.018589 s (model generation: 0.017585,  model checking: 0.001004):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s>(q_gen_3140) -> q_gen_3140
<s, z>(q_gen_3110) -> q_gen_3140
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, z, s>(q_gen_3140) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<z, s, s>(q_gen_3140) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 22
() -> 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]) -> 37
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 27
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 23
}
Sat witness: Found: ((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 32, which took 0.020383 s (model generation: 0.019484,  model checking: 0.000899):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s>(q_gen_3123) -> q_gen_3140
<s, s>(q_gen_3140) -> q_gen_3140
<s, z>(q_gen_3110) -> q_gen_3140
<s, s, s>(q_gen_3103) -> q_gen_3103
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3140) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, z, s>(q_gen_3140) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
}

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

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

}
--
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]) -> 23
() -> 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]) -> 40
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 28
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 24
}
Sat witness: Found: ((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.025252 s (model generation: 0.024542,  model checking: 0.000710):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3104, q_gen_3106, q_gen_3131},
Q_f={q_gen_3104},
Delta=
{
<s>(q_gen_3106) -> q_gen_3106
<z>() -> q_gen_3106
<s, s>(q_gen_3104) -> q_gen_3104
<z, s>(q_gen_3106) -> q_gen_3104
<z, z>() -> q_gen_3104
<s, s>(q_gen_3131) -> q_gen_3131
<s, z>(q_gen_3106) -> q_gen_3131
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3103, q_gen_3110, q_gen_3114, q_gen_3123, q_gen_3130, q_gen_3140},
Q_f={q_gen_3103, q_gen_3114},
Delta=
{
<s>(q_gen_3110) -> q_gen_3110
<z>() -> q_gen_3110
<s, s>(q_gen_3123) -> q_gen_3123
<z, s>(q_gen_3110) -> q_gen_3123
<z, z>() -> q_gen_3123
<s, s>(q_gen_3140) -> q_gen_3140
<s, z>(q_gen_3110) -> q_gen_3140
<s, z, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3123) -> q_gen_3103
<z, s, s>(q_gen_3140) -> q_gen_3103
<z, s, z>(q_gen_3110) -> q_gen_3103
<z, z, s>(q_gen_3110) -> q_gen_3103
<z, z, z>() -> q_gen_3103
<s, s, s>(q_gen_3103) -> q_gen_3114
<s, z, z>(q_gen_3110) -> q_gen_3114
<s, s, s>(q_gen_3114) -> q_gen_3130
<s, s, s>(q_gen_3130) -> q_gen_3130
<s, z, s>(q_gen_3140) -> q_gen_3130
}

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

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

}
--
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]) -> 24
() -> 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]) -> 43
(mult([n, s(m), _iq])) -> leq([n, _iq]) -> 29
(plus([n, mm, _xp])) -> plus([n, s(mm), s(_xp)]) -> 25
}
Sat witness: Found: ((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))
})

Total time: 0.659274
Reason for stopping: Proved