Solving ../../benchmarks/true/plus_le.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)])}
(plus([_yba, _zba, _aca]) /\ plus([_yba, _zba, _bca])) -> eq_nat([_aca, _bca])
)
(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:
{(le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca])}


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

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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 0  ;  (le([z, z])) -> BOT -> 0  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 0
}


Solving took 0.323838 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4934},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<s>(q_gen_4926) -> q_gen_4926
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s>(q_gen_4934) -> q_gen_4934
<z, s>(q_gen_4926) -> q_gen_4934
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<s, z, s>(q_gen_4934) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4934) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009720 s (model generation: 0.009358,  model checking: 0.000362):

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}
--
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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010441 s (model generation: 0.010024,  model checking: 0.000417):

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

}

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

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

}
--
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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 1
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.010364 s (model generation: 0.010294,  model checking: 0.000070):

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

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

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

}
--
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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.004343 s (model generation: 0.003972,  model checking: 0.000371):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919},
Q_f={q_gen_4915},
Delta=
{
<z, z>() -> q_gen_4919
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

}
--
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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 2  ;  (le([z, z])) -> BOT -> 2  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 4
}
Sat witness: Yes: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.011469 s (model generation: 0.010920,  model checking: 0.000549):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919},
Q_f={q_gen_4915},
Delta=
{
<z, z>() -> q_gen_4919
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

}
--
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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 3  ;  (le([z, z])) -> BOT -> 3  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 5, which took 0.011914 s (model generation: 0.010995,  model checking: 0.000919):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919},
Q_f={q_gen_4915},
Delta=
{
<z, z>() -> q_gen_4919
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 4  ;  (le([z, z])) -> BOT -> 4  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 4
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 6, which took 0.011865 s (model generation: 0.011507,  model checking: 0.000358):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919},
Q_f={q_gen_4915},
Delta=
{
<z, z>() -> q_gen_4919
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 4  ;  (le([z, z])) -> BOT -> 4  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.012294 s (model generation: 0.012056,  model checking: 0.000238):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4926},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4915) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, s>(q_gen_4926) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 7  ;  (le([z, z])) -> BOT -> 5  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 7
}
Sat witness: Yes: ((le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]), {
_cca -> s(z)  ;  m -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 8, which took 0.013274 s (model generation: 0.012631,  model checking: 0.000643):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4926},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4915) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, s>(q_gen_4926) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 7  ;  (le([z, z])) -> BOT -> 8  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 7
}
Sat witness: Yes: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 9, which took 0.013056 s (model generation: 0.012893,  model checking: 0.000163):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4929},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<s, s>(q_gen_4929) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<z, z>() -> q_gen_4929
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4926},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4915) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, s>(q_gen_4926) -> q_gen_4915
<z, z, z>() -> q_gen_4915
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> 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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 7  ;  (le([z, z])) -> BOT -> 8  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 7
}
Sat witness: Yes: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.013103 s (model generation: 0.012685,  model checking: 0.000418):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4925, q_gen_4926},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4925) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4915) -> q_gen_4925
<z, z, s>(q_gen_4926) -> q_gen_4925
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (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, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 7  ;  (le([z, z])) -> BOT -> 8  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 11, which took 0.013761 s (model generation: 0.012950,  model checking: 0.000811):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4925, q_gen_4926},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4925) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4915) -> q_gen_4925
<z, z, s>(q_gen_4926) -> q_gen_4925
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8  ;  (le([s(nn1), z])) -> BOT -> 7  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 7  ;  (le([z, z])) -> BOT -> 8  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 12, which took 0.013775 s (model generation: 0.013541,  model checking: 0.000234):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, s>(q_gen_4926) -> q_gen_4919
<z, z>() -> q_gen_4919
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<s, z, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8  ;  (le([s(nn1), z])) -> BOT -> 7  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 10  ;  (le([z, z])) -> BOT -> 8  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 10
}
Sat witness: Yes: ((le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]), {
_cca -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.016870 s (model generation: 0.015691,  model checking: 0.001179):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, s>(q_gen_4926) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 8  ;  () -> plus([n, z, n]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9  ;  (le([s(nn1), z])) -> BOT -> 8  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 10  ;  (le([z, z])) -> BOT -> 9  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.018166 s (model generation: 0.017544,  model checking: 0.000622):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4919, q_gen_4925, q_gen_4926, q_gen_4934},
Q_f={q_gen_4915},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, z>() -> q_gen_4919
<z, s>(q_gen_4926) -> q_gen_4934
<s, s, s>(q_gen_4925) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, s, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4915) -> q_gen_4925
<s, z, s>(q_gen_4934) -> q_gen_4925
<z, s, s>(q_gen_4934) -> q_gen_4925
<z, z, s>(q_gen_4926) -> q_gen_4925
}

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

}
--
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]) -> 10  ;  (le([s(nn1), z])) -> BOT -> 9  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 13  ;  (le([z, z])) -> BOT -> 10  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 13
}
Sat witness: Yes: ((le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]), {
_cca -> s(s(z))  ;  m -> s(s(z))  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.017195 s (model generation: 0.016943,  model checking: 0.000252):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928, q_gen_4929},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4929) -> q_gen_4928
<z, z>() -> q_gen_4929
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, s>(q_gen_4926) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s, s>(q_gen_4927) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<s, z, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10  ;  () -> plus([n, z, n]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 10  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 13  ;  (le([z, z])) -> BOT -> 11  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 13
}
Sat witness: Yes: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> s(z)
})

-------------------------------------------
Step 16, which took 0.014592 s (model generation: 0.013854,  model checking: 0.000738):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4931},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<z>() -> q_gen_4926
<z, z>() -> q_gen_4919
<s, s>(q_gen_4919) -> q_gen_4931
<z, s>(q_gen_4926) -> q_gen_4931
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<s, z, s>(q_gen_4931) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4931) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10  ;  () -> plus([n, z, n]) -> 13  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 11  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 13  ;  (le([z, z])) -> BOT -> 11  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 13
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(s(z)))
})

-------------------------------------------
Step 17, which took 0.019861 s (model generation: 0.018983,  model checking: 0.000878):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4931},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<z>() -> q_gen_4926
<s, s>(q_gen_4931) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s>(q_gen_4919) -> q_gen_4931
<z, s>(q_gen_4926) -> q_gen_4931
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, s, s>(q_gen_4918) -> q_gen_4918
<s, z, s>(q_gen_4931) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4931) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 11  ;  () -> plus([n, z, n]) -> 13  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 12  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 13  ;  (le([z, z])) -> BOT -> 12  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 16
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 18, which took 0.020080 s (model generation: 0.019833,  model checking: 0.000247):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4931},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<s>(q_gen_4926) -> q_gen_4926
<z>() -> q_gen_4926
<s, s>(q_gen_4931) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s>(q_gen_4919) -> q_gen_4931
<z, s>(q_gen_4926) -> q_gen_4931
<s, s, s>(q_gen_4918) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, z, s>(q_gen_4931) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4931) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 12  ;  () -> plus([n, z, n]) -> 13  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 13  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 16  ;  (le([z, z])) -> BOT -> 13  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 16
}
Sat witness: Yes: ((le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]), {
_cca -> s(s(s(z)))  ;  m -> s(z)  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 19, which took 0.019671 s (model generation: 0.018665,  model checking: 0.001006):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4934},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<s>(q_gen_4926) -> q_gen_4926
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, z>() -> q_gen_4919
<z, s>(q_gen_4926) -> q_gen_4934
<s, s, s>(q_gen_4918) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, z, s>(q_gen_4934) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4934) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

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

-------------------------------------------
Step 20, which took 0.024106 s (model generation: 0.023083,  model checking: 0.001023):

Model:
|_
{
le -> 
{{{
Q={q_gen_4916, q_gen_4917, q_gen_4928},
Q_f={q_gen_4916},
Delta=
{
<s>(q_gen_4917) -> q_gen_4917
<z>() -> q_gen_4917
<s, s>(q_gen_4916) -> q_gen_4916
<z, s>(q_gen_4917) -> q_gen_4916
<s, s>(q_gen_4928) -> q_gen_4928
<z, z>() -> q_gen_4928
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4915, q_gen_4918, q_gen_4919, q_gen_4926, q_gen_4927, q_gen_4934},
Q_f={q_gen_4915, q_gen_4918},
Delta=
{
<s>(q_gen_4926) -> q_gen_4926
<z>() -> q_gen_4926
<s, s>(q_gen_4919) -> q_gen_4919
<z, z>() -> q_gen_4919
<s, s>(q_gen_4934) -> q_gen_4934
<z, s>(q_gen_4926) -> q_gen_4934
<s, s, s>(q_gen_4918) -> q_gen_4915
<s, z, s>(q_gen_4919) -> q_gen_4915
<z, z, z>() -> q_gen_4915
<s, z, s>(q_gen_4934) -> q_gen_4918
<z, s, s>(q_gen_4919) -> q_gen_4918
<z, s, s>(q_gen_4934) -> q_gen_4918
<z, z, s>(q_gen_4926) -> q_gen_4918
<s, s, s>(q_gen_4915) -> q_gen_4927
<s, s, s>(q_gen_4927) -> q_gen_4927
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 14  ;  () -> plus([n, z, n]) -> 15  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 15  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15  ;  (le([s(nn1), z])) -> BOT -> 15  ;  (le([z, m]) /\ plus([n, m, _cca])) -> le([n, _cca]) -> 17  ;  (le([z, z])) -> BOT -> 15  ;  (plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]) -> 22
}
Sat witness: Yes: ((plus([n, mm, _xba])) -> plus([n, s(mm), s(_xba)]), {
_xba -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

Total time: 0.323838
Reason for stopping: Proved