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, _uu])) -> plus([n, s(mm), s(_uu)])}
(plus([_vu, _wu, _xu]) /\ plus([_vu, _wu, _yu])) -> eq_nat([_xu, _yu])
)
(mult, F:
{() -> mult([n, z, z])
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av])}
(mult([_bv, _cv, _dv]) /\ mult([_bv, _cv, _ev])) -> eq_nat([_dv, _ev])
)
(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:
{(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv])}


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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 0
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 0
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 0
}


Solving took 0.864788 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989, q_gen_4001},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, s>(q_gen_3982) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, s>(q_gen_4001) -> q_gen_4001
<s, z>(q_gen_3969) -> q_gen_4001
<s, s, s>(q_gen_3962) -> q_gen_3962
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_4001) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, z, s>(q_gen_4001) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008235 s (model generation: 0.007576,  model checking: 0.000659):

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 1
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010159 s (model generation: 0.009996,  model checking: 0.000163):

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_3961},
Q_f={q_gen_3961},
Delta=
{
<z, z, z>() -> q_gen_3961
}

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 1
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 1
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.010194 s (model generation: 0.010093,  model checking: 0.000101):

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

}

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 1
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 3, which took 0.010364 s (model generation: 0.010242,  model checking: 0.000122):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 1
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 4, which took 0.010971 s (model generation: 0.010684,  model checking: 0.000287):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 1
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.011102 s (model generation: 0.010902,  model checking: 0.000200):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 1
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> z  ;  _zu -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.011420 s (model generation: 0.011135,  model checking: 0.000285):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 2
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.013278 s (model generation: 0.012814,  model checking: 0.000464):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 3
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.012369 s (model generation: 0.011877,  model checking: 0.000492):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 4
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.012734 s (model generation: 0.011813,  model checking: 0.000921):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 4
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 4
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 10, which took 0.012946 s (model generation: 0.012614,  model checking: 0.000332):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 4
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 4
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.013785 s (model generation: 0.013477,  model checking: 0.000308):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 4
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 7
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 7
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.015552 s (model generation: 0.013699,  model checking: 0.001853):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 5
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 7
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 13, which took 0.015119 s (model generation: 0.014158,  model checking: 0.000961):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 6
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> z  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 14, which took 0.016445 s (model generation: 0.016210,  model checking: 0.000235):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 9
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(z)  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.017784 s (model generation: 0.017722,  model checking: 0.000062):

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

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

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

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 -> 9
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 9
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 16, which took 0.017624 s (model generation: 0.017437,  model checking: 0.000187):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3991},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<s, s>(q_gen_3991) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, z>(q_gen_3965) -> q_gen_3991
}

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

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

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]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 9
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 17, which took 0.018872 s (model generation: 0.017314,  model checking: 0.001558):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3982, q_gen_3988},
Q_f={q_gen_3962},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, z>() -> q_gen_3982
<s, s, s>(q_gen_3988) -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3988
<z, z, s>(q_gen_3969) -> q_gen_3988
}

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

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]) -> 7
() -> mult([n, z, z]) -> 8
() -> plus([n, z, n]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 12
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 10
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 18, which took 0.020578 s (model generation: 0.019172,  model checking: 0.001406):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, z>() -> q_gen_3982
<s, s, s>(q_gen_3962) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3973
<z, s, s>(q_gen_3982) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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]) -> 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]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 12
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 19, which took 0.021922 s (model generation: 0.021327,  model checking: 0.000595):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3974, q_gen_3982, q_gen_3985},
Q_f={q_gen_3962},
Delta=
{
<z>() -> q_gen_3969
<s>(q_gen_3969) -> q_gen_3974
<z, z>() -> q_gen_3982
<s, z, z>(q_gen_3974) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3985
<s, s, s>(q_gen_3985) -> q_gen_3985
<s, z, z>(q_gen_3969) -> q_gen_3985
}

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

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)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 12
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 13
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(z)
})

-------------------------------------------
Step 20, which took 0.021816 s (model generation: 0.021040,  model checking: 0.000776):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3982, q_gen_3987, q_gen_3989},
Q_f={q_gen_3962, q_gen_3987},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, z>() -> q_gen_3982
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3987) -> q_gen_3987
<z, z, s>(q_gen_3969) -> q_gen_3987
<s, s, s>(q_gen_3962) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 12
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 13
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 13
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 21, which took 0.024542 s (model generation: 0.022806,  model checking: 0.001736):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3981, q_gen_3982, q_gen_3989},
Q_f={q_gen_3962, q_gen_3981},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, z>() -> q_gen_3982
<s, s, s>(q_gen_3981) -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3981
<z, z, s>(q_gen_3969) -> q_gen_3981
<s, s, s>(q_gen_3962) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 13
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 16
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 14
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 22, which took 0.024971 s (model generation: 0.023034,  model checking: 0.001937):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, s, s>(q_gen_3962) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 14
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 19
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 15
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(s(z)))  ;  _zu -> z  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.026999 s (model generation: 0.026060,  model checking: 0.000939):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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]) -> 14
() -> 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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 17
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 19
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 15
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 24, which took 0.032517 s (model generation: 0.032241,  model checking: 0.000276):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990, q_gen_3991},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3991) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3991
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3988},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3973
<s, s, s>(q_gen_3988) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3988
<s, z, s>(q_gen_3982) -> q_gen_3988
<z, z, s>(q_gen_3969) -> q_gen_3988
}

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

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]) -> 14
() -> plus([n, z, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16
(leq([s(nn1), z])) -> BOT -> 14
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 17
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 19
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 15
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 25, which took 0.033406 s (model generation: 0.031350,  model checking: 0.002056):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989, q_gen_4001},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z>(q_gen_3969) -> q_gen_4001
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<z, s, s>(q_gen_4001) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
<s, z, s>(q_gen_4001) -> q_gen_3989
}

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

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]) -> 15
() -> plus([n, z, n]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 15
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 18
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 22
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 16
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(z)  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 26, which took 0.033690 s (model generation: 0.031937,  model checking: 0.001753):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3968, q_gen_3969, q_gen_3982, q_gen_3989, q_gen_4001},
Q_f={q_gen_3962, q_gen_3968},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z>(q_gen_3969) -> q_gen_4001
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_4001) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3968
<s, z, z>(q_gen_3969) -> q_gen_3968
<z, s, z>(q_gen_3969) -> q_gen_3968
<s, s, s>(q_gen_3968) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
<s, z, s>(q_gen_4001) -> q_gen_3989
}

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

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]) -> 16
() -> 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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 19
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 25
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 17
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> s(z)  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 27, which took 0.038139 s (model generation: 0.036183,  model checking: 0.001956):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989, q_gen_4001},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z>(q_gen_3969) -> q_gen_4001
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_4001) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
<s, z, s>(q_gen_4001) -> q_gen_3989
}

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

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]) -> 17
() -> 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
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 20
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 28
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 18
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 28, which took 0.048830 s (model generation: 0.047450,  model checking: 0.001380):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3981, q_gen_3982},
Q_f={q_gen_3962},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3981
<s, s, s>(q_gen_3981) -> q_gen_3981
<s, z, s>(q_gen_3982) -> q_gen_3981
<z, s, s>(q_gen_3982) -> q_gen_3981
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3961, q_gen_3967, q_gen_3979, q_gen_3980, q_gen_3984},
Q_f={q_gen_3961},
Delta=
{
<s>(q_gen_3980) -> q_gen_3980
<z>() -> q_gen_3980
<s, s>(q_gen_3967) -> q_gen_3967
<z, z>() -> q_gen_3967
<s, s>(q_gen_3984) -> q_gen_3984
<z, s>(q_gen_3980) -> q_gen_3984
<s, s, s>(q_gen_3979) -> q_gen_3961
<s, z, s>(q_gen_3967) -> q_gen_3961
<z, s, s>(q_gen_3967) -> q_gen_3961
<z, z, z>() -> q_gen_3961
<s, s, s>(q_gen_3961) -> q_gen_3979
<s, z, s>(q_gen_3984) -> q_gen_3979
<z, s, s>(q_gen_3984) -> q_gen_3979
<z, z, s>(q_gen_3980) -> q_gen_3979
}

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]) -> 18
() -> plus([n, z, n]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 18
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 20
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 28
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 21
}
Sat witness: Found: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 29, which took 0.050829 s (model generation: 0.048951,  model checking: 0.001878):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3982, q_gen_3987},
Q_f={q_gen_3962},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z, s>(q_gen_3982) -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3987
<s, s, s>(q_gen_3987) -> q_gen_3987
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3961, q_gen_3967, q_gen_3979, q_gen_3980, q_gen_3984},
Q_f={q_gen_3961},
Delta=
{
<s>(q_gen_3980) -> q_gen_3980
<z>() -> q_gen_3980
<s, s>(q_gen_3967) -> q_gen_3967
<z, z>() -> q_gen_3967
<s, s>(q_gen_3984) -> q_gen_3984
<z, s>(q_gen_3980) -> q_gen_3984
<s, s, s>(q_gen_3961) -> q_gen_3961
<s, s, s>(q_gen_3979) -> q_gen_3961
<s, z, s>(q_gen_3967) -> q_gen_3961
<z, s, s>(q_gen_3967) -> q_gen_3961
<z, z, z>() -> q_gen_3961
<s, z, s>(q_gen_3984) -> q_gen_3979
<z, s, s>(q_gen_3984) -> q_gen_3979
<z, z, s>(q_gen_3980) -> q_gen_3979
}

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]) -> 19
() -> plus([n, z, n]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20
(leq([s(nn1), z])) -> BOT -> 19
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 21
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 31
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 22
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 30, which took 0.051914 s (model generation: 0.050028,  model checking: 0.001886):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3982, q_gen_3987},
Q_f={q_gen_3962},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z, z>(q_gen_3969) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, s, s>(q_gen_3962) -> q_gen_3987
<s, s, s>(q_gen_3987) -> q_gen_3987
<s, z, s>(q_gen_3982) -> q_gen_3987
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3961, q_gen_3967, q_gen_3979, q_gen_3980, q_gen_3984},
Q_f={q_gen_3961},
Delta=
{
<s>(q_gen_3980) -> q_gen_3980
<z>() -> q_gen_3980
<s, s>(q_gen_3967) -> q_gen_3967
<z, z>() -> q_gen_3967
<s, s>(q_gen_3984) -> q_gen_3984
<z, s>(q_gen_3980) -> q_gen_3984
<s, s, s>(q_gen_3961) -> q_gen_3961
<s, s, s>(q_gen_3979) -> q_gen_3961
<s, z, s>(q_gen_3967) -> q_gen_3961
<z, s, s>(q_gen_3967) -> q_gen_3961
<z, z, z>() -> q_gen_3961
<s, z, s>(q_gen_3984) -> q_gen_3979
<z, s, s>(q_gen_3984) -> q_gen_3979
<z, z, s>(q_gen_3980) -> q_gen_3979
}

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]) -> 20
() -> plus([n, z, n]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 20
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 22
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 34
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 23
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> z  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 31, which took 0.055632 s (model generation: 0.053674,  model checking: 0.001958):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989, q_gen_4001},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<z, s>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, z>(q_gen_3969) -> q_gen_4001
<s, s, s>(q_gen_3962) -> q_gen_3962
<s, z, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, s>(q_gen_4001) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
<s, z, s>(q_gen_4001) -> q_gen_3989
}

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

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]) -> 21
() -> plus([n, z, n]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 21
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 23
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 37
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 24
}
Sat witness: Found: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(s(z)))  ;  _zu -> z  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 32, which took 0.065896 s (model generation: 0.064647,  model checking: 0.001249):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3963, q_gen_3965, q_gen_3990},
Q_f={q_gen_3963},
Delta=
{
<s>(q_gen_3965) -> q_gen_3965
<z>() -> q_gen_3965
<s, s>(q_gen_3963) -> q_gen_3963
<z, s>(q_gen_3965) -> q_gen_3963
<z, z>() -> q_gen_3963
<s, s>(q_gen_3990) -> q_gen_3990
<s, z>(q_gen_3965) -> q_gen_3990
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  mult -> 
{{{
Q={q_gen_3962, q_gen_3969, q_gen_3973, q_gen_3982, q_gen_3989, q_gen_4006},
Q_f={q_gen_3962, q_gen_3973},
Delta=
{
<s>(q_gen_3969) -> q_gen_3969
<z>() -> q_gen_3969
<s, z>(q_gen_3969) -> q_gen_3982
<z, z>() -> q_gen_3982
<s, s>(q_gen_3982) -> q_gen_4006
<z, s>(q_gen_3969) -> q_gen_4006
<s, s, s>(q_gen_3962) -> q_gen_3962
<s, z, s>(q_gen_4006) -> q_gen_3962
<z, s, s>(q_gen_3982) -> q_gen_3962
<z, s, z>(q_gen_3969) -> q_gen_3962
<z, z, s>(q_gen_3969) -> q_gen_3962
<z, z, z>() -> q_gen_3962
<s, z, s>(q_gen_3982) -> q_gen_3973
<s, z, z>(q_gen_3969) -> q_gen_3973
<s, s, s>(q_gen_3973) -> q_gen_3989
<s, s, s>(q_gen_3989) -> q_gen_3989
}

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

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]) -> 22
() -> plus([n, z, n]) -> 21
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 22
(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 26
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 37
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 24
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(s(s(z))))
})

Total time: 0.864788
Reason for stopping: Proved