Solving ../../benchmarks/true/timbuk_plus_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, _gg])) -> plus([n, s(mm), s(_gg)])}
(plus([_hg, _ig, _jg]) /\ plus([_hg, _ig, _kg])) -> eq_nat([_jg, _kg])
)
}

properties:
{(plus([x, x, _lg])) -> is_even([_lg])}


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

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


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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305, q_gen_6314},
Q_f={q_gen_6290},
Delta=
{
<s>(q_gen_6314) -> q_gen_6299
<z>() -> q_gen_6299
<s>(q_gen_6299) -> q_gen_6314
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6314) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s>(q_gen_6305) -> q_gen_6305
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, s>(q_gen_6314) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<s, z, s>(q_gen_6305) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004076 s (model generation: 0.003979,  model checking: 0.000097):

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

-------------------------------------------
Step 1, which took 0.003474 s (model generation: 0.003458,  model checking: 0.000016):

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

}

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

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

})

-------------------------------------------
Step 2, which took 0.003634 s (model generation: 0.003350,  model checking: 0.000284):

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

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

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

-------------------------------------------
Step 3, which took 0.003431 s (model generation: 0.003391,  model checking: 0.000040):

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

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

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

-------------------------------------------
Step 4, which took 0.003655 s (model generation: 0.003627,  model checking: 0.000028):

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

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

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

})

-------------------------------------------
Step 5, which took 0.004986 s (model generation: 0.004710,  model checking: 0.000276):

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

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

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

-------------------------------------------
Step 6, which took 0.006414 s (model generation: 0.006187,  model checking: 0.000227):

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

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

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

-------------------------------------------
Step 7, which took 0.007007 s (model generation: 0.006844,  model checking: 0.000163):

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

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

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]) -> 6  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 5  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 5  ;  (is_even([s(z)])) -> BOT -> 5  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 7  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 8
}
Sat witness: Yes: ((plus([x, x, _lg])) -> is_even([_lg]), {
_lg -> s(z)  ;  x -> s(z)
})

-------------------------------------------
Step 8, which took 0.009883 s (model generation: 0.009702,  model checking: 0.000181):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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([s(s(n3))])) -> is_even([n3]) -> 6  ;  (is_even([s(z)])) -> BOT -> 6  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 7  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 8
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.008442 s (model generation: 0.008061,  model checking: 0.000381):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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([s(s(n3))])) -> is_even([n3]) -> 7  ;  (is_even([s(z)])) -> BOT -> 7  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 10  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 8
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.008962 s (model generation: 0.008818,  model checking: 0.000144):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6292, q_gen_6293, q_gen_6299, q_gen_6300},
Q_f={q_gen_6290, q_gen_6292},
Delta=
{
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6293
<z, z>() -> q_gen_6293
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6292) -> q_gen_6292
<s, z, s>(q_gen_6293) -> q_gen_6292
<z, s, s>(q_gen_6293) -> q_gen_6292
<z, z, s>(q_gen_6299) -> q_gen_6292
<s, s, s>(q_gen_6290) -> q_gen_6300
}

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]) -> 9  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 8  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 8  ;  (is_even([s(z)])) -> BOT -> 8  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 10  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 11
}
Sat witness: Yes: ((plus([x, x, _lg])) -> is_even([_lg]), {
_lg -> s(z)  ;  x -> z
})

-------------------------------------------
Step 11, which took 0.008538 s (model generation: 0.007688,  model checking: 0.000850):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, z>() -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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([s(s(n3))])) -> is_even([n3]) -> 9  ;  (is_even([s(z)])) -> BOT -> 9  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 13  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 11
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.006420 s (model generation: 0.005786,  model checking: 0.000634):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, z>() -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<s, z, s>(q_gen_6305) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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]) -> 11  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 10  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 10  ;  (is_even([s(z)])) -> BOT -> 10  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 16  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 12
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.006612 s (model generation: 0.006013,  model checking: 0.000599):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s>(q_gen_6305) -> q_gen_6305
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<s, z, s>(q_gen_6305) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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

-------------------------------------------
Step 14, which took 0.007510 s (model generation: 0.007273,  model checking: 0.000237):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6292, q_gen_6293, q_gen_6298, q_gen_6299},
Q_f={q_gen_6290, q_gen_6292},
Delta=
{
<s>(q_gen_6299) -> q_gen_6299
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6292) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6298) -> q_gen_6292
<s, z, s>(q_gen_6293) -> q_gen_6292
<z, s, s>(q_gen_6293) -> q_gen_6292
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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]) -> 13  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 12  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 12  ;  (is_even([s(z)])) -> BOT -> 12  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 19  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 16
}
Sat witness: Yes: ((plus([x, x, _lg])) -> is_even([_lg]), {
_lg -> s(s(s(z)))  ;  x -> s(z)
})

-------------------------------------------
Step 15, which took 0.008524 s (model generation: 0.007811,  model checking: 0.000713):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305, q_gen_6314},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s>(q_gen_6299) -> q_gen_6314
<s, s>(q_gen_6293) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s>(q_gen_6305) -> q_gen_6305
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, s>(q_gen_6314) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<s, z, s>(q_gen_6305) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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]) -> 14  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 13  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 13  ;  (is_even([s(z)])) -> BOT -> 13  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 22  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 17
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(z))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 16, which took 0.007919 s (model generation: 0.007852,  model checking: 0.000067):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6292, q_gen_6293, q_gen_6298, q_gen_6299},
Q_f={q_gen_6290, q_gen_6292},
Delta=
{
<s>(q_gen_6299) -> q_gen_6299
<z>() -> q_gen_6299
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6292) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6298) -> q_gen_6292
<s, z, s>(q_gen_6293) -> q_gen_6292
<z, s, s>(q_gen_6293) -> q_gen_6292
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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]) -> 14  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 13  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 16  ;  (is_even([s(z)])) -> BOT -> 14  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 22  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 17
}
Sat witness: Yes: ((is_even([s(s(n3))])) -> is_even([n3]), {
n3 -> s(z)
})

-------------------------------------------
Step 17, which took 0.008696 s (model generation: 0.008279,  model checking: 0.000417):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6292, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6314},
Q_f={q_gen_6290, q_gen_6292},
Delta=
{
<z>() -> q_gen_6299
<s>(q_gen_6299) -> q_gen_6314
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6293
<z, s>(q_gen_6314) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6292) -> q_gen_6290
<z, z, s>(q_gen_6314) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6298) -> q_gen_6292
<s, z, s>(q_gen_6293) -> q_gen_6292
<z, s, s>(q_gen_6293) -> q_gen_6292
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 14  ;  () -> plus([n, z, n]) -> 15  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 14  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 17  ;  (is_even([s(z)])) -> BOT -> 15  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 22  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 20
}
Sat witness: Yes: ((plus([x, x, _lg])) -> is_even([_lg]), {
_lg -> s(s(s(s(s(z)))))  ;  x -> s(s(s(s(s(z)))))
})

-------------------------------------------
Step 18, which took 0.015497 s (model generation: 0.015120,  model checking: 0.000377):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6292, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6314},
Q_f={q_gen_6290, q_gen_6292},
Delta=
{
<z>() -> q_gen_6299
<s>(q_gen_6299) -> q_gen_6314
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6299) -> q_gen_6293
<z, s>(q_gen_6314) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s, s>(q_gen_6292) -> q_gen_6290
<s, s, s>(q_gen_6298) -> q_gen_6290
<z, z, s>(q_gen_6314) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6292
<z, s, s>(q_gen_6293) -> q_gen_6292
<s, s, s>(q_gen_6290) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 15  ;  () -> plus([n, z, n]) -> 16  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 15  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 18  ;  (is_even([s(z)])) -> BOT -> 16  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 25  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 21
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 19, which took 0.013710 s (model generation: 0.012866,  model checking: 0.000844):

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

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6290, q_gen_6293, q_gen_6298, q_gen_6299, q_gen_6305, q_gen_6314},
Q_f={q_gen_6290},
Delta=
{
<z>() -> q_gen_6299
<s>(q_gen_6299) -> q_gen_6314
<s, s>(q_gen_6293) -> q_gen_6293
<z, s>(q_gen_6314) -> q_gen_6293
<z, z>() -> q_gen_6293
<s, s>(q_gen_6305) -> q_gen_6305
<z, s>(q_gen_6299) -> q_gen_6305
<s, s, s>(q_gen_6298) -> q_gen_6290
<s, z, s>(q_gen_6293) -> q_gen_6290
<z, s, s>(q_gen_6293) -> q_gen_6290
<z, z, s>(q_gen_6314) -> q_gen_6290
<z, z, z>() -> q_gen_6290
<s, s, s>(q_gen_6290) -> q_gen_6298
<s, z, s>(q_gen_6305) -> q_gen_6298
<z, s, s>(q_gen_6305) -> q_gen_6298
<z, z, s>(q_gen_6299) -> q_gen_6298
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 16  ;  () -> plus([n, z, n]) -> 17  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 16  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 19  ;  (is_even([s(z)])) -> BOT -> 17  ;  (plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]) -> 28  ;  (plus([x, x, _lg])) -> is_even([_lg]) -> 22
}
Sat witness: Yes: ((plus([n, mm, _gg])) -> plus([n, s(mm), s(_gg)]), {
_gg -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.163870
Reason for stopping: Proved