Solving ../../benchmarks/true/plus_succ_not_zero.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, _wc])) -> plus([n, s(mm), s(_wc)])}
(plus([_xc, _yc, _ad]) /\ plus([_xc, _yc, _zc])) -> eq_nat([_zc, _ad])
)
(not_zero, P:
{() -> not_zero([s(nn)])
(not_zero([z])) -> BOT}
)
}

properties:
{(plus([s(n), m, _bd])) -> not_zero([_bd])}


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

Clause system for inference is:

{
() -> not_zero([s(nn)]) -> 0  ;  () -> plus([n, z, n]) -> 0  ;  (not_zero([z])) -> BOT -> 0  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 0  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 0
}


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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008579 s (model generation: 0.008210,  model checking: 0.000369):

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([z])) -> BOT -> 1  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 1  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.009518 s (model generation: 0.009441,  model checking: 0.000077):

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

}

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

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([z])) -> BOT -> 1  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 1  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 1
}
Sat witness: Yes: (() -> not_zero([s(nn)]), {
nn -> z
})

-------------------------------------------
Step 2, which took 0.010833 s (model generation: 0.010617,  model checking: 0.000216):

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

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

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([z])) -> BOT -> 1  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 4  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 2
}
Sat witness: Yes: ((plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]), {
_wc -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.010332 s (model generation: 0.010324,  model checking: 0.000008):

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

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

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([z])) -> BOT -> 4  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 4  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 2
}
Sat witness: Yes: ((not_zero([z])) -> BOT, {

})

-------------------------------------------
Step 4, which took 0.006653 s (model generation: 0.006315,  model checking: 0.000338):

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

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

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([z])) -> BOT -> 4  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 4  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 3
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 5, which took 0.004011 s (model generation: 0.003949,  model checking: 0.000062):

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

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

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([z])) -> BOT -> 4  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 4  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 4
}
Sat witness: Yes: (() -> not_zero([s(nn)]), {
nn -> s(z)
})

-------------------------------------------
Step 6, which took 0.003670 s (model generation: 0.003533,  model checking: 0.000137):

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

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

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([z])) -> BOT -> 4  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 7  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 5
}
Sat witness: Yes: ((plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]), {
_wc -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.010514 s (model generation: 0.010213,  model checking: 0.000301):

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

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

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([z])) -> BOT -> 5  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 7  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 6
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.013020 s (model generation: 0.012553,  model checking: 0.000467):

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

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

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([z])) -> BOT -> 6  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 10  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]), {
_wc -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.013453 s (model generation: 0.012772,  model checking: 0.000681):

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

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

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([z])) -> BOT -> 7  ;  (plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 13  ;  (plus([s(n), m, _bd])) -> not_zero([_bd]) -> 8
}
Sat witness: Yes: ((plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]), {
_wc -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.106236
Reason for stopping: Proved