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, _ma])) -> plus([n, s(mm), s(_ma)])}
(plus([_na, _oa, _pa]) /\ plus([_na, _oa, _qa])) -> eq_nat([_pa, _qa])
)
(mult, F:
{() -> mult([n, z, z])
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa])}
(mult([_ta, _ua, _va]) /\ mult([_ta, _ua, _wa])) -> eq_nat([_va, _wa])
)
(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, _xa])) -> leq([n, _xa])}


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, _xa])) -> leq([n, _xa]) -> 0
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 0
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 0
}


Solving took 0.654644 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307, q_gen_319},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, s>(q_gen_300) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, s>(q_gen_319) -> q_gen_319
<s, z>(q_gen_287) -> q_gen_319
<s, s, s>(q_gen_280) -> q_gen_280
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_319) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, z, s>(q_gen_319) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007758 s (model generation: 0.007470,  model checking: 0.000288):

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 1
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 1
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.012367 s (model generation: 0.012214,  model checking: 0.000153):

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 1
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 1
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 1
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> z
})

-------------------------------------------
Step 2, which took 0.009559 s (model generation: 0.009507,  model checking: 0.000052):

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

}

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 1
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 1
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 3, which took 0.008227 s (model generation: 0.008158,  model checking: 0.000069):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 1
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 1
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 4, which took 0.007666 s (model generation: 0.007519,  model checking: 0.000147):

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

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

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

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

-------------------------------------------
Step 5, which took 0.007852 s (model generation: 0.007751,  model checking: 0.000101):

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

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

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

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

-------------------------------------------
Step 6, which took 0.009287 s (model generation: 0.008619,  model checking: 0.000668):

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

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

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

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

-------------------------------------------
Step 7, which took 0.008299 s (model generation: 0.008079,  model checking: 0.000220):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 3
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 4
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.009115 s (model generation: 0.008890,  model checking: 0.000225):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 4
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 4
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 4
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.011080 s (model generation: 0.010981,  model checking: 0.000099):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 4
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 4
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 4
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 10, which took 0.008883 s (model generation: 0.008733,  model checking: 0.000150):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 4
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 4
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]), {
_ma -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.010265 s (model generation: 0.010116,  model checking: 0.000149):

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

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

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 4
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 7
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 7
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> z  ;  _sa -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.010903 s (model generation: 0.010414,  model checking: 0.000489):

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

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

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

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

-------------------------------------------
Step 13, which took 0.011211 s (model generation: 0.010834,  model checking: 0.000377):

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

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

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

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

-------------------------------------------
Step 14, which took 0.012848 s (model generation: 0.012736,  model checking: 0.000112):

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

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

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

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

-------------------------------------------
Step 15, which took 0.013147 s (model generation: 0.013113,  model checking: 0.000034):

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

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

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

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

-------------------------------------------
Step 16, which took 0.014298 s (model generation: 0.014207,  model checking: 0.000091):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_309},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<s, s>(q_gen_309) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, z>(q_gen_283) -> q_gen_309
}

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

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

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

-------------------------------------------
Step 17, which took 0.013985 s (model generation: 0.013539,  model checking: 0.000446):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_300, q_gen_306},
Q_f={q_gen_280},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, z>() -> q_gen_300
<s, s, s>(q_gen_306) -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_306
<z, z, s>(q_gen_287) -> q_gen_306
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 12
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 10
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 10
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]), {
_xa -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 18, which took 0.014924 s (model generation: 0.014089,  model checking: 0.000835):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, z>() -> q_gen_300
<s, s, s>(q_gen_280) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_291
<z, s, s>(q_gen_300) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 12
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 10
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]), {
_ma -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 19, which took 0.016454 s (model generation: 0.016180,  model checking: 0.000274):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_292, q_gen_300, q_gen_303},
Q_f={q_gen_280},
Delta=
{
<z>() -> q_gen_287
<s>(q_gen_287) -> q_gen_292
<z, z>() -> q_gen_300
<s, z, z>(q_gen_292) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_303
<s, s, s>(q_gen_303) -> q_gen_303
<s, z, z>(q_gen_287) -> q_gen_303
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 12
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 10
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 13
}
Sat witness: Found: (() -> mult([n, z, z]), {
n -> s(z)
})

-------------------------------------------
Step 20, which took 0.017490 s (model generation: 0.017204,  model checking: 0.000286):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_300, q_gen_305, q_gen_307},
Q_f={q_gen_280, q_gen_305},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, z>() -> q_gen_300
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_305) -> q_gen_305
<z, z, s>(q_gen_287) -> q_gen_305
<s, s, s>(q_gen_280) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 12
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 13
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 13
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> s(s(z))  ;  _sa -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 21, which took 0.018275 s (model generation: 0.017305,  model checking: 0.000970):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_299, q_gen_300, q_gen_307},
Q_f={q_gen_280, q_gen_299},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, z>() -> q_gen_300
<s, s, s>(q_gen_299) -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_299
<z, z, s>(q_gen_287) -> q_gen_299
<s, s, s>(q_gen_280) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 13
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 16
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 14
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> s(z)  ;  _sa -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 22, which took 0.018825 s (model generation: 0.017786,  model checking: 0.001039):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, s, s>(q_gen_280) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 14
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 19
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 15
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> z  ;  _sa -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.021745 s (model generation: 0.021369,  model checking: 0.000376):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 17
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 19
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 15
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]), {
_xa -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 24, which took 0.022507 s (model generation: 0.022340,  model checking: 0.000167):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308, q_gen_309},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<s, s>(q_gen_308) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_309) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_309
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_306},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_291
<s, s, s>(q_gen_306) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_306
<s, z, s>(q_gen_300) -> q_gen_306
<z, z, s>(q_gen_287) -> q_gen_306
}

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

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]) -> 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, _xa])) -> leq([n, _xa]) -> 17
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 19
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 15
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 25, which took 0.023777 s (model generation: 0.022612,  model checking: 0.001165):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307, q_gen_319},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z>(q_gen_287) -> q_gen_319
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<z, s, s>(q_gen_319) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
<s, z, s>(q_gen_319) -> q_gen_307
}

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 18
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 22
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 16
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> s(z)  ;  _sa -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 26, which took 0.026357 s (model generation: 0.025503,  model checking: 0.000854):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_286, q_gen_287, q_gen_300, q_gen_307, q_gen_319},
Q_f={q_gen_280, q_gen_286},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z>(q_gen_287) -> q_gen_319
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_319) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_286
<s, z, z>(q_gen_287) -> q_gen_286
<z, s, z>(q_gen_287) -> q_gen_286
<s, s, s>(q_gen_286) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
<s, z, s>(q_gen_319) -> q_gen_307
}

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

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

-------------------------------------------
Step 27, which took 0.035982 s (model generation: 0.034796,  model checking: 0.001186):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307, q_gen_319},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z>(q_gen_287) -> q_gen_319
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_319) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
<s, z, s>(q_gen_319) -> q_gen_307
}

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

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]) -> 19
(leq([s(nn1), z])) -> BOT -> 17
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 20
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 28
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 18
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> s(s(z))  ;  _sa -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 28, which took 0.035628 s (model generation: 0.034666,  model checking: 0.000962):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_299, q_gen_300},
Q_f={q_gen_280},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_299
<s, s, s>(q_gen_299) -> q_gen_299
<s, z, s>(q_gen_300) -> q_gen_299
<z, s, s>(q_gen_300) -> q_gen_299
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_279, q_gen_285, q_gen_297, q_gen_298, q_gen_302},
Q_f={q_gen_279},
Delta=
{
<s>(q_gen_298) -> q_gen_298
<z>() -> q_gen_298
<s, s>(q_gen_285) -> q_gen_285
<z, z>() -> q_gen_285
<s, s>(q_gen_302) -> q_gen_302
<z, s>(q_gen_298) -> q_gen_302
<s, s, s>(q_gen_297) -> q_gen_279
<s, z, s>(q_gen_285) -> q_gen_279
<z, s, s>(q_gen_285) -> q_gen_279
<z, z, z>() -> q_gen_279
<s, s, s>(q_gen_279) -> q_gen_297
<s, z, s>(q_gen_302) -> q_gen_297
<z, s, s>(q_gen_302) -> q_gen_297
<z, z, s>(q_gen_298) -> q_gen_297
}

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 20
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 28
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 21
}
Sat witness: Found: ((plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]), {
_ma -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 29, which took 0.036609 s (model generation: 0.035455,  model checking: 0.001154):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_300, q_gen_305},
Q_f={q_gen_280},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z, s>(q_gen_300) -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_305
<s, s, s>(q_gen_305) -> q_gen_305
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_279, q_gen_285, q_gen_297, q_gen_298, q_gen_302},
Q_f={q_gen_279},
Delta=
{
<s>(q_gen_298) -> q_gen_298
<z>() -> q_gen_298
<s, s>(q_gen_285) -> q_gen_285
<z, z>() -> q_gen_285
<s, s>(q_gen_302) -> q_gen_302
<z, s>(q_gen_298) -> q_gen_302
<s, s, s>(q_gen_279) -> q_gen_279
<s, s, s>(q_gen_297) -> q_gen_279
<s, z, s>(q_gen_285) -> q_gen_279
<z, s, s>(q_gen_285) -> q_gen_279
<z, z, z>() -> q_gen_279
<s, z, s>(q_gen_302) -> q_gen_297
<z, s, s>(q_gen_302) -> q_gen_297
<z, z, s>(q_gen_298) -> q_gen_297
}

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 21
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 31
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 22
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> s(z)  ;  _sa -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 30, which took 0.037762 s (model generation: 0.036692,  model checking: 0.001070):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_300, q_gen_305},
Q_f={q_gen_280},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z, z>(q_gen_287) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, s, s>(q_gen_280) -> q_gen_305
<s, s, s>(q_gen_305) -> q_gen_305
<s, z, s>(q_gen_300) -> q_gen_305
}

Datatype: <nat, nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_279, q_gen_285, q_gen_297, q_gen_298, q_gen_302},
Q_f={q_gen_279},
Delta=
{
<s>(q_gen_298) -> q_gen_298
<z>() -> q_gen_298
<s, s>(q_gen_285) -> q_gen_285
<z, z>() -> q_gen_285
<s, s>(q_gen_302) -> q_gen_302
<z, s>(q_gen_298) -> q_gen_302
<s, s, s>(q_gen_279) -> q_gen_279
<s, s, s>(q_gen_297) -> q_gen_279
<s, z, s>(q_gen_285) -> q_gen_279
<z, s, s>(q_gen_285) -> q_gen_279
<z, z, z>() -> q_gen_279
<s, z, s>(q_gen_302) -> q_gen_297
<z, s, s>(q_gen_302) -> q_gen_297
<z, z, s>(q_gen_298) -> q_gen_297
}

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 22
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 34
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 23
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> z  ;  _sa -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 31, which took 0.039253 s (model generation: 0.037907,  model checking: 0.001346):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307, q_gen_319},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<z, s>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, z>(q_gen_287) -> q_gen_319
<s, s, s>(q_gen_280) -> q_gen_280
<s, z, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, s>(q_gen_319) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
<s, z, s>(q_gen_319) -> q_gen_307
}

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 23
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 37
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 24
}
Sat witness: Found: ((mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]), {
_ra -> z  ;  _sa -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 32, which took 0.046211 s (model generation: 0.045650,  model checking: 0.000561):

Model:
|_
{
leq -> 
{{{
Q={q_gen_281, q_gen_283, q_gen_308},
Q_f={q_gen_281},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<s, s>(q_gen_281) -> q_gen_281
<z, s>(q_gen_283) -> q_gen_281
<z, z>() -> q_gen_281
<s, s>(q_gen_308) -> q_gen_308
<s, z>(q_gen_283) -> q_gen_308
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  mult -> 
{{{
Q={q_gen_280, q_gen_287, q_gen_291, q_gen_300, q_gen_307, q_gen_324},
Q_f={q_gen_280, q_gen_291},
Delta=
{
<s>(q_gen_287) -> q_gen_287
<z>() -> q_gen_287
<s, z>(q_gen_287) -> q_gen_300
<z, z>() -> q_gen_300
<s, s>(q_gen_300) -> q_gen_324
<z, s>(q_gen_287) -> q_gen_324
<s, s, s>(q_gen_280) -> q_gen_280
<s, z, s>(q_gen_324) -> q_gen_280
<z, s, s>(q_gen_300) -> q_gen_280
<z, s, z>(q_gen_287) -> q_gen_280
<z, z, s>(q_gen_287) -> q_gen_280
<z, z, z>() -> q_gen_280
<s, z, s>(q_gen_300) -> q_gen_291
<s, z, z>(q_gen_287) -> q_gen_291
<s, s, s>(q_gen_291) -> q_gen_307
<s, s, s>(q_gen_307) -> q_gen_307
}

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

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
(leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]) -> 26
(mult([n, mm, _ra]) /\ plus([n, _ra, _sa])) -> mult([n, s(mm), _sa]) -> 37
(plus([n, mm, _ma])) -> plus([n, s(mm), s(_ma)]) -> 24
}
Sat witness: Found: ((leq([s(z), m]) /\ mult([n, m, _xa])) -> leq([n, _xa]), {
_xa -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(s(s(z))))
})

Total time: 0.654644
Reason for stopping: Proved