Solving ../../benchmarks/true/plus_even_even.smt2...

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


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, _ny])) -> plus([n, s(mm), s(_ny)])}
(plus([_oy, _py, _qy]) /\ plus([_oy, _py, _ry])) -> eq_nat([_qy, _ry])
)
}

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


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, _sy])) -> is_even([_sy]) -> 0  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 0  ;  (is_even([s(z)])) -> BOT -> 0  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 0
}


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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4898, q_gen_4905},
Q_f={q_gen_4884},
Delta=
{
<s>(q_gen_4905) -> q_gen_4893
<z>() -> q_gen_4893
<s>(q_gen_4893) -> q_gen_4905
<s, s>(q_gen_4887) -> q_gen_4887
<z, s>(q_gen_4905) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s>(q_gen_4898) -> q_gen_4898
<z, s>(q_gen_4893) -> q_gen_4898
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, s>(q_gen_4905) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<s, s, s>(q_gen_4884) -> q_gen_4892
<s, z, s>(q_gen_4898) -> q_gen_4892
<z, s, s>(q_gen_4898) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003739 s (model generation: 0.003643,  model checking: 0.000096):

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

}

Datatype: <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:
{
() -> 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, _sy])) -> is_even([_sy]) -> 1  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 1  ;  (is_even([s(z)])) -> BOT -> 1  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003450 s (model generation: 0.003435,  model checking: 0.000015):

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

}

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

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

}
--
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, _sy])) -> is_even([_sy]) -> 1  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 1  ;  (is_even([s(z)])) -> BOT -> 1  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 1
}
Sat witness: Yes: (() -> is_even([z]), {

})

-------------------------------------------
Step 2, which took 0.003448 s (model generation: 0.003388,  model checking: 0.000060):

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

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

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

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

-------------------------------------------
Step 3, which took 0.003802 s (model generation: 0.003717,  model checking: 0.000085):

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

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

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

}
--
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, _sy])) -> is_even([_sy]) -> 2  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 2  ;  (is_even([s(z)])) -> BOT -> 2  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 4
}
Sat witness: Yes: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 4, which took 0.004542 s (model generation: 0.004527,  model checking: 0.000015):

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

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

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

}
--
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, _sy])) -> is_even([_sy]) -> 2  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 2  ;  (is_even([s(z)])) -> BOT -> 5  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 4
}
Sat witness: Yes: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.004475 s (model generation: 0.004277,  model checking: 0.000198):

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

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

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

}
--
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, _sy])) -> is_even([_sy]) -> 3  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 3  ;  (is_even([s(z)])) -> BOT -> 5  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 6, which took 0.008649 s (model generation: 0.008355,  model checking: 0.000294):

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

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

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

}
--
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, _sy])) -> is_even([_sy]) -> 4  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 4  ;  (is_even([s(z)])) -> BOT -> 5  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.007231 s (model generation: 0.007132,  model checking: 0.000099):

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

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

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

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

-------------------------------------------
Step 8, which took 0.007546 s (model generation: 0.005476,  model checking: 0.002070):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<z, z>() -> q_gen_4887
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 9, which took 0.013857 s (model generation: 0.013023,  model checking: 0.000834):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 10, which took 0.014716 s (model generation: 0.013523,  model checking: 0.001193):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, s>(q_gen_4893) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s, s>(q_gen_4884) -> q_gen_4884
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 11, which took 0.011406 s (model generation: 0.010780,  model checking: 0.000626):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4898},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s>(q_gen_4898) -> q_gen_4898
<z, s>(q_gen_4893) -> q_gen_4898
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<s, z, s>(q_gen_4898) -> q_gen_4892
<z, s, s>(q_gen_4898) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 12, which took 0.010961 s (model generation: 0.010812,  model checking: 0.000149):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4895},
Q_f={q_gen_4884},
Delta=
{
<s>(q_gen_4893) -> q_gen_4893
<z>() -> q_gen_4893
<z, z>() -> q_gen_4887
<s, s>(q_gen_4887) -> q_gen_4895
<s, s>(q_gen_4895) -> q_gen_4895
<z, s>(q_gen_4893) -> q_gen_4895
<s, s, s>(q_gen_4884) -> q_gen_4884
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<s, z, s>(q_gen_4895) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, s, s>(q_gen_4895) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 13, which took 0.015972 s (model generation: 0.015848,  model checking: 0.000124):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893},
Q_f={q_gen_4884},
Delta=
{
<s>(q_gen_4893) -> q_gen_4893
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, s>(q_gen_4893) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s, s>(q_gen_4884) -> q_gen_4884
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 14, which took 0.012401 s (model generation: 0.012337,  model checking: 0.000064):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893},
Q_f={q_gen_4884},
Delta=
{
<s>(q_gen_4893) -> q_gen_4893
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, s>(q_gen_4893) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s, s>(q_gen_4884) -> q_gen_4884
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

}
--
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))]) -> 12  ;  (is_even([x]) /\ is_even([y]) /\ plus([x, y, _sy])) -> is_even([_sy]) -> 13  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 13  ;  (is_even([s(z)])) -> BOT -> 11  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 13
}
Sat witness: Yes: ((is_even([s(s(n3))])) -> is_even([n3]), {
n3 -> s(z)
})

-------------------------------------------
Step 15, which took 0.018152 s (model generation: 0.016684,  model checking: 0.001468):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4898},
Q_f={q_gen_4884},
Delta=
{
<s>(q_gen_4893) -> q_gen_4893
<z>() -> q_gen_4893
<s, s>(q_gen_4887) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s>(q_gen_4898) -> q_gen_4898
<z, s>(q_gen_4893) -> q_gen_4898
<s, s, s>(q_gen_4884) -> q_gen_4884
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<s, z, s>(q_gen_4898) -> q_gen_4892
<z, s, s>(q_gen_4898) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

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

-------------------------------------------
Step 16, which took 0.014645 s (model generation: 0.013944,  model checking: 0.000701):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4898, q_gen_4905},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<s>(q_gen_4893) -> q_gen_4905
<s, s>(q_gen_4887) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s>(q_gen_4898) -> q_gen_4898
<z, s>(q_gen_4893) -> q_gen_4898
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, s>(q_gen_4905) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<s, s, s>(q_gen_4884) -> q_gen_4892
<s, z, s>(q_gen_4898) -> q_gen_4892
<z, s, s>(q_gen_4898) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 12  ;  () -> plus([n, z, n]) -> 12  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 14  ;  (is_even([x]) /\ is_even([y]) /\ plus([x, y, _sy])) -> is_even([_sy]) -> 16  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 14  ;  (is_even([s(z)])) -> BOT -> 13  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 17
}
Sat witness: Yes: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(s(z))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 17, which took 0.014410 s (model generation: 0.011928,  model checking: 0.002482):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4884, q_gen_4887, q_gen_4892, q_gen_4893, q_gen_4898, q_gen_4905},
Q_f={q_gen_4884},
Delta=
{
<z>() -> q_gen_4893
<s>(q_gen_4893) -> q_gen_4905
<s, s>(q_gen_4887) -> q_gen_4887
<z, s>(q_gen_4905) -> q_gen_4887
<z, z>() -> q_gen_4887
<s, s>(q_gen_4898) -> q_gen_4898
<z, s>(q_gen_4893) -> q_gen_4898
<s, s, s>(q_gen_4892) -> q_gen_4884
<s, z, s>(q_gen_4887) -> q_gen_4884
<z, s, s>(q_gen_4887) -> q_gen_4884
<z, z, s>(q_gen_4905) -> q_gen_4884
<z, z, z>() -> q_gen_4884
<s, s, s>(q_gen_4884) -> q_gen_4892
<s, z, s>(q_gen_4898) -> q_gen_4892
<z, s, s>(q_gen_4898) -> q_gen_4892
<z, z, s>(q_gen_4893) -> q_gen_4892
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 13  ;  () -> plus([n, z, n]) -> 13  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 15  ;  (is_even([x]) /\ is_even([y]) /\ plus([x, y, _sy])) -> is_even([_sy]) -> 17  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 15  ;  (is_even([s(z)])) -> BOT -> 14  ;  (plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 20
}
Sat witness: Yes: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.198742
Reason for stopping: Proved