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, _jz])) -> plus([n, s(mm), s(_jz)])}
(plus([_kz, _lz, _mz]) /\ plus([_kz, _lz, _nz])) -> eq_nat([_mz, _nz])
)
(le, P:
{() -> le([z, s(nn2)])
(le([nn1, nn2])) -> le([s(nn1), s(nn2)])
(le([s(nn1), s(nn2)])) -> le([nn1, nn2])
(le([s(nn1), z])) -> BOT
(le([z, z])) -> BOT}
)
}

properties:
{(plus([n, s(m), _oz])) -> le([n, _oz])}


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

Clause system for inference is:

{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 0
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0
(le([s(nn1), z])) -> BOT -> 0
(le([z, z])) -> BOT -> 0
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 0
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 0
}


Solving took 0.292040 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6713, q_gen_6714, q_gen_6719},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, z>() -> q_gen_6703
<s, s>(q_gen_6719) -> q_gen_6719
<z, s>(q_gen_6713) -> q_gen_6719
<s, z, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6702) -> q_gen_6702
<s, z, s>(q_gen_6719) -> q_gen_6702
<z, s, s>(q_gen_6703) -> q_gen_6702
<z, s, s>(q_gen_6719) -> q_gen_6702
<z, z, s>(q_gen_6713) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010004 s (model generation: 0.009838,  model checking: 0.000166):

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

}

Datatype: <nat, 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:
{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 1
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.009655 s (model generation: 0.009564,  model checking: 0.000091):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 1
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 1
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.011324 s (model generation: 0.009491,  model checking: 0.001833):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<z>() -> q_gen_6701
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 4
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 2
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.009705 s (model generation: 0.009587,  model checking: 0.000118):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<z>() -> q_gen_6701
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2
(le([s(nn1), z])) -> BOT -> 2
(le([z, z])) -> BOT -> 2
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 4
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 2
}
Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.009585 s (model generation: 0.009281,  model checking: 0.000304):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 4
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 3
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.009069 s (model generation: 0.008974,  model checking: 0.000095):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 4
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 6
}
Sat witness: Found: ((plus([n, s(m), _oz])) -> le([n, _oz]), {
_oz -> s(s(z))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.016674 s (model generation: 0.014735,  model checking: 0.001939):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 4
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 4
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 7
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 6
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.014627 s (model generation: 0.014315,  model checking: 0.000312):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 5
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 7
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 9
}
Sat witness: Found: ((plus([n, s(m), _oz])) -> le([n, _oz]), {
_oz -> s(z)  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 8, which took 0.013666 s (model generation: 0.013648,  model checking: 0.000018):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<z, z>() -> q_gen_6700
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 7
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 9
}
Sat witness: Found: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 9, which took 0.016713 s (model generation: 0.016628,  model checking: 0.000085):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6716},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<s, s>(q_gen_6716) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<z, z>() -> q_gen_6716
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 6
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 7
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 9
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.014361 s (model generation: 0.013859,  model checking: 0.000502):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6703, q_gen_6712, q_gen_6713},
Q_f={q_gen_6699},
Delta=
{
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, z>() -> q_gen_6703
<s, s, s>(q_gen_6712) -> q_gen_6699
<s, z, s>(q_gen_6703) -> q_gen_6699
<z, s, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6699) -> q_gen_6712
<z, z, s>(q_gen_6713) -> q_gen_6712
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6
() -> plus([n, z, n]) -> 7
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 7
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 10
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 9
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.014453 s (model generation: 0.014042,  model checking: 0.000411):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6712, q_gen_6713},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6703
<z, z>() -> q_gen_6703
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6702) -> q_gen_6702
<s, s, s>(q_gen_6712) -> q_gen_6702
<s, z, s>(q_gen_6703) -> q_gen_6702
<z, s, s>(q_gen_6703) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6712
<z, z, s>(q_gen_6713) -> q_gen_6712
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 7
() -> plus([n, z, n]) -> 8
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9
(le([s(nn1), z])) -> BOT -> 8
(le([z, z])) -> BOT -> 9
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 10
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 12
}
Sat witness: Found: ((plus([n, s(m), _oz])) -> le([n, _oz]), {
_oz -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.013501 s (model generation: 0.012103,  model checking: 0.001398):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6713, q_gen_6714},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6703
<z, z>() -> q_gen_6703
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6702) -> q_gen_6702
<s, z, s>(q_gen_6703) -> q_gen_6702
<z, s, s>(q_gen_6703) -> q_gen_6702
<z, z, s>(q_gen_6713) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 8
() -> plus([n, z, n]) -> 9
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10
(le([s(nn1), z])) -> BOT -> 9
(le([z, z])) -> BOT -> 10
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 13
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 12
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.017621 s (model generation: 0.016847,  model checking: 0.000774):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6713, q_gen_6714},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6703
<z, z>() -> q_gen_6703
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6702) -> q_gen_6702
<s, z, s>(q_gen_6703) -> q_gen_6702
<z, s, s>(q_gen_6703) -> q_gen_6702
<z, z, s>(q_gen_6713) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 9
() -> plus([n, z, n]) -> 10
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11
(le([s(nn1), z])) -> BOT -> 10
(le([z, z])) -> BOT -> 11
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 13
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 15
}
Sat witness: Found: ((plus([n, s(m), _oz])) -> le([n, _oz]), {
_oz -> s(s(z))  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.018223 s (model generation: 0.017316,  model checking: 0.000907):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6713, q_gen_6714},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6703
<z, z>() -> q_gen_6703
<s, s, s>(q_gen_6702) -> q_gen_6699
<s, z, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<z, s, s>(q_gen_6703) -> q_gen_6702
<z, z, s>(q_gen_6713) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10
() -> plus([n, z, n]) -> 11
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12
(le([s(nn1), z])) -> BOT -> 11
(le([z, z])) -> BOT -> 12
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 16
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 15
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.018022 s (model generation: 0.017242,  model checking: 0.000780):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715, q_gen_6716},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6716) -> q_gen_6715
<z, z>() -> q_gen_6716
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6702, q_gen_6703, q_gen_6712, q_gen_6713},
Q_f={q_gen_6699, q_gen_6702},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6703
<z, z>() -> q_gen_6703
<s, s, s>(q_gen_6702) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6712) -> q_gen_6702
<s, z, s>(q_gen_6703) -> q_gen_6702
<z, s, s>(q_gen_6703) -> q_gen_6702
<s, s, s>(q_gen_6699) -> q_gen_6712
<z, z, s>(q_gen_6713) -> q_gen_6712
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 11
() -> plus([n, z, n]) -> 12
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15
(le([s(nn1), z])) -> BOT -> 12
(le([z, z])) -> BOT -> 13
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 16
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 15
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> s(z)
})

-------------------------------------------
Step 16, which took 0.016244 s (model generation: 0.016018,  model checking: 0.000226):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6703, q_gen_6705, q_gen_6706, q_gen_6710, q_gen_6713},
Q_f={q_gen_6699, q_gen_6705},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<z, z>() -> q_gen_6703
<s, s>(q_gen_6703) -> q_gen_6706
<z, s>(q_gen_6713) -> q_gen_6706
<z, s, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6705) -> q_gen_6705
<s, z, s>(q_gen_6706) -> q_gen_6705
<z, s, s>(q_gen_6706) -> q_gen_6705
<z, z, s>(q_gen_6713) -> q_gen_6705
<s, s, s>(q_gen_6699) -> q_gen_6710
<s, s, s>(q_gen_6710) -> q_gen_6710
<s, z, s>(q_gen_6703) -> q_gen_6710
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 12
() -> plus([n, z, n]) -> 15
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15
(le([s(nn1), z])) -> BOT -> 13
(le([z, z])) -> BOT -> 13
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 16
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 15
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 17, which took 0.017356 s (model generation: 0.016360,  model checking: 0.000996):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6703, q_gen_6712, q_gen_6713, q_gen_6714, q_gen_6719},
Q_f={q_gen_6699, q_gen_6712},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<s, s>(q_gen_6703) -> q_gen_6703
<z, z>() -> q_gen_6703
<z, s>(q_gen_6713) -> q_gen_6719
<s, s, s>(q_gen_6712) -> q_gen_6699
<s, z, s>(q_gen_6703) -> q_gen_6699
<z, s, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, z, s>(q_gen_6719) -> q_gen_6712
<z, s, s>(q_gen_6719) -> q_gen_6712
<z, z, s>(q_gen_6713) -> q_gen_6712
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 13
() -> plus([n, z, n]) -> 16
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16
(le([s(nn1), z])) -> BOT -> 14
(le([z, z])) -> BOT -> 14
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 19
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 16
}
Sat witness: Found: ((plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]), {
_jz -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 18, which took 0.018832 s (model generation: 0.018633,  model checking: 0.000199):

Model:
|_
{
le -> 
{{{
Q={q_gen_6700, q_gen_6701, q_gen_6715},
Q_f={q_gen_6700},
Delta=
{
<s>(q_gen_6701) -> q_gen_6701
<z>() -> q_gen_6701
<s, s>(q_gen_6700) -> q_gen_6700
<z, s>(q_gen_6701) -> q_gen_6700
<s, s>(q_gen_6715) -> q_gen_6715
<z, z>() -> q_gen_6715
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_6699, q_gen_6703, q_gen_6705, q_gen_6706, q_gen_6713, q_gen_6714},
Q_f={q_gen_6699, q_gen_6705},
Delta=
{
<s>(q_gen_6713) -> q_gen_6713
<z>() -> q_gen_6713
<z, z>() -> q_gen_6703
<s, s>(q_gen_6703) -> q_gen_6706
<s, s>(q_gen_6706) -> q_gen_6706
<z, s>(q_gen_6713) -> q_gen_6706
<s, z, s>(q_gen_6703) -> q_gen_6699
<z, s, s>(q_gen_6703) -> q_gen_6699
<z, z, z>() -> q_gen_6699
<s, s, s>(q_gen_6705) -> q_gen_6705
<s, z, s>(q_gen_6706) -> q_gen_6705
<z, s, s>(q_gen_6706) -> q_gen_6705
<z, z, s>(q_gen_6713) -> q_gen_6705
<s, s, s>(q_gen_6699) -> q_gen_6714
<s, s, s>(q_gen_6714) -> q_gen_6714
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 14
() -> plus([n, z, n]) -> 16
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 14
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16
(le([s(nn1), z])) -> BOT -> 15
(le([z, z])) -> BOT -> 15
(plus([n, mm, _jz])) -> plus([n, s(mm), s(_jz)]) -> 19
(plus([n, s(m), _oz])) -> le([n, _oz]) -> 19
}
Sat witness: Found: ((plus([n, s(m), _oz])) -> le([n, _oz]), {
_oz -> s(s(s(z)))  ;  m -> z  ;  n -> s(s(s(z)))
})

Total time: 0.292040
Reason for stopping: Proved