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


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, _g])) -> plus([n, s(mm), s(_g)])}
(plus([_h, _i, _j]) /\ plus([_h, _i, _k])) -> eq_nat([_j, _k])
)
}

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


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, _l])) -> is_even([_l]) -> 0
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 0
(is_odd([z])) -> BOT -> 0
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 0
}


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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35, q_gen_39, q_gen_50},
Q_f={q_gen_20},
Delta=
{
<s>(q_gen_50) -> q_gen_35
<z>() -> q_gen_35
<s>(q_gen_35) -> q_gen_50
<s, s>(q_gen_25) -> q_gen_25
<z, s>(q_gen_50) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_39) -> q_gen_39
<z, s>(q_gen_35) -> q_gen_39
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, s>(q_gen_50) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<s, z, s>(q_gen_39) -> q_gen_34
<z, s, s>(q_gen_39) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.011259 s (model generation: 0.009917,  model checking: 0.001342):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> 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, _l])) -> is_even([_l]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010092 s (model generation: 0.010031,  model checking: 0.000061):

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

}

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

}

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

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

}
--
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, _l])) -> is_even([_l]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 1
}
Sat witness: Found: (() -> is_odd([s(z)]), {

})

-------------------------------------------
Step 2, which took 0.010387 s (model generation: 0.010336,  model checking: 0.000051):

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

}

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 1
}
Sat witness: Found: (() -> is_even([z]), {

})

-------------------------------------------
Step 3, which took 0.010648 s (model generation: 0.010456,  model checking: 0.000192):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 1
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 4, which took 0.010770 s (model generation: 0.010740,  model checking: 0.000030):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 1
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 1
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: ((is_odd([z])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.011026 s (model generation: 0.010755,  model checking: 0.000271):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 2
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 2
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: ((is_odd([n3])) -> is_odd([s(s(n3))]), {
n3 -> s(z)
})

-------------------------------------------
Step 6, which took 0.011490 s (model generation: 0.011364,  model checking: 0.000126):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 2
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 2
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 7, which took 0.012421 s (model generation: 0.012009,  model checking: 0.000412):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 3
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 3
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 8, which took 0.012102 s (model generation: 0.011696,  model checking: 0.000406):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 4
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 4
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.012605 s (model generation: 0.012181,  model checking: 0.000424):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 4
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 4
(is_odd([z])) -> BOT -> 4
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.013551 s (model generation: 0.013255,  model checking: 0.000296):

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

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

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

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

}
--
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, _l])) -> is_even([_l]) -> 7
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 5
(is_odd([z])) -> BOT -> 5
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 7
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _l])) -> is_even([_l]), {
_l -> s(z)  ;  x -> s(z)  ;  y -> s(z)
})

-------------------------------------------
Step 11, which took 0.014719 s (model generation: 0.013604,  model checking: 0.001115):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, z>() -> q_gen_25
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

}
--
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, _l])) -> is_even([_l]) -> 7
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 6
(is_odd([z])) -> BOT -> 6
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 12, which took 0.015624 s (model generation: 0.015039,  model checking: 0.000585):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_24, q_gen_25, q_gen_35, q_gen_36},
Q_f={q_gen_20, q_gen_24},
Delta=
{
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, s>(q_gen_35) -> q_gen_25
<z, z>() -> q_gen_25
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_24) -> q_gen_24
<s, z, s>(q_gen_25) -> q_gen_24
<z, s, s>(q_gen_25) -> q_gen_24
<z, z, s>(q_gen_35) -> q_gen_24
<s, s, s>(q_gen_20) -> q_gen_36
}

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

}
--
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, _l])) -> is_even([_l]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 7
(is_odd([z])) -> BOT -> 7
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 10
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _l])) -> is_even([_l]), {
_l -> s(s(s(z)))  ;  x -> s(s(s(z)))  ;  y -> s(z)
})

-------------------------------------------
Step 13, which took 0.017466 s (model generation: 0.016337,  model checking: 0.001129):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_24, q_gen_25, q_gen_35, q_gen_36},
Q_f={q_gen_20, q_gen_24},
Delta=
{
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, s>(q_gen_35) -> q_gen_25
<z, z>() -> q_gen_25
<s, z, s>(q_gen_25) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_24) -> q_gen_24
<z, s, s>(q_gen_25) -> q_gen_24
<z, z, s>(q_gen_35) -> q_gen_24
<s, s, s>(q_gen_20) -> q_gen_36
}

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

}
--
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, _l])) -> is_even([_l]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 8
(is_odd([z])) -> BOT -> 8
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.018676 s (model generation: 0.018088,  model checking: 0.000588):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_31, q_gen_32, q_gen_35},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<z, s>(q_gen_35) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_25) -> q_gen_31
<s, s, s>(q_gen_32) -> q_gen_20
<s, z, s>(q_gen_31) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, s>(q_gen_35) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_32
<s, z, s>(q_gen_25) -> q_gen_32
}

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

}
--
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, _l])) -> is_even([_l]) -> 10
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 9
(is_odd([z])) -> BOT -> 9
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 13
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 15, which took 0.019555 s (model generation: 0.017980,  model checking: 0.001575):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35, q_gen_39},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, z>() -> q_gen_25
<z, s>(q_gen_35) -> q_gen_39
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<s, z, s>(q_gen_39) -> q_gen_34
<z, s, s>(q_gen_39) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

}
--
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, _l])) -> is_even([_l]) -> 11
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 10
(is_odd([z])) -> BOT -> 10
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 16
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 16, which took 0.022030 s (model generation: 0.020387,  model checking: 0.001643):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35, q_gen_39},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_39) -> q_gen_39
<z, s>(q_gen_35) -> q_gen_39
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<s, z, s>(q_gen_39) -> q_gen_34
<z, s, s>(q_gen_39) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

}
--
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, _l])) -> is_even([_l]) -> 12
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 11
(is_odd([z])) -> BOT -> 11
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 19
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 17, which took 0.025058 s (model generation: 0.024826,  model checking: 0.000232):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_24, q_gen_25, q_gen_35, q_gen_36},
Q_f={q_gen_20, q_gen_24},
Delta=
{
<s>(q_gen_35) -> q_gen_35
<z>() -> q_gen_35
<s, s>(q_gen_25) -> q_gen_25
<z, s>(q_gen_35) -> q_gen_25
<z, z>() -> q_gen_25
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_24) -> q_gen_24
<s, z, s>(q_gen_25) -> q_gen_24
<z, s, s>(q_gen_25) -> q_gen_24
<z, z, s>(q_gen_35) -> q_gen_24
<s, s, s>(q_gen_20) -> q_gen_36
}

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

}
--
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, _l])) -> is_even([_l]) -> 12
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 11
(is_odd([z])) -> BOT -> 11
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 19
}
Sat witness: Found: ((is_even([s(s(n3))])) -> is_even([n3]), {
n3 -> s(z)
})

-------------------------------------------
Step 18, which took 0.024898 s (model generation: 0.024348,  model checking: 0.000550):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_24, q_gen_25, q_gen_31, q_gen_35, q_gen_36},
Q_f={q_gen_20, q_gen_24},
Delta=
{
<s>(q_gen_35) -> q_gen_35
<z>() -> q_gen_35
<z, s>(q_gen_35) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_25) -> q_gen_31
<s, s, s>(q_gen_36) -> q_gen_20
<s, z, s>(q_gen_31) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_24) -> q_gen_24
<s, z, s>(q_gen_25) -> q_gen_24
<z, s, s>(q_gen_25) -> q_gen_24
<z, z, s>(q_gen_35) -> q_gen_24
<s, s, s>(q_gen_20) -> q_gen_36
<z, s, s>(q_gen_31) -> q_gen_36
}

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

}
--
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, _l])) -> is_even([_l]) -> 15
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 12
(is_odd([z])) -> BOT -> 12
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 19
}
Sat witness: Found: ((is_odd([x]) /\ is_odd([y]) /\ plus([x, y, _l])) -> is_even([_l]), {
_l -> s(s(s(z)))  ;  x -> s(z)  ;  y -> s(z)
})

-------------------------------------------
Step 19, which took 0.026017 s (model generation: 0.024219,  model checking: 0.001798):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35, q_gen_39, q_gen_50},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<s>(q_gen_35) -> q_gen_50
<s, s>(q_gen_25) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_39) -> q_gen_39
<z, s>(q_gen_35) -> q_gen_39
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, s>(q_gen_50) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<s, z, s>(q_gen_39) -> q_gen_34
<z, s, s>(q_gen_39) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

}
--
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, _l])) -> is_even([_l]) -> 16
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 13
(is_odd([z])) -> BOT -> 13
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 22
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(z))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.028249 s (model generation: 0.025758,  model checking: 0.002491):

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

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_20, q_gen_25, q_gen_34, q_gen_35, q_gen_39, q_gen_50},
Q_f={q_gen_20},
Delta=
{
<z>() -> q_gen_35
<s>(q_gen_35) -> q_gen_50
<s, s>(q_gen_25) -> q_gen_25
<z, s>(q_gen_50) -> q_gen_25
<z, z>() -> q_gen_25
<s, s>(q_gen_39) -> q_gen_39
<z, s>(q_gen_35) -> q_gen_39
<s, s, s>(q_gen_34) -> q_gen_20
<s, z, s>(q_gen_25) -> q_gen_20
<z, s, s>(q_gen_25) -> q_gen_20
<z, z, s>(q_gen_50) -> q_gen_20
<z, z, z>() -> q_gen_20
<s, s, s>(q_gen_20) -> q_gen_34
<s, z, s>(q_gen_39) -> q_gen_34
<z, s, s>(q_gen_39) -> q_gen_34
<z, z, s>(q_gen_35) -> q_gen_34
}

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

}
--
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, _l])) -> is_even([_l]) -> 17
(is_odd([s(s(n3))])) -> is_odd([n3]) -> 14
(is_odd([z])) -> BOT -> 14
(plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]) -> 25
}
Sat witness: Found: ((plus([n, mm, _g])) -> plus([n, s(mm), s(_g)]), {
_g -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.373049
Reason for stopping: Proved