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}
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _mc])) -> plus([n, s(mm), s(_mc)])}
(plus([_nc, _oc, _pc]) /\ plus([_nc, _oc, _qc])) -> eq_nat([_pc, _qc])
)
}

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


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

Clause system for inference is:

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


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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681, q_gen_691},
Q_f={q_gen_667},
Delta=
{
<s>(q_gen_691) -> q_gen_678
<z>() -> q_gen_678
<s>(q_gen_678) -> q_gen_691
<s, s>(q_gen_670) -> q_gen_670
<z, s>(q_gen_691) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, s>(q_gen_691) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, s, s>(q_gen_667) -> q_gen_677
<s, z, s>(q_gen_681) -> q_gen_677
<z, s, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009112 s (model generation: 0.008834,  model checking: 0.000278):

Model:
|_
{
is_even -> 
{{{
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
() -> plus([n, z, n]) -> 3
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([x]) /\ is_even([y]) /\ plus([x, y, _rc])) -> is_even([_rc]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
(plus([n, mm, _mc])) -> plus([n, s(mm), s(_mc)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.007811 s (model generation: 0.007784,  model checking: 0.000027):

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

}

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

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

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

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

})

-------------------------------------------
Step 2, which took 0.007417 s (model generation: 0.007327,  model checking: 0.000090):

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

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

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

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

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

-------------------------------------------
Step 3, which took 0.007125 s (model generation: 0.007051,  model checking: 0.000074):

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

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

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

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

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

-------------------------------------------
Step 4, which took 0.008478 s (model generation: 0.008417,  model checking: 0.000061):

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

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

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

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

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

})

-------------------------------------------
Step 5, which took 0.008369 s (model generation: 0.008140,  model checking: 0.000229):

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

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

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

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

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

-------------------------------------------
Step 6, which took 0.009117 s (model generation: 0.008535,  model checking: 0.000582):

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

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

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

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

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

-------------------------------------------
Step 7, which took 0.008995 s (model generation: 0.008876,  model checking: 0.000119):

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

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

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

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

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

-------------------------------------------
Step 8, which took 0.009958 s (model generation: 0.009341,  model checking: 0.000617):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, z>() -> q_gen_670
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 9, which took 0.009898 s (model generation: 0.009657,  model checking: 0.000241):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, s>(q_gen_678) -> q_gen_670
<z, z>() -> q_gen_670
<s, s, s>(q_gen_667) -> q_gen_667
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 10, which took 0.012323 s (model generation: 0.012250,  model checking: 0.000073):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, s>(q_gen_678) -> q_gen_670
<z, z>() -> q_gen_670
<s, s, s>(q_gen_667) -> q_gen_667
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 11, which took 0.011489 s (model generation: 0.011383,  model checking: 0.000106):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, s>(q_gen_678) -> q_gen_670
<z, z>() -> q_gen_670
<s, s, s>(q_gen_667) -> q_gen_667
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 12, which took 0.011879 s (model generation: 0.011192,  model checking: 0.000687):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, z, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 13, which took 0.013183 s (model generation: 0.012404,  model checking: 0.000779):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, z, s>(q_gen_681) -> q_gen_677
<z, s, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 14, which took 0.015005 s (model generation: 0.014490,  model checking: 0.000515):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681},
Q_f={q_gen_667},
Delta=
{
<s>(q_gen_678) -> q_gen_678
<z>() -> q_gen_678
<s, s>(q_gen_670) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_667) -> q_gen_667
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, z, s>(q_gen_681) -> q_gen_677
<z, s, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 15, which took 0.015060 s (model generation: 0.014908,  model checking: 0.000152):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_674, q_gen_675, q_gen_678, q_gen_691},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s>(q_gen_678) -> q_gen_691
<s, s>(q_gen_674) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_670) -> q_gen_674
<z, s>(q_gen_678) -> q_gen_674
<s, s, s>(q_gen_667) -> q_gen_667
<s, z, s>(q_gen_674) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, s>(q_gen_691) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, s, s>(q_gen_675) -> q_gen_675
<s, z, s>(q_gen_670) -> q_gen_675
<z, s, s>(q_gen_674) -> q_gen_675
<z, z, s>(q_gen_678) -> q_gen_675
}

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

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

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

-------------------------------------------
Step 16, which took 0.018656 s (model generation: 0.017743,  model checking: 0.000913):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681, q_gen_691},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s>(q_gen_678) -> q_gen_691
<s, s>(q_gen_670) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, s>(q_gen_691) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, s, s>(q_gen_667) -> q_gen_677
<s, z, s>(q_gen_681) -> q_gen_677
<z, s, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

-------------------------------------------
Step 17, which took 0.017378 s (model generation: 0.016261,  model checking: 0.001117):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_667, q_gen_670, q_gen_677, q_gen_678, q_gen_681, q_gen_691},
Q_f={q_gen_667},
Delta=
{
<z>() -> q_gen_678
<s>(q_gen_678) -> q_gen_691
<s, s>(q_gen_670) -> q_gen_670
<z, s>(q_gen_691) -> q_gen_670
<z, z>() -> q_gen_670
<s, s>(q_gen_681) -> q_gen_681
<z, s>(q_gen_678) -> q_gen_681
<s, s, s>(q_gen_677) -> q_gen_667
<s, z, s>(q_gen_670) -> q_gen_667
<z, s, s>(q_gen_670) -> q_gen_667
<z, z, s>(q_gen_691) -> q_gen_667
<z, z, z>() -> q_gen_667
<s, s, s>(q_gen_667) -> q_gen_677
<s, z, s>(q_gen_681) -> q_gen_677
<z, s, s>(q_gen_681) -> q_gen_677
<z, z, s>(q_gen_678) -> q_gen_677
}

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

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

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

Total time: 0.222534
Reason for stopping: Proved