Solving ../../benchmarks/true/mult_leq.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)])}
(plus([_vu, _wu, _xu]) /\ plus([_vu, _wu, _yu])) -> eq_nat([_xu, _yu])
)
(mult, F:
{() -> mult([n, z, z])
(mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av])}
(mult([_bv, _cv, _dv]) /\ mult([_bv, _cv, _ev])) -> eq_nat([_dv, _ev])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
}

properties:
{(leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv])}


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

Clause system for inference is:

{
() -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 0  ;  () -> mult([n, z, z]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0  ;  (leq([s(nn1), z])) -> BOT -> 0  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 0  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 0  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 0
}


Solving took 0.503033 seconds.
Proved
Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, s>(q_gen_4594) -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, s>(q_gen_4613) -> q_gen_4613
<s, z>(q_gen_4584) -> q_gen_4613
<s, s, s>(q_gen_4577) -> q_gen_4577
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4613) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4613) -> q_gen_4604
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004068 s (model generation: 0.003893,  model checking: 0.000175):

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

}

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

}

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.003552 s (model generation: 0.003501,  model checking: 0.000051):

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

}

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.003366 s (model generation: 0.003340,  model checking: 0.000026):

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

}

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

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

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

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

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

})

-------------------------------------------
Step 3, which took 0.004321 s (model generation: 0.004280,  model checking: 0.000041):

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

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

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

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

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

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

-------------------------------------------
Step 4, which took 0.003574 s (model generation: 0.003504,  model checking: 0.000070):

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

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

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

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

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

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

-------------------------------------------
Step 5, which took 0.004399 s (model generation: 0.004295,  model checking: 0.000104):

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

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

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

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

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

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

-------------------------------------------
Step 6, which took 0.006669 s (model generation: 0.006434,  model checking: 0.000235):

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

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

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

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

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

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

-------------------------------------------
Step 7, which took 0.010863 s (model generation: 0.009670,  model checking: 0.001193):

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

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

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

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

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

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

-------------------------------------------
Step 8, which took 0.007931 s (model generation: 0.007342,  model checking: 0.000589):

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

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

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

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

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

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

-------------------------------------------
Step 9, which took 0.012711 s (model generation: 0.012497,  model checking: 0.000214):

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

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

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

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

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

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

-------------------------------------------
Step 10, which took 0.012370 s (model generation: 0.012271,  model checking: 0.000099):

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

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

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

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

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

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

-------------------------------------------
Step 11, which took 0.012649 s (model generation: 0.012165,  model checking: 0.000484):

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

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

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

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

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

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

-------------------------------------------
Step 12, which took 0.015248 s (model generation: 0.012929,  model checking: 0.002319):

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

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

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

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

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

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

-------------------------------------------
Step 13, which took 0.014032 s (model generation: 0.013612,  model checking: 0.000420):

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

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

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

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

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

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

-------------------------------------------
Step 14, which took 0.012361 s (model generation: 0.011622,  model checking: 0.000739):

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

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

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

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

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

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

-------------------------------------------
Step 15, which took 0.016182 s (model generation: 0.014593,  model checking: 0.001589):

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

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

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

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

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

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

-------------------------------------------
Step 16, which took 0.016407 s (model generation: 0.016177,  model checking: 0.000230):

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

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

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

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

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

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

-------------------------------------------
Step 17, which took 0.013004 s (model generation: 0.012985,  model checking: 0.000019):

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

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

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

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

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

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

-------------------------------------------
Step 18, which took 0.016275 s (model generation: 0.016080,  model checking: 0.000195):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4606},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<s, s>(q_gen_4606) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, z>(q_gen_4580) -> q_gen_4606
}

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

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

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

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

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

-------------------------------------------
Step 19, which took 0.018057 s (model generation: 0.015858,  model checking: 0.002199):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4594, q_gen_4603},
Q_f={q_gen_4577},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, z>() -> q_gen_4594
<s, s, s>(q_gen_4603) -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4603
<z, z, s>(q_gen_4584) -> q_gen_4603
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  () -> mult([n, z, z]) -> 10  ;  () -> plus([n, z, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 10  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 10  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]), {
_uu -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 20, which took 0.018474 s (model generation: 0.017420,  model checking: 0.001054):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4594, q_gen_4603},
Q_f={q_gen_4577},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, z>() -> q_gen_4594
<s, s, s>(q_gen_4603) -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4603
<z, z, s>(q_gen_4584) -> q_gen_4603
}

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

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

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

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

-------------------------------------------
Step 21, which took 0.012339 s (model generation: 0.011538,  model checking: 0.000801):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, z>() -> q_gen_4594
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<z, s, s>(q_gen_4594) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 10  ;  () -> leq([z, z]) -> 10  ;  () -> mult([n, z, z]) -> 11  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 11  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 16  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 14
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(z)  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.009249 s (model generation: 0.007795,  model checking: 0.001454):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4583, q_gen_4584, q_gen_4594, q_gen_4604},
Q_f={q_gen_4577, q_gen_4583},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, z>() -> q_gen_4594
<s, s, s>(q_gen_4577) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4583
<z, s, z>(q_gen_4584) -> q_gen_4583
<s, s, s>(q_gen_4583) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 11  ;  () -> leq([z, z]) -> 11  ;  () -> mult([n, z, z]) -> 12  ;  () -> plus([n, z, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12  ;  (leq([s(nn1), z])) -> BOT -> 12  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 12  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 19  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 15
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> z  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 23, which took 0.013251 s (model generation: 0.012714,  model checking: 0.000537):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4583, q_gen_4584, q_gen_4594, q_gen_4604},
Q_f={q_gen_4577, q_gen_4583},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4583
<s, z, z>(q_gen_4584) -> q_gen_4583
<z, s, z>(q_gen_4584) -> q_gen_4583
<s, s, s>(q_gen_4583) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 12  ;  () -> leq([z, z]) -> 12  ;  () -> mult([n, z, z]) -> 13  ;  () -> plus([n, z, n]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 13  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 22  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 16
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(z)  ;  _zu -> s(z)  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 24, which took 0.010727 s (model generation: 0.009954,  model checking: 0.000773):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4603},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, s, s>(q_gen_4603) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4603
<z, z, s>(q_gen_4584) -> q_gen_4603
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 13  ;  () -> leq([z, z]) -> 13  ;  () -> mult([n, z, z]) -> 13  ;  () -> plus([n, z, n]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 16  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 22  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 16
}
Sat witness: Yes: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 25, which took 0.022876 s (model generation: 0.021398,  model checking: 0.001478):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 14  ;  () -> leq([z, z]) -> 14  ;  () -> mult([n, z, z]) -> 14  ;  () -> plus([n, z, n]) -> 14  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14  ;  (leq([s(nn1), z])) -> BOT -> 14  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 17  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 25  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 17
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(s(z)))  ;  _zu -> z  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 26, which took 0.022793 s (model generation: 0.021920,  model checking: 0.000873):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 15  ;  () -> leq([z, z]) -> 15  ;  () -> mult([n, z, z]) -> 15  ;  () -> plus([n, z, n]) -> 15  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15  ;  (leq([s(nn1), z])) -> BOT -> 15  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 20  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 25  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 18
}
Sat witness: Yes: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 27, which took 0.019768 s (model generation: 0.019588,  model checking: 0.000180):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605, q_gen_4606},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4606) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4606
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4603},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, s, s>(q_gen_4603) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4603
<s, z, s>(q_gen_4594) -> q_gen_4603
<z, z, s>(q_gen_4584) -> q_gen_4603
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 15  ;  () -> leq([z, z]) -> 15  ;  () -> mult([n, z, z]) -> 15  ;  () -> plus([n, z, n]) -> 15  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18  ;  (leq([s(nn1), z])) -> BOT -> 16  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 20  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 25  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 18
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 28, which took 0.021738 s (model generation: 0.020678,  model checking: 0.001060):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4623},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, z>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4623
<s, z, s>(q_gen_4623) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4594) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 16  ;  () -> leq([z, z]) -> 16  ;  () -> mult([n, z, z]) -> 16  ;  () -> plus([n, z, n]) -> 16  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19  ;  (leq([s(nn1), z])) -> BOT -> 17  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 21  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 28  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 19
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> z  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 29, which took 0.026599 s (model generation: 0.025527,  model checking: 0.001072):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z>(q_gen_4584) -> q_gen_4613
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<z, s, s>(q_gen_4613) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4613) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 17  ;  () -> leq([z, z]) -> 17  ;  () -> mult([n, z, z]) -> 17  ;  () -> plus([n, z, n]) -> 17  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20  ;  (leq([s(nn1), z])) -> BOT -> 18  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 22  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 31  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 20
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(z)  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 30, which took 0.018395 s (model generation: 0.017600,  model checking: 0.000795):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z>(q_gen_4584) -> q_gen_4613
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4613) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, s, s>(q_gen_4577) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4613) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 18  ;  () -> leq([z, z]) -> 18  ;  () -> mult([n, z, z]) -> 18  ;  () -> plus([n, z, n]) -> 18  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21  ;  (leq([s(nn1), z])) -> BOT -> 19  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 23  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 34  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 21
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 31, which took 0.023187 s (model generation: 0.022360,  model checking: 0.000827):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z>(q_gen_4584) -> q_gen_4613
<s, s, s>(q_gen_4577) -> q_gen_4577
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4613) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4613) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 19  ;  () -> leq([z, z]) -> 19  ;  () -> mult([n, z, z]) -> 19  ;  () -> plus([n, z, n]) -> 19  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22  ;  (leq([s(nn1), z])) -> BOT -> 20  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 24  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 37  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 22
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(s(z)))  ;  _zu -> z  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 32, which took 0.026683 s (model generation: 0.025738,  model checking: 0.000945):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, s>(q_gen_4594) -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z>(q_gen_4584) -> q_gen_4613
<s, s, s>(q_gen_4577) -> q_gen_4577
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4613) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
<s, z, s>(q_gen_4613) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 20  ;  () -> leq([z, z]) -> 20  ;  () -> mult([n, z, z]) -> 20  ;  () -> plus([n, z, n]) -> 20  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23  ;  (leq([s(nn1), z])) -> BOT -> 21  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 25  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 40  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 23
}
Sat witness: Yes: ((mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]), {
_av -> s(s(z))  ;  _zu -> z  ;  mm -> s(s(z))  ;  n -> z
})

-------------------------------------------
Step 33, which took 0.023494 s (model generation: 0.023013,  model checking: 0.000481):

Model:
|_
{
leq -> 
{{{
Q={q_gen_4578, q_gen_4580, q_gen_4605},
Q_f={q_gen_4578},
Delta=
{
<s>(q_gen_4580) -> q_gen_4580
<z>() -> q_gen_4580
<s, s>(q_gen_4578) -> q_gen_4578
<z, s>(q_gen_4580) -> q_gen_4578
<z, z>() -> q_gen_4578
<s, s>(q_gen_4605) -> q_gen_4605
<s, z>(q_gen_4580) -> q_gen_4605
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  mult -> 
{{{
Q={q_gen_4577, q_gen_4584, q_gen_4587, q_gen_4594, q_gen_4604, q_gen_4613},
Q_f={q_gen_4577, q_gen_4587},
Delta=
{
<s>(q_gen_4584) -> q_gen_4584
<z>() -> q_gen_4584
<s, s>(q_gen_4594) -> q_gen_4594
<s, s>(q_gen_4613) -> q_gen_4594
<z, s>(q_gen_4584) -> q_gen_4594
<z, z>() -> q_gen_4594
<s, z>(q_gen_4584) -> q_gen_4613
<s, s, s>(q_gen_4577) -> q_gen_4577
<s, z, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4594) -> q_gen_4577
<z, s, s>(q_gen_4613) -> q_gen_4577
<z, s, z>(q_gen_4584) -> q_gen_4577
<z, z, s>(q_gen_4584) -> q_gen_4577
<z, z, z>() -> q_gen_4577
<s, z, s>(q_gen_4613) -> q_gen_4587
<s, z, z>(q_gen_4584) -> q_gen_4587
<s, s, s>(q_gen_4587) -> q_gen_4604
<s, s, s>(q_gen_4604) -> q_gen_4604
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, s(nn2)]) -> 21  ;  () -> leq([z, z]) -> 21  ;  () -> mult([n, z, z]) -> 21  ;  () -> plus([n, z, n]) -> 21  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24  ;  (leq([s(nn1), z])) -> BOT -> 22  ;  (leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]) -> 28  ;  (mult([n, mm, _zu]) /\ plus([n, _zu, _av])) -> mult([n, s(mm), _av]) -> 40  ;  (plus([n, mm, _uu])) -> plus([n, s(mm), s(_uu)]) -> 24
}
Sat witness: Yes: ((leq([s(z), m]) /\ mult([n, m, _fv])) -> leq([n, _fv]), {
_fv -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(s(s(z))))
})

Total time: 0.503033
Reason for stopping: Proved