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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005254 s (model generation: 0.004920,  model checking: 0.000334):

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

-------------------------------------------
Step 1, which took 0.010536 s (model generation: 0.010459,  model checking: 0.000077):

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

}

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

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

-------------------------------------------
Step 2, which took 0.007288 s (model generation: 0.007201,  model checking: 0.000087):

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

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

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

-------------------------------------------
Step 3, which took 0.005029 s (model generation: 0.004994,  model checking: 0.000035):

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

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

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

})

-------------------------------------------
Step 4, which took 0.005727 s (model generation: 0.003878,  model checking: 0.001849):

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

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

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

-------------------------------------------
Step 5, which took 0.005253 s (model generation: 0.005160,  model checking: 0.000093):

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

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

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

-------------------------------------------
Step 6, which took 0.005069 s (model generation: 0.004707,  model checking: 0.000362):

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

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

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

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

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

-------------------------------------------
Step 7, which took 0.006810 s (model generation: 0.005220,  model checking: 0.001590):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> not_zero([s(nn)]) -> 5
() -> plus([n, z, n]) -> 7
(not_zero([z])) -> BOT -> 5
(plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]) -> 10
(plus([s(n), m, _bd])) -> not_zero([_bd]) -> 7
}
Sat witness: Found: ((plus([n, mm, _wc])) -> plus([n, s(mm), s(_wc)]), {
_wc -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.006699 s (model generation: 0.006350,  model checking: 0.000349):

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

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

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

Total time: 0.064757
Reason for stopping: Proved