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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)])}
(plus([_b, _c, _d]) /\ plus([_b, _c, _e])) -> eq_nat([_d, _e])
)
(mult, F:
{() -> mult([n, z, z])
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g])}
(mult([_h, _i, _j]) /\ mult([_h, _i, _k])) -> eq_nat([_j, _k])
)
(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), _l])) -> leq([n, _l])}


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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 0
(mult([n, s(m), _l])) -> leq([n, _l]) -> 0
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 0
}


Solving took 0.653942 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_43},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_43) -> q_gen_43
<s, z>(q_gen_14) -> q_gen_43
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_43) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
<s, z, s>(q_gen_43) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011991 s (model generation: 0.009814,  model checking: 0.002177):

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

}

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

}

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

}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 1
(mult([n, s(m), _l])) -> leq([n, _l]) -> 1
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010151 s (model generation: 0.010052,  model checking: 0.000099):

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

}

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

}

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

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 1
(mult([n, s(m), _l])) -> leq([n, _l]) -> 1
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 1
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.009087 s (model generation: 0.009041,  model checking: 0.000046):

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

}

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

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

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 1
(mult([n, s(m), _l])) -> leq([n, _l]) -> 1
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 3, which took 0.010363 s (model generation: 0.010293,  model checking: 0.000070):

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

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

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

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 1
(mult([n, s(m), _l])) -> leq([n, _l]) -> 1
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 4, which took 0.008957 s (model generation: 0.008805,  model checking: 0.000152):

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

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

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

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

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

-------------------------------------------
Step 5, which took 0.007945 s (model generation: 0.007808,  model checking: 0.000137):

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

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

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<z, z>() -> q_gen_12
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 4
(mult([n, s(m), _l])) -> leq([n, _l]) -> 2
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 4
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.009368 s (model generation: 0.008431,  model checking: 0.000937):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<z>() -> q_gen_14
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<z, z>() -> q_gen_12
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

-------------------------------------------
Step 7, which took 0.008671 s (model generation: 0.008445,  model checking: 0.000226):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<z>() -> q_gen_14
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<z, z>() -> q_gen_12
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 4
(mult([n, s(m), _l])) -> leq([n, _l]) -> 3
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.009072 s (model generation: 0.008850,  model checking: 0.000222):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<z>() -> q_gen_14
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 4
(mult([n, s(m), _l])) -> leq([n, _l]) -> 4
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 4
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.008611 s (model generation: 0.008509,  model checking: 0.000102):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 4
(mult([n, s(m), _l])) -> leq([n, _l]) -> 4
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 4
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 10, which took 0.010103 s (model generation: 0.009953,  model checking: 0.000150):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12},
Q_f={q_gen_11},
Delta=
{
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 4
(mult([n, s(m), _l])) -> leq([n, _l]) -> 4
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]), {
_a -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.013031 s (model generation: 0.012842,  model checking: 0.000189):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 7
(mult([n, s(m), _l])) -> leq([n, _l]) -> 5
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 7
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.011611 s (model generation: 0.011033,  model checking: 0.000578):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

-------------------------------------------
Step 13, which took 0.013061 s (model generation: 0.012541,  model checking: 0.000520):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 7
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 10
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 14, which took 0.014922 s (model generation: 0.014688,  model checking: 0.000234):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 10
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 10
}
Sat witness: Found: ((mult([n, s(m), _l])) -> leq([n, _l]), {
_l -> s(z)  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.013473 s (model generation: 0.013438,  model checking: 0.000035):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 10
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 10
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 16, which took 0.013320 s (model generation: 0.013230,  model checking: 0.000090):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_36},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<s, s>(q_gen_36) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, z>(q_gen_10) -> q_gen_36
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 10
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 10
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 17, which took 0.017934 s (model generation: 0.017293,  model checking: 0.000641):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27, q_gen_33},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_33) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_33
<z, z, s>(q_gen_14) -> q_gen_33
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 10
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]), {
_a -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 18, which took 0.015395 s (model generation: 0.015002,  model checking: 0.000393):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27, q_gen_33},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_33) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_33
<z, z, s>(q_gen_14) -> q_gen_33
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 10
(mult([n, s(m), _l])) -> leq([n, _l]) -> 13
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 13
}
Sat witness: Found: ((mult([n, s(m), _l])) -> leq([n, _l]), {
_l -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 19, which took 0.019888 s (model generation: 0.019288,  model checking: 0.000600):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_27) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 10
() -> mult([n, z, z]) -> 10
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 13
(mult([n, s(m), _l])) -> leq([n, _l]) -> 13
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 13
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(z)  ;  _g -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.017855 s (model generation: 0.017093,  model checking: 0.000762):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_27) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 11
() -> mult([n, z, z]) -> 11
() -> plus([n, z, n]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 16
(mult([n, s(m), _l])) -> leq([n, _l]) -> 14
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 14
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(z)  ;  _g -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 21, which took 0.017114 s (model generation: 0.016791,  model checking: 0.000323):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_19, q_gen_27, q_gen_30},
Q_f={q_gen_13},
Delta=
{
<z>() -> q_gen_14
<s>(q_gen_14) -> q_gen_19
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, z>(q_gen_19) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_30) -> q_gen_30
<s, z, z>(q_gen_14) -> q_gen_30
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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]) -> 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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 16
(mult([n, s(m), _l])) -> leq([n, _l]) -> 14
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 14
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(z)
})

-------------------------------------------
Step 22, which took 0.016889 s (model generation: 0.016063,  model checking: 0.000826):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_27) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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]) -> 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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 19
(mult([n, s(m), _l])) -> leq([n, _l]) -> 15
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 15
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.019409 s (model generation: 0.018917,  model checking: 0.000492):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_27) -> q_gen_18
<z, z, z>() -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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]) -> 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, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 19
(mult([n, s(m), _l])) -> leq([n, _l]) -> 18
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 16
}
Sat witness: Found: ((mult([n, s(m), _l])) -> leq([n, _l]), {
_l -> s(s(z))  ;  m -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 24, which took 0.020360 s (model generation: 0.020155,  model checking: 0.000205):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35, q_gen_36},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<s, s>(q_gen_35) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_36) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_36
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_27, q_gen_33},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s, s>(q_gen_33) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_33
<s, z, s>(q_gen_27) -> q_gen_33
<z, z, s>(q_gen_14) -> q_gen_33
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 19
(mult([n, s(m), _l])) -> leq([n, _l]) -> 18
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 16
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 25, which took 0.021292 s (model generation: 0.020270,  model checking: 0.001022):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_26, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_26
<s, s, s>(q_gen_26) -> q_gen_26
<s, z, s>(q_gen_27) -> q_gen_26
<z, s, s>(q_gen_27) -> q_gen_26
<z, z, s>(q_gen_14) -> q_gen_26
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_24, q_gen_25, q_gen_29},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, s>(q_gen_29) -> q_gen_29
<z, s>(q_gen_25) -> q_gen_29
<s, s, s>(q_gen_24) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
<s, z, s>(q_gen_29) -> q_gen_24
<z, s, s>(q_gen_29) -> q_gen_24
<z, z, s>(q_gen_25) -> q_gen_24
}

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

}
--
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]) -> 17
(leq([s(nn1), z])) -> BOT -> 16
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 19
(mult([n, s(m), _l])) -> leq([n, _l]) -> 18
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 19
}
Sat witness: Found: ((plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]), {
_a -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 26, which took 0.025261 s (model generation: 0.024479,  model checking: 0.000782):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_43},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_27) -> q_gen_43
<s, z>(q_gen_14) -> q_gen_43
<s, z, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_43) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_18
<s, z, s>(q_gen_43) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_27) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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]) -> 18
(leq([s(nn1), z])) -> BOT -> 17
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 22
(mult([n, s(m), _l])) -> leq([n, _l]) -> 19
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 20
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(z)  ;  _g -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 27, which took 0.024561 s (model generation: 0.023789,  model checking: 0.000772):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_26, q_gen_27},
Q_f={q_gen_13},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_26
<s, s, s>(q_gen_26) -> q_gen_26
<s, z, s>(q_gen_27) -> q_gen_26
<z, s, s>(q_gen_27) -> q_gen_26
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_24, q_gen_25, q_gen_29},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, z>() -> q_gen_12
<s, s>(q_gen_29) -> q_gen_29
<z, s>(q_gen_25) -> q_gen_29
<s, s, s>(q_gen_11) -> q_gen_11
<s, s, s>(q_gen_24) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, z>() -> q_gen_11
<s, z, s>(q_gen_29) -> q_gen_24
<z, s, s>(q_gen_29) -> q_gen_24
<z, z, s>(q_gen_25) -> q_gen_24
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 25
(mult([n, s(m), _l])) -> leq([n, _l]) -> 20
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 21
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 28, which took 0.025891 s (model generation: 0.025431,  model checking: 0.000460):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_45},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_27) -> q_gen_45
<z, s>(q_gen_14) -> q_gen_45
<s, z, s>(q_gen_45) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_18
<s, z, s>(q_gen_27) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_45) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 25
(mult([n, s(m), _l])) -> leq([n, _l]) -> 23
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 21
}
Sat witness: Found: ((mult([n, s(m), _l])) -> leq([n, _l]), {
_l -> s(s(s(z)))  ;  m -> z  ;  n -> s(s(s(s(z))))
})

-------------------------------------------
Step 29, which took 0.028878 s (model generation: 0.028018,  model checking: 0.000860):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_50},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<z, s>(q_gen_14) -> q_gen_50
<s, s, s>(q_gen_13) -> q_gen_13
<s, z, s>(q_gen_50) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, z, s>(q_gen_27) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 28
(mult([n, s(m), _l])) -> leq([n, _l]) -> 24
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 22
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(s(z))  ;  _g -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 30, which took 0.033861 s (model generation: 0.033065,  model checking: 0.000796):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_50},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<s, z>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<z, s>(q_gen_14) -> q_gen_50
<s, z, s>(q_gen_50) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
<s, z, s>(q_gen_27) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 31
(mult([n, s(m), _l])) -> leq([n, _l]) -> 25
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 23
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> z  ;  _g -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 31, which took 0.037123 s (model generation: 0.036196,  model checking: 0.000927):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_43},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_43) -> q_gen_43
<s, z>(q_gen_14) -> q_gen_43
<s, z, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<z, s, s>(q_gen_43) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
<s, z, s>(q_gen_43) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 34
(mult([n, s(m), _l])) -> leq([n, _l]) -> 26
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 24
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(z)  ;  _g -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 32, which took 0.045129 s (model generation: 0.043860,  model checking: 0.001269):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_26, q_gen_27, q_gen_34, q_gen_43},
Q_f={q_gen_13, q_gen_26},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_43) -> q_gen_43
<s, z>(q_gen_14) -> q_gen_43
<s, s, s>(q_gen_26) -> q_gen_13
<s, z, s>(q_gen_43) -> q_gen_13
<s, z, z>(q_gen_14) -> q_gen_13
<z, s, s>(q_gen_43) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<s, z, s>(q_gen_27) -> q_gen_26
<z, s, s>(q_gen_27) -> q_gen_26
<z, z, s>(q_gen_14) -> q_gen_26
<z, z, z>() -> q_gen_26
<s, s, s>(q_gen_13) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

}
--
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]) -> 23
() -> plus([n, z, n]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 23
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 37
(mult([n, s(m), _l])) -> leq([n, _l]) -> 27
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 25
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(z)  ;  _g -> s(z)  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 33, which took 0.039353 s (model generation: 0.038103,  model checking: 0.001250):

Model:
|_
{
leq -> 
{{{
Q={q_gen_10, q_gen_15, q_gen_35},
Q_f={q_gen_15},
Delta=
{
<s>(q_gen_10) -> q_gen_10
<z>() -> q_gen_10
<s, s>(q_gen_15) -> q_gen_15
<z, s>(q_gen_10) -> q_gen_15
<z, z>() -> q_gen_15
<s, s>(q_gen_35) -> q_gen_35
<s, z>(q_gen_10) -> q_gen_35
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_13, q_gen_14, q_gen_18, q_gen_27, q_gen_34, q_gen_43},
Q_f={q_gen_13, q_gen_18},
Delta=
{
<s>(q_gen_14) -> q_gen_14
<z>() -> q_gen_14
<s, s>(q_gen_27) -> q_gen_27
<z, s>(q_gen_14) -> q_gen_27
<z, z>() -> q_gen_27
<s, s>(q_gen_43) -> q_gen_43
<s, z>(q_gen_14) -> q_gen_43
<s, z, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_27) -> q_gen_13
<z, s, s>(q_gen_43) -> q_gen_13
<z, s, z>(q_gen_14) -> q_gen_13
<z, z, s>(q_gen_14) -> q_gen_13
<z, z, z>() -> q_gen_13
<s, s, s>(q_gen_13) -> q_gen_18
<s, z, s>(q_gen_43) -> q_gen_18
<s, z, z>(q_gen_14) -> q_gen_18
<s, s, s>(q_gen_18) -> q_gen_34
<s, s, s>(q_gen_34) -> q_gen_34
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_11, q_gen_12, q_gen_25},
Q_f={q_gen_11},
Delta=
{
<s>(q_gen_25) -> q_gen_25
<z>() -> q_gen_25
<s, s>(q_gen_12) -> q_gen_12
<z, s>(q_gen_25) -> q_gen_12
<z, z>() -> q_gen_12
<s, s, s>(q_gen_11) -> q_gen_11
<s, z, s>(q_gen_12) -> q_gen_11
<z, s, s>(q_gen_12) -> q_gen_11
<z, z, s>(q_gen_25) -> q_gen_11
<z, z, z>() -> q_gen_11
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 23
() -> leq([z, z]) -> 23
() -> mult([n, z, z]) -> 24
() -> plus([n, z, n]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 24
(mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]) -> 40
(mult([n, s(m), _l])) -> leq([n, _l]) -> 28
(plus([n, mm, _a])) -> plus([n, s(mm), s(_a)]) -> 26
}
Sat witness: Found: ((mult([n, mm, _f]) /\ plus([n, _f, _g])) -> mult([n, s(mm), _g]), {
_f -> s(s(z))  ;  _g -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

Total time: 0.653942
Reason for stopping: Proved