Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


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.080824 seconds.
Proved
Model:
|_
{
not_zero -> 
{{{
Q={q_gen_708, q_gen_709},
Q_f={q_gen_708},
Delta=
{
<s>(q_gen_708) -> q_gen_708
<s>(q_gen_709) -> q_gen_708
<z>() -> q_gen_709
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005742 s (model generation: 0.005340,  model checking: 0.000402):

Model:
|_
{
not_zero -> 
{{{
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:
{
() -> 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: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.004859 s (model generation: 0.004829,  model checking: 0.000030):

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

}

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

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

}
--
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: Found: (() -> not_zero([s(nn)]), {
nn -> z
})

-------------------------------------------
Step 2, which took 0.004478 s (model generation: 0.004218,  model checking: 0.000260):

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

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

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

}
--
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: Found: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.005329 s (model generation: 0.005318,  model checking: 0.000011):

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

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

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

}
--
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: Found: ((not_zero([z])) -> BOT, {

})

-------------------------------------------
Step 4, which took 0.005020 s (model generation: 0.004875,  model checking: 0.000145):

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

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

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

}
--
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: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.006234 s (model generation: 0.006090,  model checking: 0.000144):

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

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

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

}
--
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: Found: (() -> not_zero([s(nn)]), {
nn -> s(z)
})

-------------------------------------------
Step 6, which took 0.008436 s (model generation: 0.008129,  model checking: 0.000307):

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

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

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

}
--
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: Found: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.015188 s (model generation: 0.011559,  model checking: 0.003629):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 7
() -> plus([n, z, n]) -> 7
(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)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.014274 s (model generation: 0.013493,  model checking: 0.000781):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 8
() -> plus([n, z, n]) -> 8
(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)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _qc])) -> plus([n, s(mm), s(_qc)]), {
_qc -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.080824
Reason for stopping: Proved