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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(is_even, P:
{() -> is_even([z])
(is_even([n3])) -> is_even([s(s(n3))])
(is_even([s(s(n3))])) -> is_even([n3])
(is_even([s(z)])) -> BOT}
)
(is_odd, P:
{() -> is_odd([s(z)])
(is_odd([n3])) -> is_odd([s(s(n3))])
(is_odd([s(s(n3))])) -> is_odd([n3])
(is_odd([z])) -> BOT}
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)])}
(plus([_sy, _ty, _uy]) /\ plus([_sy, _ty, _vy])) -> eq_nat([_uy, _vy])
)
}

properties:
{(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy])}


over-approximation: {is_odd, plus}
under-approximation: {is_even}

Clause system for inference is:

{
() -> is_even([z]) -> 0
() -> is_odd([s(z)]) -> 0
() -> plus([n, z, n]) -> 0
(is_even([n3])) -> is_even([s(s(n3))]) -> 0
(is_even([s(s(n3))])) -> is_even([n3]) -> 0
(is_even([s(z)])) -> BOT -> 0
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 0
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 0
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 0
(is_odd([z])) -> BOT -> 0
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 0
}


Solving took 0.360104 seconds.
Proved
Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582, q_gen_6586, q_gen_6597},
Q_f={q_gen_6567},
Delta=
{
<s>(q_gen_6597) -> q_gen_6582
<z>() -> q_gen_6582
<s>(q_gen_6582) -> q_gen_6597
<s, s>(q_gen_6572) -> q_gen_6572
<z, s>(q_gen_6597) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6586) -> q_gen_6586
<z, s>(q_gen_6582) -> q_gen_6586
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, s>(q_gen_6597) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<s, z, s>(q_gen_6586) -> q_gen_6581
<z, s, s>(q_gen_6586) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.016335 s (model generation: 0.016074,  model checking: 0.000261):

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

}

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

}

Datatype: <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:
{
() -> is_even([z]) -> 0
() -> is_odd([s(z)]) -> 0
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 1
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.012945 s (model generation: 0.012903,  model checking: 0.000042):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 0
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 1
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 1
}
Sat witness: Found: (() -> is_odd([s(z)]), {

})

-------------------------------------------
Step 2, which took 0.021563 s (model generation: 0.021526,  model checking: 0.000037):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 1
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 1
}
Sat witness: Found: (() -> is_even([z]), {

})

-------------------------------------------
Step 3, which took 0.012547 s (model generation: 0.012442,  model checking: 0.000105):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 1
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 4, which took 0.012161 s (model generation: 0.012144,  model checking: 0.000017):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 1
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: ((is_odd([z])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.009316 s (model generation: 0.009185,  model checking: 0.000131):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 2
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 2
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: ((is_odd([n3])) -> is_odd([s(s(n3))]), {
n3 -> s(z)
})

-------------------------------------------
Step 6, which took 0.010343 s (model generation: 0.010277,  model checking: 0.000066):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 2
(is_even([s(z)])) -> BOT -> 2
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 2
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 2
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 7, which took 0.010219 s (model generation: 0.010142,  model checking: 0.000077):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6570) -> q_gen_6570
<z>() -> q_gen_6570
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 2
(is_even([s(z)])) -> BOT -> 5
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 3
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 3
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 8, which took 0.010780 s (model generation: 0.010580,  model checking: 0.000200):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 3
() -> is_odd([s(z)]) -> 3
() -> plus([n, z, n]) -> 6
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 3
(is_even([s(z)])) -> BOT -> 5
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 4
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 4
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.011781 s (model generation: 0.011571,  model checking: 0.000210):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 4
() -> is_odd([s(z)]) -> 4
() -> plus([n, z, n]) -> 6
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 4
(is_even([s(z)])) -> BOT -> 5
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 4
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 4
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.016280 s (model generation: 0.016135,  model checking: 0.000145):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

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

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 4
() -> is_odd([s(z)]) -> 4
() -> plus([n, z, n]) -> 6
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 4
(is_even([s(z)])) -> BOT -> 5
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 4
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 7
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 5
(is_odd([z])) -> BOT -> 5
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 7
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]), {
_wy -> s(z)  ;  x -> s(z)  ;  y -> s(z)
})

-------------------------------------------
Step 11, which took 0.012648 s (model generation: 0.011771,  model checking: 0.000877):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 5
() -> is_odd([s(z)]) -> 5
() -> plus([n, z, n]) -> 7
(is_even([n3])) -> is_even([s(s(n3))]) -> 5
(is_even([s(s(n3))])) -> is_even([n3]) -> 5
(is_even([s(z)])) -> BOT -> 6
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 5
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 7
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 6
(is_odd([z])) -> BOT -> 6
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 12, which took 0.015866 s (model generation: 0.015478,  model checking: 0.000388):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6571, q_gen_6572, q_gen_6582, q_gen_6583},
Q_f={q_gen_6567, q_gen_6571},
Delta=
{
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, s>(q_gen_6582) -> q_gen_6572
<z, z>() -> q_gen_6572
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6571) -> q_gen_6571
<s, z, s>(q_gen_6572) -> q_gen_6571
<z, s, s>(q_gen_6572) -> q_gen_6571
<z, z, s>(q_gen_6582) -> q_gen_6571
<s, s, s>(q_gen_6567) -> q_gen_6583
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 6
() -> is_odd([s(z)]) -> 6
() -> plus([n, z, n]) -> 7
(is_even([n3])) -> is_even([s(s(n3))]) -> 6
(is_even([s(s(n3))])) -> is_even([n3]) -> 6
(is_even([s(z)])) -> BOT -> 7
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 6
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 7
(is_odd([z])) -> BOT -> 7
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 10
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]), {
_wy -> s(s(s(z)))  ;  x -> s(s(s(z)))  ;  y -> s(z)
})

-------------------------------------------
Step 13, which took 0.019849 s (model generation: 0.019150,  model checking: 0.000699):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6571, q_gen_6572, q_gen_6582, q_gen_6583},
Q_f={q_gen_6567, q_gen_6571},
Delta=
{
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, s>(q_gen_6582) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6571) -> q_gen_6571
<z, s, s>(q_gen_6572) -> q_gen_6571
<z, z, s>(q_gen_6582) -> q_gen_6571
<s, s, s>(q_gen_6567) -> q_gen_6583
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 7
() -> is_odd([s(z)]) -> 7
() -> plus([n, z, n]) -> 8
(is_even([n3])) -> is_even([s(s(n3))]) -> 7
(is_even([s(s(n3))])) -> is_even([n3]) -> 7
(is_even([s(z)])) -> BOT -> 8
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 7
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 8
(is_odd([z])) -> BOT -> 8
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.022761 s (model generation: 0.022428,  model checking: 0.000333):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6578, q_gen_6579, q_gen_6582},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<z, s>(q_gen_6582) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6572) -> q_gen_6578
<s, s, s>(q_gen_6579) -> q_gen_6567
<s, z, s>(q_gen_6578) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, s>(q_gen_6582) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6579
<s, z, s>(q_gen_6572) -> q_gen_6579
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 8
() -> is_odd([s(z)]) -> 8
() -> plus([n, z, n]) -> 11
(is_even([n3])) -> is_even([s(s(n3))]) -> 8
(is_even([s(s(n3))])) -> is_even([n3]) -> 8
(is_even([s(z)])) -> BOT -> 9
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 8
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 9
(is_odd([z])) -> BOT -> 9
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 13
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 15, which took 0.017093 s (model generation: 0.016189,  model checking: 0.000904):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582, q_gen_6586},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, z>() -> q_gen_6572
<z, s>(q_gen_6582) -> q_gen_6586
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<s, z, s>(q_gen_6586) -> q_gen_6581
<z, s, s>(q_gen_6586) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 9
() -> is_odd([s(z)]) -> 9
() -> plus([n, z, n]) -> 12
(is_even([n3])) -> is_even([s(s(n3))]) -> 9
(is_even([s(s(n3))])) -> is_even([n3]) -> 9
(is_even([s(z)])) -> BOT -> 10
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 9
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 11
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 10
(is_odd([z])) -> BOT -> 10
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 16
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 16, which took 0.017022 s (model generation: 0.015996,  model checking: 0.001026):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582, q_gen_6586},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6586) -> q_gen_6586
<z, s>(q_gen_6582) -> q_gen_6586
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<s, z, s>(q_gen_6586) -> q_gen_6581
<z, s, s>(q_gen_6586) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 10
() -> is_odd([s(z)]) -> 10
() -> plus([n, z, n]) -> 13
(is_even([n3])) -> is_even([s(s(n3))]) -> 10
(is_even([s(s(n3))])) -> is_even([n3]) -> 10
(is_even([s(z)])) -> BOT -> 11
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 10
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 12
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 11
(is_odd([z])) -> BOT -> 11
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 19
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 17, which took 0.021296 s (model generation: 0.021174,  model checking: 0.000122):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6575, q_gen_6576},
Q_f={q_gen_6570, q_gen_6575},
Delta=
{
<z>() -> q_gen_6570
<s>(q_gen_6575) -> q_gen_6575
<s>(q_gen_6576) -> q_gen_6575
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6571, q_gen_6572, q_gen_6582, q_gen_6583},
Q_f={q_gen_6567, q_gen_6571},
Delta=
{
<s>(q_gen_6582) -> q_gen_6582
<z>() -> q_gen_6582
<s, s>(q_gen_6572) -> q_gen_6572
<z, s>(q_gen_6582) -> q_gen_6572
<z, z>() -> q_gen_6572
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6571) -> q_gen_6571
<s, z, s>(q_gen_6572) -> q_gen_6571
<z, s, s>(q_gen_6572) -> q_gen_6571
<z, z, s>(q_gen_6582) -> q_gen_6571
<s, s, s>(q_gen_6567) -> q_gen_6583
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 10
() -> is_odd([s(z)]) -> 10
() -> plus([n, z, n]) -> 13
(is_even([n3])) -> is_even([s(s(n3))]) -> 10
(is_even([s(s(n3))])) -> is_even([n3]) -> 13
(is_even([s(z)])) -> BOT -> 11
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 11
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 12
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 11
(is_odd([z])) -> BOT -> 11
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 19
}
Sat witness: Found: ((is_even([s(s(n3))])) -> is_even([n3]), {
n3 -> s(z)
})

-------------------------------------------
Step 18, which took 0.018758 s (model generation: 0.018315,  model checking: 0.000443):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6571, q_gen_6572, q_gen_6578, q_gen_6582, q_gen_6583},
Q_f={q_gen_6567, q_gen_6571},
Delta=
{
<s>(q_gen_6582) -> q_gen_6582
<z>() -> q_gen_6582
<z, s>(q_gen_6582) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6572) -> q_gen_6578
<s, s, s>(q_gen_6583) -> q_gen_6567
<s, z, s>(q_gen_6578) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6571) -> q_gen_6571
<s, z, s>(q_gen_6572) -> q_gen_6571
<z, s, s>(q_gen_6572) -> q_gen_6571
<z, z, s>(q_gen_6582) -> q_gen_6571
<s, s, s>(q_gen_6567) -> q_gen_6583
<z, s, s>(q_gen_6578) -> q_gen_6583
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 11
() -> is_odd([s(z)]) -> 11
() -> plus([n, z, n]) -> 13
(is_even([n3])) -> is_even([s(s(n3))]) -> 11
(is_even([s(s(n3))])) -> is_even([n3]) -> 13
(is_even([s(z)])) -> BOT -> 12
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 12
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 15
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 12
(is_odd([z])) -> BOT -> 12
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 19
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]), {
_wy -> s(s(s(z)))  ;  x -> s(z)  ;  y -> s(z)
})

-------------------------------------------
Step 19, which took 0.020601 s (model generation: 0.019499,  model checking: 0.001102):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582, q_gen_6586, q_gen_6597},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<s>(q_gen_6582) -> q_gen_6597
<s, s>(q_gen_6572) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6586) -> q_gen_6586
<z, s>(q_gen_6582) -> q_gen_6586
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, s>(q_gen_6597) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<s, z, s>(q_gen_6586) -> q_gen_6581
<z, s, s>(q_gen_6586) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 12
() -> is_odd([s(z)]) -> 12
() -> plus([n, z, n]) -> 14
(is_even([n3])) -> is_even([s(s(n3))]) -> 12
(is_even([s(s(n3))])) -> is_even([n3]) -> 14
(is_even([s(z)])) -> BOT -> 13
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 13
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 16
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 13
(is_odd([z])) -> BOT -> 13
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 22
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(z))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.020396 s (model generation: 0.019107,  model checking: 0.001289):

Model:
|_
{
is_even -> 
{{{
Q={q_gen_6570, q_gen_6576},
Q_f={q_gen_6570},
Delta=
{
<s>(q_gen_6576) -> q_gen_6570
<z>() -> q_gen_6570
<s>(q_gen_6570) -> q_gen_6576
}

Datatype: <nat>
Convolution form: left
}}}
  ;  is_odd -> 
{{{
Q={q_gen_6568, q_gen_6569},
Q_f={q_gen_6568},
Delta=
{
<s>(q_gen_6569) -> q_gen_6568
<s>(q_gen_6568) -> q_gen_6569
<z>() -> q_gen_6569
}

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6567, q_gen_6572, q_gen_6581, q_gen_6582, q_gen_6586, q_gen_6597},
Q_f={q_gen_6567},
Delta=
{
<z>() -> q_gen_6582
<s>(q_gen_6582) -> q_gen_6597
<s, s>(q_gen_6572) -> q_gen_6572
<z, s>(q_gen_6597) -> q_gen_6572
<z, z>() -> q_gen_6572
<s, s>(q_gen_6586) -> q_gen_6586
<z, s>(q_gen_6582) -> q_gen_6586
<s, s, s>(q_gen_6581) -> q_gen_6567
<s, z, s>(q_gen_6572) -> q_gen_6567
<z, s, s>(q_gen_6572) -> q_gen_6567
<z, z, s>(q_gen_6597) -> q_gen_6567
<z, z, z>() -> q_gen_6567
<s, s, s>(q_gen_6567) -> q_gen_6581
<s, z, s>(q_gen_6586) -> q_gen_6581
<z, s, s>(q_gen_6586) -> q_gen_6581
<z, z, s>(q_gen_6582) -> q_gen_6581
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 13
() -> is_odd([s(z)]) -> 13
() -> plus([n, z, n]) -> 15
(is_even([n3])) -> is_even([s(s(n3))]) -> 13
(is_even([s(s(n3))])) -> is_even([n3]) -> 15
(is_even([s(z)])) -> BOT -> 14
(is_odd([n3])) -> is_odd([s(s(n3))]) -> 14
(is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _wy])) -> is_even([_wy]) -> 17
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 14
(is_odd([z])) -> BOT -> 14
(plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]) -> 25
}
Sat witness: Found: ((plus([n, mm, _ry])) -> plus([n, s(mm), s(_ry)]), {
_ry -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.360104
Reason for stopping: Proved