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, _dz])) -> plus([n, s(mm), s(_dz)])}
(plus([_ez, _fz, _gz]) /\ plus([_ez, _fz, _hz])) -> eq_nat([_gz, _hz])
)
(not_zero, P:
{() -> not_zero([s(nn)])
(not_zero([z])) -> BOT}
)
}

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


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, _dz])) -> plus([n, s(mm), s(_dz)]) -> 0
(plus([s(n), m, _iz])) -> not_zero([_iz]) -> 0
}


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

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.013749 s (model generation: 0.013068,  model checking: 0.000681):

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

-------------------------------------------
Step 1, which took 0.008425 s (model generation: 0.008382,  model checking: 0.000043):

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

}

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

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

-------------------------------------------
Step 2, which took 0.009408 s (model generation: 0.009300,  model checking: 0.000108):

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

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

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

-------------------------------------------
Step 3, which took 0.010954 s (model generation: 0.010938,  model checking: 0.000016):

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

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

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

})

-------------------------------------------
Step 4, which took 0.010209 s (model generation: 0.010023,  model checking: 0.000186):

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

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

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

-------------------------------------------
Step 5, which took 0.010441 s (model generation: 0.010357,  model checking: 0.000084):

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

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

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

-------------------------------------------
Step 6, which took 0.009588 s (model generation: 0.009429,  model checking: 0.000159):

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

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

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

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

-------------------------------------------
Step 7, which took 0.012016 s (model generation: 0.011739,  model checking: 0.000277):

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

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

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

}
--
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, _dz])) -> plus([n, s(mm), s(_dz)]) -> 10
(plus([s(n), m, _iz])) -> not_zero([_iz]) -> 7
}
Sat witness: Found: ((plus([n, mm, _dz])) -> plus([n, s(mm), s(_dz)]), {
_dz -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 8, which took 0.012404 s (model generation: 0.012048,  model checking: 0.000356):

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

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

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

Total time: 0.113925
Reason for stopping: Proved