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

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, _cha])) -> plus([n, s(mm), s(_cha)])}
(plus([_dha, _eha, _fha]) /\ plus([_dha, _eha, _gha])) -> eq_nat([_fha, _gha])
)
}

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


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

Clause system for inference is:

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


Solving took 0.146924 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010250 s (model generation: 0.009907,  model checking: 0.000343):

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

-------------------------------------------
Step 1, which took 0.010040 s (model generation: 0.009991,  model checking: 0.000049):

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

}

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

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

})

-------------------------------------------
Step 2, which took 0.010273 s (model generation: 0.010087,  model checking: 0.000186):

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

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

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

-------------------------------------------
Step 3, which took 0.010606 s (model generation: 0.010473,  model checking: 0.000133):

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

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

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

-------------------------------------------
Step 4, which took 0.010980 s (model generation: 0.010919,  model checking: 0.000061):

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

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

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

})

-------------------------------------------
Step 5, which took 0.013181 s (model generation: 0.012839,  model checking: 0.000342):

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

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

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

-------------------------------------------
Step 6, which took 0.011881 s (model generation: 0.011292,  model checking: 0.000589):

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

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

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

-------------------------------------------
Step 7, which took 0.012577 s (model generation: 0.012192,  model checking: 0.000385):

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

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

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

-------------------------------------------
Step 8, which took 0.013982 s (model generation: 0.012940,  model checking: 0.001042):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_6521, q_gen_6524, q_gen_6531, q_gen_6532},
Q_f={q_gen_6521},
Delta=
{
<z>() -> q_gen_6532
<s, s>(q_gen_6524) -> q_gen_6524
<z, z>() -> q_gen_6524
<s, s, s>(q_gen_6531) -> q_gen_6521
<s, z, s>(q_gen_6524) -> q_gen_6521
<z, s, s>(q_gen_6524) -> q_gen_6521
<z, z, z>() -> q_gen_6521
<s, s, s>(q_gen_6521) -> q_gen_6531
<z, z, s>(q_gen_6532) -> q_gen_6531
}

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

-------------------------------------------
Step 9, which took 0.015033 s (model generation: 0.014048,  model checking: 0.000985):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_6521, q_gen_6524, q_gen_6531, q_gen_6532, q_gen_6536},
Q_f={q_gen_6521},
Delta=
{
<z>() -> q_gen_6532
<s, s>(q_gen_6524) -> q_gen_6524
<z, z>() -> q_gen_6524
<z, s>(q_gen_6532) -> q_gen_6536
<s, s, s>(q_gen_6531) -> q_gen_6521
<s, z, s>(q_gen_6524) -> q_gen_6521
<z, s, s>(q_gen_6524) -> q_gen_6521
<z, z, z>() -> q_gen_6521
<s, s, s>(q_gen_6521) -> q_gen_6531
<z, s, s>(q_gen_6536) -> q_gen_6531
<z, z, s>(q_gen_6532) -> q_gen_6531
}

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

-------------------------------------------
Step 10, which took 0.014676 s (model generation: 0.014185,  model checking: 0.000491):

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

Datatype: <nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_6521, q_gen_6524, q_gen_6528, q_gen_6529, q_gen_6532},
Q_f={q_gen_6521},
Delta=
{
<z>() -> q_gen_6532
<z, z>() -> q_gen_6524
<s, s>(q_gen_6524) -> q_gen_6528
<z, s>(q_gen_6532) -> q_gen_6528
<s, z, s>(q_gen_6528) -> q_gen_6521
<z, s, s>(q_gen_6524) -> q_gen_6521
<z, z, z>() -> q_gen_6521
<s, s, s>(q_gen_6521) -> q_gen_6529
<s, s, s>(q_gen_6529) -> q_gen_6529
<s, z, s>(q_gen_6524) -> q_gen_6529
<z, s, s>(q_gen_6528) -> q_gen_6529
<z, z, s>(q_gen_6532) -> q_gen_6529
}

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

Total time: 0.146924
Reason for stopping: Disproved