Solving ../../benchmarks/false/plus_even_implies.smt2...

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, _lia])) -> plus([n, s(mm), s(_lia)])}
(plus([_mia, _nia, _oia]) /\ plus([_mia, _nia, _pia])) -> eq_nat([_oia, _pia])
)
}

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


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

Clause system for inference is:

{
() -> is_even([z]) -> 0
() -> plus([n, z, n]) -> 0
(is_even([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 0
}


Solving took 0.251298 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.016611 s (model generation: 0.016298,  model checking: 0.000313):

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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
(plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.016411 s (model generation: 0.016354,  model checking: 0.000057):

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

}

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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
(plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]) -> 1
}
Sat witness: Found: (() -> is_even([z]), {

})

-------------------------------------------
Step 2, which took 0.017296 s (model generation: 0.017087,  model checking: 0.000209):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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
(plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]), {
_lia -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.017973 s (model generation: 0.017744,  model checking: 0.000229):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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
(plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]) -> 4
}
Sat witness: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 4, which took 0.018150 s (model generation: 0.018081,  model checking: 0.000069):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 2
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 4
}
Sat witness: Found: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.018813 s (model generation: 0.018436,  model checking: 0.000377):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 3
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 6, which took 0.025675 s (model generation: 0.018540,  model checking: 0.007135):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 4
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]), {
_lia -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.022478 s (model generation: 0.022005,  model checking: 0.000473):

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

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

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 7
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 7
}
Sat witness: Found: ((is_even([_qia]) /\ plus([x, y, _qia])) -> is_even([x]), {
_qia -> s(s(z))  ;  x -> s(z)  ;  y -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.024330 s (model generation: 0.021719,  model checking: 0.002611):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_8883, q_gen_8886, q_gen_8893, q_gen_8894},
Q_f={q_gen_8883},
Delta=
{
<z>() -> q_gen_8894
<s, s>(q_gen_8886) -> q_gen_8886
<z, z>() -> q_gen_8886
<s, s, s>(q_gen_8893) -> q_gen_8883
<s, z, s>(q_gen_8886) -> q_gen_8883
<z, s, s>(q_gen_8886) -> q_gen_8883
<z, z, z>() -> q_gen_8883
<s, s, s>(q_gen_8883) -> q_gen_8893
<z, z, s>(q_gen_8894) -> q_gen_8893
}

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]) -> 7
(is_even([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _lia])) -> plus([n, s(mm), s(_lia)]), {
_lia -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 9, which took 0.024877 s (model generation: 0.024428,  model checking: 0.000449):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_8883, q_gen_8886, q_gen_8893, q_gen_8894, q_gen_8898},
Q_f={q_gen_8883},
Delta=
{
<z>() -> q_gen_8894
<s, s>(q_gen_8886) -> q_gen_8886
<z, z>() -> q_gen_8886
<z, s>(q_gen_8894) -> q_gen_8898
<s, s, s>(q_gen_8893) -> q_gen_8883
<s, z, s>(q_gen_8886) -> q_gen_8883
<z, s, s>(q_gen_8886) -> q_gen_8883
<z, z, z>() -> q_gen_8883
<s, s, s>(q_gen_8883) -> q_gen_8893
<z, s, s>(q_gen_8898) -> q_gen_8893
<z, z, s>(q_gen_8894) -> q_gen_8893
}

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([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 10
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 10
}
Sat witness: Found: ((is_even([_qia]) /\ plus([x, y, _qia])) -> is_even([x]), {
_qia -> s(s(z))  ;  x -> s(z)  ;  y -> s(z)
})

-------------------------------------------
Step 10, which took 0.026032 s (model generation: 0.024104,  model checking: 0.001928):

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

Datatype: <nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_8883, q_gen_8886, q_gen_8890, q_gen_8891, q_gen_8894},
Q_f={q_gen_8883},
Delta=
{
<z>() -> q_gen_8894
<z, z>() -> q_gen_8886
<s, s>(q_gen_8886) -> q_gen_8890
<z, s>(q_gen_8894) -> q_gen_8890
<s, z, s>(q_gen_8890) -> q_gen_8883
<z, s, s>(q_gen_8886) -> q_gen_8883
<z, z, z>() -> q_gen_8883
<s, s, s>(q_gen_8883) -> q_gen_8891
<s, s, s>(q_gen_8891) -> q_gen_8891
<s, z, s>(q_gen_8886) -> q_gen_8891
<z, s, s>(q_gen_8890) -> q_gen_8891
<z, z, s>(q_gen_8894) -> q_gen_8891
}

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]) -> 10
(is_even([_qia]) /\ plus([x, y, _qia])) -> is_even([x]) -> 10
(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, _lia])) -> plus([n, s(mm), s(_lia)]) -> 10
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

Total time: 0.251298
Reason for stopping: Disproved