Solving ../../benchmarks/true/nat_double_is_even.smt2...

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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(double, F:
{() -> double([z, z])
(double([nn, _of])) -> double([s(nn), s(s(_of))])}
(double([_pf, _qf]) /\ double([_pf, _rf])) -> eq_nat([_qf, _rf])
)
(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}
)
}

properties:
{(double([n, _sf])) -> is_even([_sf])}


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

Clause system for inference is:

{
() -> double([z, z]) -> 0  ;  () -> is_even([z]) -> 0  ;  (double([n, _sf])) -> is_even([_sf]) -> 0  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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
}


Solving took 0.100541 seconds.
Proved
Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4715, q_gen_4716, q_gen_4721},
Q_f={q_gen_4711},
Delta=
{
<s>(q_gen_4721) -> q_gen_4716
<z>() -> q_gen_4716
<s>(q_gen_4716) -> q_gen_4721
<s, s>(q_gen_4715) -> q_gen_4711
<z, s>(q_gen_4721) -> q_gen_4711
<z, z>() -> q_gen_4711
<s, s>(q_gen_4711) -> q_gen_4715
<z, s>(q_gen_4716) -> q_gen_4715
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003465 s (model generation: 0.003422,  model checking: 0.000043):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 0  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 1  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 1  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 1  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 1  ;  (is_even([s(z)])) -> BOT -> 1
}
Sat witness: Yes: (() -> is_even([z]), {

})

-------------------------------------------
Step 1, which took 0.004337 s (model generation: 0.004291,  model checking: 0.000046):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 1  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 1  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 1  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 1  ;  (is_even([s(z)])) -> BOT -> 1
}
Sat witness: Yes: (() -> double([z, z]), {

})

-------------------------------------------
Step 2, which took 0.005916 s (model generation: 0.005852,  model checking: 0.000064):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 1  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 1  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 4  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 2  ;  (is_even([s(z)])) -> BOT -> 2
}
Sat witness: Yes: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 3, which took 0.006477 s (model generation: 0.006382,  model checking: 0.000095):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 1  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 4  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 4  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 2  ;  (is_even([s(z)])) -> BOT -> 2
}
Sat witness: Yes: ((double([nn, _of])) -> double([s(nn), s(s(_of))]), {
_of -> z  ;  nn -> z
})

-------------------------------------------
Step 4, which took 0.010520 s (model generation: 0.010449,  model checking: 0.000071):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4716},
Q_f={q_gen_4711},
Delta=
{
<z>() -> q_gen_4716
<s, s>(q_gen_4711) -> q_gen_4711
<z, s>(q_gen_4716) -> q_gen_4711
<z, z>() -> q_gen_4711
}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 2  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 4  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 4  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 2  ;  (is_even([s(z)])) -> BOT -> 5
}
Sat witness: Yes: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.011337 s (model generation: 0.011269,  model checking: 0.000068):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4716},
Q_f={q_gen_4711},
Delta=
{
<z>() -> q_gen_4716
<s, s>(q_gen_4711) -> q_gen_4711
<z, s>(q_gen_4716) -> q_gen_4711
<z, z>() -> q_gen_4711
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3  ;  () -> is_even([z]) -> 3  ;  (double([n, _sf])) -> is_even([_sf]) -> 5  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 4  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 4  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 3  ;  (is_even([s(z)])) -> BOT -> 5
}
Sat witness: Yes: ((double([n, _sf])) -> is_even([_sf]), {
_sf -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 6, which took 0.012566 s (model generation: 0.007204,  model checking: 0.005362):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4715, q_gen_4716},
Q_f={q_gen_4711},
Delta=
{
<z>() -> q_gen_4716
<s, s>(q_gen_4715) -> q_gen_4711
<z, z>() -> q_gen_4711
<s, s>(q_gen_4711) -> q_gen_4715
<z, s>(q_gen_4716) -> q_gen_4715
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 4  ;  () -> is_even([z]) -> 4  ;  (double([n, _sf])) -> is_even([_sf]) -> 5  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 7  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 5  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 4  ;  (is_even([s(z)])) -> BOT -> 5
}
Sat witness: Yes: ((double([nn, _of])) -> double([s(nn), s(s(_of))]), {
_of -> s(s(z))  ;  nn -> s(z)
})

-------------------------------------------
Step 7, which took 0.014133 s (model generation: 0.013192,  model checking: 0.000941):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4715, q_gen_4716, q_gen_4721},
Q_f={q_gen_4711},
Delta=
{
<z>() -> q_gen_4716
<s>(q_gen_4716) -> q_gen_4721
<s, s>(q_gen_4715) -> q_gen_4711
<z, s>(q_gen_4721) -> q_gen_4711
<z, z>() -> q_gen_4711
<s, s>(q_gen_4711) -> q_gen_4715
<z, s>(q_gen_4716) -> q_gen_4715
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 5  ;  () -> is_even([z]) -> 5  ;  (double([n, _sf])) -> is_even([_sf]) -> 6  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 10  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 6  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 5  ;  (is_even([s(z)])) -> BOT -> 6
}
Sat witness: Yes: ((double([nn, _of])) -> double([s(nn), s(s(_of))]), {
_of -> s(s(z))  ;  nn -> z
})

-------------------------------------------
Step 8, which took 0.009344 s (model generation: 0.009228,  model checking: 0.000116):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4714, q_gen_4716, q_gen_4717},
Q_f={q_gen_4711, q_gen_4714},
Delta=
{
<s>(q_gen_4716) -> q_gen_4716
<z>() -> q_gen_4716
<z, z>() -> q_gen_4711
<s, s>(q_gen_4714) -> q_gen_4714
<z, s>(q_gen_4716) -> q_gen_4714
<s, s>(q_gen_4711) -> q_gen_4717
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 6  ;  () -> is_even([z]) -> 6  ;  (double([n, _sf])) -> is_even([_sf]) -> 9  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 10  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 7  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 6  ;  (is_even([s(z)])) -> BOT -> 7
}
Sat witness: Yes: ((double([n, _sf])) -> is_even([_sf]), {
_sf -> s(z)  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.007912 s (model generation: 0.007516,  model checking: 0.000396):

Model:
|_
{
double -> 
{{{
Q={q_gen_4711, q_gen_4714, q_gen_4715, q_gen_4716},
Q_f={q_gen_4711, q_gen_4714},
Delta=
{
<s>(q_gen_4716) -> q_gen_4716
<z>() -> q_gen_4716
<z, z>() -> q_gen_4711
<s, s>(q_gen_4714) -> q_gen_4714
<s, s>(q_gen_4715) -> q_gen_4714
<s, s>(q_gen_4711) -> q_gen_4715
<z, s>(q_gen_4716) -> q_gen_4715
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  is_even -> 
{{{
Q={q_gen_4710, q_gen_4713},
Q_f={q_gen_4710},
Delta=
{
<s>(q_gen_4713) -> q_gen_4710
<z>() -> q_gen_4710
<s>(q_gen_4710) -> q_gen_4713
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 7  ;  () -> is_even([z]) -> 7  ;  (double([n, _sf])) -> is_even([_sf]) -> 12  ;  (double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 10  ;  (is_even([n3])) -> is_even([s(s(n3))]) -> 8  ;  (is_even([s(s(n3))])) -> is_even([n3]) -> 7  ;  (is_even([s(z)])) -> BOT -> 8
}
Sat witness: Yes: ((double([n, _sf])) -> is_even([_sf]), {
_sf -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

Total time: 0.100541
Reason for stopping: Proved