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, _sc])) -> plus([n, s(mm), s(_sc)])}
(plus([_tc, _uc, _vc]) /\ plus([_tc, _uc, _wc])) -> eq_nat([_vc, _wc])
)
}

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


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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 0
(plus([x, x, _xc])) -> is_even([_xc]) -> 0
}


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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710, q_gen_714, q_gen_730},
Q_f={q_gen_699},
Delta=
{
<s>(q_gen_730) -> q_gen_710
<z>() -> q_gen_710
<s>(q_gen_710) -> q_gen_730
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_730) -> q_gen_702
<z, z>() -> q_gen_702
<s, s>(q_gen_714) -> q_gen_714
<z, s>(q_gen_710) -> q_gen_714
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, s>(q_gen_730) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<s, z, s>(q_gen_714) -> q_gen_709
<z, s, s>(q_gen_714) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006962 s (model generation: 0.006821,  model checking: 0.000141):

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

-------------------------------------------
Step 1, which took 0.007320 s (model generation: 0.007291,  model checking: 0.000029):

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

}

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

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

})

-------------------------------------------
Step 2, which took 0.008245 s (model generation: 0.008134,  model checking: 0.000111):

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

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

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

-------------------------------------------
Step 3, which took 0.010605 s (model generation: 0.010524,  model checking: 0.000081):

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

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

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

-------------------------------------------
Step 4, which took 0.008614 s (model generation: 0.008579,  model checking: 0.000035):

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

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

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

})

-------------------------------------------
Step 5, which took 0.008205 s (model generation: 0.008041,  model checking: 0.000164):

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

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

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

-------------------------------------------
Step 6, which took 0.008239 s (model generation: 0.008036,  model checking: 0.000203):

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

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

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

-------------------------------------------
Step 7, which took 0.009285 s (model generation: 0.008815,  model checking: 0.000470):

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

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

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 7
(plus([x, x, _xc])) -> is_even([_xc]) -> 8
}
Sat witness: Found: ((plus([x, x, _xc])) -> is_even([_xc]), {
_xc -> s(z)  ;  x -> s(z)
})

-------------------------------------------
Step 8, which took 0.010187 s (model generation: 0.009693,  model checking: 0.000494):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, z>() -> q_gen_702
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

-------------------------------------------
Step 9, which took 0.010511 s (model generation: 0.010124,  model checking: 0.000387):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_710, q_gen_711},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_701) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<z, z, s>(q_gen_710) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_711
}

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]) -> 8
(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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 10
(plus([x, x, _xc])) -> is_even([_xc]) -> 11
}
Sat witness: Found: ((plus([x, x, _xc])) -> is_even([_xc]), {
_xc -> s(z)  ;  x -> z
})

-------------------------------------------
Step 10, which took 0.010844 s (model generation: 0.010464,  model checking: 0.000380):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<s, s, s>(q_gen_701) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_709) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 13
(plus([x, x, _xc])) -> is_even([_xc]) -> 11
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(z))  ;  mm -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 11, which took 0.016758 s (model generation: 0.016260,  model checking: 0.000498):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<s, s, s>(q_gen_709) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_701) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 16
(plus([x, x, _xc])) -> is_even([_xc]) -> 12
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.015571 s (model generation: 0.014898,  model checking: 0.000673):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_701) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 19
(plus([x, x, _xc])) -> is_even([_xc]) -> 13
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.016589 s (model generation: 0.016237,  model checking: 0.000352):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_701) -> q_gen_701
<s, s, s>(q_gen_709) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 19
(plus([x, x, _xc])) -> is_even([_xc]) -> 16
}
Sat witness: Found: ((plus([x, x, _xc])) -> is_even([_xc]), {
_xc -> s(s(s(z)))  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 14, which took 0.018377 s (model generation: 0.017618,  model checking: 0.000759):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710, q_gen_714},
Q_f={q_gen_699},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, z>() -> q_gen_702
<z, s>(q_gen_710) -> q_gen_714
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<s, z, s>(q_gen_714) -> q_gen_709
<z, s, s>(q_gen_714) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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]) -> 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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 22
(plus([x, x, _xc])) -> is_even([_xc]) -> 17
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(s(z)))  ;  mm -> s(s(z))  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.020103 s (model generation: 0.019347,  model checking: 0.000756):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710, q_gen_714},
Q_f={q_gen_699},
Delta=
{
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, z>() -> q_gen_702
<s, s>(q_gen_714) -> q_gen_714
<z, s>(q_gen_710) -> q_gen_714
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<s, z, s>(q_gen_714) -> q_gen_709
<z, s, s>(q_gen_714) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

}
--
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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 25
(plus([x, x, _xc])) -> is_even([_xc]) -> 18
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 16, which took 0.025428 s (model generation: 0.025330,  model checking: 0.000098):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<s>(q_gen_710) -> q_gen_710
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_701) -> q_gen_701
<s, s, s>(q_gen_709) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<s, s, s>(q_gen_699) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

}
--
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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 25
(plus([x, x, _xc])) -> is_even([_xc]) -> 18
}
Sat witness: Found: ((is_even([s(s(n3))])) -> is_even([n3]), {
n3 -> s(z)
})

-------------------------------------------
Step 17, which took 0.025558 s (model generation: 0.024680,  model checking: 0.000878):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710, q_gen_714, q_gen_730},
Q_f={q_gen_699},
Delta=
{
<z>() -> q_gen_710
<s>(q_gen_710) -> q_gen_730
<s, s>(q_gen_702) -> q_gen_702
<z, z>() -> q_gen_702
<s, s>(q_gen_714) -> q_gen_714
<z, s>(q_gen_710) -> q_gen_714
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, s>(q_gen_730) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<s, z, s>(q_gen_714) -> q_gen_709
<z, s, s>(q_gen_714) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

}
--
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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 28
(plus([x, x, _xc])) -> is_even([_xc]) -> 19
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(z))  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 18, which took 0.028934 s (model generation: 0.028660,  model checking: 0.000274):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_701, q_gen_702, q_gen_709, q_gen_710, q_gen_711},
Q_f={q_gen_699, q_gen_701},
Delta=
{
<s>(q_gen_710) -> q_gen_710
<z>() -> q_gen_710
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<s, s, s>(q_gen_701) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_709) -> q_gen_701
<s, z, s>(q_gen_702) -> q_gen_701
<z, s, s>(q_gen_702) -> q_gen_701
<z, z, s>(q_gen_710) -> q_gen_709
<s, s, s>(q_gen_699) -> q_gen_711
<s, s, s>(q_gen_711) -> q_gen_711
}

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

}
--
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, _sc])) -> plus([n, s(mm), s(_sc)]) -> 28
(plus([x, x, _xc])) -> is_even([_xc]) -> 22
}
Sat witness: Found: ((plus([x, x, _xc])) -> is_even([_xc]), {
_xc -> s(s(s(z)))  ;  x -> s(z)
})

-------------------------------------------
Step 19, which took 0.025569 s (model generation: 0.025398,  model checking: 0.000171):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_706, q_gen_707, q_gen_709, q_gen_710},
Q_f={q_gen_699},
Delta=
{
<s>(q_gen_710) -> q_gen_710
<z>() -> q_gen_710
<z, s>(q_gen_710) -> q_gen_702
<z, z>() -> q_gen_702
<s, s>(q_gen_702) -> q_gen_706
<s, s, s>(q_gen_707) -> q_gen_699
<s, z, s>(q_gen_706) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_706) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_707
<s, s, s>(q_gen_709) -> q_gen_707
<s, z, s>(q_gen_702) -> q_gen_707
<z, z, s>(q_gen_710) -> q_gen_709
}

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

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

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

-------------------------------------------
Step 20, which took 0.027454 s (model generation: 0.026391,  model checking: 0.001063):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_699, q_gen_702, q_gen_709, q_gen_710, q_gen_714, q_gen_730},
Q_f={q_gen_699},
Delta=
{
<z>() -> q_gen_710
<s>(q_gen_710) -> q_gen_730
<s, s>(q_gen_702) -> q_gen_702
<z, s>(q_gen_730) -> q_gen_702
<z, z>() -> q_gen_702
<s, s>(q_gen_714) -> q_gen_714
<z, s>(q_gen_710) -> q_gen_714
<s, s, s>(q_gen_709) -> q_gen_699
<s, z, s>(q_gen_702) -> q_gen_699
<z, s, s>(q_gen_702) -> q_gen_699
<z, z, s>(q_gen_730) -> q_gen_699
<z, z, z>() -> q_gen_699
<s, s, s>(q_gen_699) -> q_gen_709
<s, z, s>(q_gen_714) -> q_gen_709
<z, s, s>(q_gen_714) -> q_gen_709
<z, z, s>(q_gen_710) -> q_gen_709
}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 17
() -> plus([n, z, n]) -> 20
(is_even([n3])) -> is_even([s(s(n3))]) -> 17
(is_even([s(s(n3))])) -> is_even([n3]) -> 19
(is_even([s(z)])) -> BOT -> 18
(plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]) -> 31
(plus([x, x, _xc])) -> is_even([_xc]) -> 23
}
Sat witness: Found: ((plus([n, mm, _sc])) -> plus([n, s(mm), s(_sc)]), {
_sc -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.352972
Reason for stopping: Proved