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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(is_even, P:
{() -> is_even([z])
(is_even([n3])) -> is_even([s(s(n3))])
(is_even([s(s(n3))])) -> is_even([n3])
(is_even([s(z)])) -> BOT}
)
(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.146913 seconds.
Proved
Model:
|_
{
is_even -> 
{{{
Q={q_gen_4807, q_gen_4811},
Q_f={q_gen_4807},
Delta=
{
<s>(q_gen_4811) -> q_gen_4807
<z>() -> q_gen_4807
<s>(q_gen_4807) -> q_gen_4811
}

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820, q_gen_4830},
Q_f={q_gen_4806},
Delta=
{
<s>(q_gen_4830) -> q_gen_4817
<z>() -> q_gen_4817
<s>(q_gen_4817) -> q_gen_4830
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4830) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, s>(q_gen_4830) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, s, s>(q_gen_4806) -> q_gen_4816
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, s, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006446 s (model generation: 0.005975,  model checking: 0.000471):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> is_even([z]) -> 0
() -> 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: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.004649 s (model generation: 0.004583,  model checking: 0.000066):

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

}

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

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

}
--
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: Found: (() -> is_even([z]), {

})

-------------------------------------------
Step 2, which took 0.005057 s (model generation: 0.004781,  model checking: 0.000276):

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

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

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

}
--
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: Found: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.005953 s (model generation: 0.005618,  model checking: 0.000335):

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

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

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

}
--
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: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 4, which took 0.004667 s (model generation: 0.004618,  model checking: 0.000049):

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

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

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

}
--
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: Found: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.004862 s (model generation: 0.004316,  model checking: 0.000546):

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

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

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 6, which took 0.006651 s (model generation: 0.005896,  model checking: 0.000755):

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

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

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

}
--
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: Found: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.005957 s (model generation: 0.005677,  model checking: 0.000280):

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

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

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

}
--
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: Found: ((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.007485 s (model generation: 0.006504,  model checking: 0.000981):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

}
--
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, _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)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.006188 s (model generation: 0.006001,  model checking: 0.000187):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4817) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s, s>(q_gen_4806) -> q_gen_4806
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

}
--
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, _sy])) -> is_even([_sy]) -> 10
(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: Found: ((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 10, which took 0.006984 s (model generation: 0.006412,  model checking: 0.000572):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4817) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s, s>(q_gen_4806) -> q_gen_4806
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

}
--
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, _sy])) -> is_even([_sy]) -> 10
(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: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> s(s(z))
})

-------------------------------------------
Step 11, which took 0.007639 s (model generation: 0.007343,  model checking: 0.000296):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4817) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s, s>(q_gen_4806) -> q_gen_4806
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

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

-------------------------------------------
Step 12, which took 0.008533 s (model generation: 0.007599,  model checking: 0.000934):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

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

-------------------------------------------
Step 13, which took 0.008362 s (model generation: 0.007542,  model checking: 0.000820):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, s, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

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

-------------------------------------------
Step 14, which took 0.009942 s (model generation: 0.009195,  model checking: 0.000747):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820},
Q_f={q_gen_4806},
Delta=
{
<s>(q_gen_4817) -> q_gen_4817
<z>() -> q_gen_4817
<s, s>(q_gen_4809) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4806) -> q_gen_4806
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, s, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

}
--
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, _sy])) -> is_even([_sy]) -> 14
(is_even([s(s(n3))])) -> is_even([n3]) -> 12
(is_even([s(z)])) -> BOT -> 11
(plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 16
}
Sat witness: Found: ((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 15, which took 0.010006 s (model generation: 0.009836,  model checking: 0.000170):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4813, q_gen_4814, q_gen_4817, q_gen_4830},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s>(q_gen_4817) -> q_gen_4830
<s, s>(q_gen_4813) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4809) -> q_gen_4813
<z, s>(q_gen_4817) -> q_gen_4813
<s, s, s>(q_gen_4806) -> q_gen_4806
<s, z, s>(q_gen_4813) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, s>(q_gen_4830) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, s, s>(q_gen_4814) -> q_gen_4814
<s, z, s>(q_gen_4809) -> q_gen_4814
<z, s, s>(q_gen_4813) -> q_gen_4814
<z, z, s>(q_gen_4817) -> q_gen_4814
}

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

}
--
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, _sy])) -> is_even([_sy]) -> 14
(is_even([s(s(n3))])) -> is_even([n3]) -> 12
(is_even([s(z)])) -> BOT -> 11
(plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]) -> 16
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 16, which took 0.012050 s (model generation: 0.011238,  model checking: 0.000812):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820, q_gen_4830},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s>(q_gen_4817) -> q_gen_4830
<s, s>(q_gen_4809) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, s>(q_gen_4830) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, s, s>(q_gen_4806) -> q_gen_4816
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, s, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

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

-------------------------------------------
Step 17, which took 0.011737 s (model generation: 0.010909,  model checking: 0.000828):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4806, q_gen_4809, q_gen_4816, q_gen_4817, q_gen_4820, q_gen_4830},
Q_f={q_gen_4806},
Delta=
{
<z>() -> q_gen_4817
<s>(q_gen_4817) -> q_gen_4830
<s, s>(q_gen_4809) -> q_gen_4809
<z, s>(q_gen_4830) -> q_gen_4809
<z, z>() -> q_gen_4809
<s, s>(q_gen_4820) -> q_gen_4820
<z, s>(q_gen_4817) -> q_gen_4820
<s, s, s>(q_gen_4816) -> q_gen_4806
<s, z, s>(q_gen_4809) -> q_gen_4806
<z, s, s>(q_gen_4809) -> q_gen_4806
<z, z, s>(q_gen_4830) -> q_gen_4806
<z, z, z>() -> q_gen_4806
<s, s, s>(q_gen_4806) -> q_gen_4816
<s, z, s>(q_gen_4820) -> q_gen_4816
<z, s, s>(q_gen_4820) -> q_gen_4816
<z, z, s>(q_gen_4817) -> q_gen_4816
}

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

}
--
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, _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)]) -> 22
}
Sat witness: Found: ((plus([n, mm, _ny])) -> plus([n, s(mm), s(_ny)]), {
_ny -> s(s(s(z)))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.146913
Reason for stopping: Proved