Solving ../../benchmarks/true/plus_not_zero_implication.smt2...

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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)])}
(plus([_rc, _sc, _tc]) /\ plus([_rc, _sc, _uc])) -> eq_nat([_tc, _uc])
)
(not_zero, P:
{() -> not_zero([s(nn)])
(not_zero([z])) -> BOT}
)
}

properties:
{(not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc])}


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

Clause system for inference is:

{
() -> not_zero([s(nn)]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 0  ;  (not_zero([z])) -> BOT -> 0  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 0
}


Solving took 0.070297 seconds.
Proved
Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4990) -> q_gen_4990
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4989, q_gen_4993, q_gen_4998},
Q_f={q_gen_4989},
Delta=
{
<s>(q_gen_4998) -> q_gen_4998
<z>() -> q_gen_4998
<s, s>(q_gen_4993) -> q_gen_4993
<z, s>(q_gen_4998) -> q_gen_4993
<z, z>() -> q_gen_4993
<s, s, s>(q_gen_4989) -> q_gen_4989
<s, z, s>(q_gen_4993) -> q_gen_4989
<z, s, s>(q_gen_4993) -> q_gen_4989
<z, z, s>(q_gen_4998) -> q_gen_4989
<z, z, z>() -> q_gen_4989
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004897 s (model generation: 0.004731,  model checking: 0.000166):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 0  ;  () -> plus([n, z, n]) -> 3  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 1  ;  (not_zero([z])) -> BOT -> 1  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.008122 s (model generation: 0.008050,  model checking: 0.000072):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 1  ;  (not_zero([z])) -> BOT -> 1  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 1
}
Sat witness: Yes: (() -> not_zero([s(nn)]), {
nn -> z
})

-------------------------------------------
Step 2, which took 0.010741 s (model generation: 0.010538,  model checking: 0.000203):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 1  ;  (not_zero([z])) -> BOT -> 1  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.011314 s (model generation: 0.011285,  model checking: 0.000029):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 1  ;  (not_zero([z])) -> BOT -> 4  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 4
}
Sat witness: Yes: ((not_zero([z])) -> BOT, {

})

-------------------------------------------
Step 4, which took 0.007197 s (model generation: 0.007050,  model checking: 0.000147):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 3  ;  () -> plus([n, z, n]) -> 6  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 2  ;  (not_zero([z])) -> BOT -> 4  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 5, which took 0.005105 s (model generation: 0.004958,  model checking: 0.000147):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 3  ;  (not_zero([z])) -> BOT -> 4  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 4
}
Sat witness: Yes: (() -> not_zero([s(nn)]), {
nn -> s(z)
})

-------------------------------------------
Step 6, which took 0.004870 s (model generation: 0.004750,  model checking: 0.000120):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4990) -> q_gen_4990
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 6  ;  () -> plus([n, z, n]) -> 6  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 4  ;  (not_zero([z])) -> BOT -> 4  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.004012 s (model generation: 0.003907,  model checking: 0.000105):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4990) -> q_gen_4990
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4989, q_gen_4993, q_gen_4998},
Q_f={q_gen_4989},
Delta=
{
<z>() -> q_gen_4998
<z, z>() -> q_gen_4993
<s, s, s>(q_gen_4989) -> q_gen_4989
<s, z, s>(q_gen_4993) -> q_gen_4989
<z, s, s>(q_gen_4993) -> q_gen_4989
<z, z, s>(q_gen_4998) -> q_gen_4989
<z, z, z>() -> q_gen_4989
}

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 5  ;  (not_zero([z])) -> BOT -> 5  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.004280 s (model generation: 0.003944,  model checking: 0.000336):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4990) -> q_gen_4990
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4989, q_gen_4993, q_gen_4998},
Q_f={q_gen_4989},
Delta=
{
<z>() -> q_gen_4998
<s, s>(q_gen_4993) -> q_gen_4993
<z, z>() -> q_gen_4993
<s, s, s>(q_gen_4989) -> q_gen_4989
<s, z, s>(q_gen_4993) -> q_gen_4989
<z, s, s>(q_gen_4993) -> q_gen_4989
<z, z, s>(q_gen_4998) -> q_gen_4989
<z, z, z>() -> q_gen_4989
}

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 6  ;  (not_zero([z])) -> BOT -> 6  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.004455 s (model generation: 0.004198,  model checking: 0.000257):

Model:
|_
{
not_zero -> 
{{{
Q={q_gen_4990, q_gen_4991},
Q_f={q_gen_4990},
Delta=
{
<s>(q_gen_4990) -> q_gen_4990
<s>(q_gen_4991) -> q_gen_4990
<z>() -> q_gen_4991
}

Datatype: <nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4989, q_gen_4993, q_gen_4998},
Q_f={q_gen_4989},
Delta=
{
<z>() -> q_gen_4998
<s, s>(q_gen_4993) -> q_gen_4993
<z, s>(q_gen_4998) -> q_gen_4993
<z, z>() -> q_gen_4993
<s, s, s>(q_gen_4989) -> q_gen_4989
<s, z, s>(q_gen_4993) -> q_gen_4989
<z, s, s>(q_gen_4993) -> q_gen_4989
<z, z, s>(q_gen_4998) -> q_gen_4989
<z, z, z>() -> q_gen_4989
}

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 8  ;  () -> plus([n, z, n]) -> 10  ;  (not_zero([n]) /\ plus([n, m, _vc])) -> not_zero([_vc]) -> 7  ;  (not_zero([z])) -> BOT -> 7  ;  (plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.070297
Reason for stopping: Proved