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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)])}
(plus([_ol, _pl, _ql]) /\ plus([_ol, _pl, _rl])) -> eq_nat([_ql, _rl])
)
(not_zero, P:
{() -> not_zero([s(nn)])
(not_zero([z])) -> BOT}
)
}

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


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, _sl])) -> not_zero([_sl]) -> 0
(not_zero([z])) -> BOT -> 0
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 0
}


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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007735 s (model generation: 0.006790,  model checking: 0.000945):

Model:
|_
{
not_zero -> 
{{{
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:
{
() -> not_zero([s(nn)]) -> 0
() -> plus([n, z, n]) -> 3
(not_zero([n]) /\ plus([n, m, _sl])) -> not_zero([_sl]) -> 1
(not_zero([z])) -> BOT -> 1
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.007160 s (model generation: 0.007116,  model checking: 0.000044):

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

}

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 1
(not_zero([z])) -> BOT -> 1
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 1
}
Sat witness: Found: (() -> not_zero([s(nn)]), {
nn -> z
})

-------------------------------------------
Step 2, which took 0.007295 s (model generation: 0.007203,  model checking: 0.000092):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 1
(not_zero([z])) -> BOT -> 1
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]), {
_nl -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.007528 s (model generation: 0.007513,  model checking: 0.000015):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 1
(not_zero([z])) -> BOT -> 4
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 4
}
Sat witness: Found: ((not_zero([z])) -> BOT, {

})

-------------------------------------------
Step 4, which took 0.010029 s (model generation: 0.009840,  model checking: 0.000189):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 2
(not_zero([z])) -> BOT -> 4
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.008806 s (model generation: 0.008701,  model checking: 0.000105):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 3
(not_zero([z])) -> BOT -> 4
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 4
}
Sat witness: Found: (() -> not_zero([s(nn)]), {
nn -> s(z)
})

-------------------------------------------
Step 6, which took 0.010279 s (model generation: 0.007861,  model checking: 0.002418):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 4
(not_zero([z])) -> BOT -> 4
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]), {
_nl -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.009014 s (model generation: 0.008719,  model checking: 0.000295):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 5
(not_zero([z])) -> BOT -> 5
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]), {
_nl -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.010909 s (model generation: 0.009623,  model checking: 0.001286):

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

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

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

}
--
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, _sl])) -> not_zero([_sl]) -> 6
(not_zero([z])) -> BOT -> 6
(plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _nl])) -> plus([n, s(mm), s(_nl)]), {
_nl -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

Total time: 0.090203
Reason for stopping: Proved