Solving ../../benchmarks/true/plus_le_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, _lda])) -> plus([n, s(mm), s(_lda)])}
(plus([_mda, _nda, _oda]) /\ plus([_mda, _nda, _pda])) -> eq_nat([_oda, _pda])
)
(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]) /\ le([z, n]) /\ plus([n, m, _qda])) -> le([n, _qda])}


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


Solving took 0.283714 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4969},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<s>(q_gen_4961) -> q_gen_4961
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s>(q_gen_4969) -> q_gen_4969
<z, s>(q_gen_4961) -> q_gen_4969
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4969) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4969) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009356 s (model generation: 0.008997,  model checking: 0.000359):

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

-------------------------------------------
Step 1, which took 0.010340 s (model generation: 0.010217,  model checking: 0.000123):

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

}

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

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

-------------------------------------------
Step 2, which took 0.010598 s (model generation: 0.010306,  model checking: 0.000292):

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

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

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

-------------------------------------------
Step 3, which took 0.011117 s (model generation: 0.010798,  model checking: 0.000319):

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

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

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

-------------------------------------------
Step 4, which took 0.014304 s (model generation: 0.010964,  model checking: 0.003340):

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

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

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

-------------------------------------------
Step 5, which took 0.011527 s (model generation: 0.011049,  model checking: 0.000478):

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

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

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

-------------------------------------------
Step 6, which took 0.011635 s (model generation: 0.011336,  model checking: 0.000299):

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

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

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

-------------------------------------------
Step 7, which took 0.013071 s (model generation: 0.012827,  model checking: 0.000244):

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

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

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

-------------------------------------------
Step 8, which took 0.013349 s (model generation: 0.012985,  model checking: 0.000364):

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

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

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

})

-------------------------------------------
Step 9, which took 0.013232 s (model generation: 0.013079,  model checking: 0.000153):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4964},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<s, s>(q_gen_4964) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<z, z>() -> q_gen_4964
}

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

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

-------------------------------------------
Step 10, which took 0.015446 s (model generation: 0.013014,  model checking: 0.002432):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4954, q_gen_4960, q_gen_4961},
Q_f={q_gen_4950},
Delta=
{
<z>() -> q_gen_4961
<z, z>() -> q_gen_4954
<s, s, s>(q_gen_4960) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, s, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4950) -> q_gen_4960
<z, z, s>(q_gen_4961) -> q_gen_4960
}

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

-------------------------------------------
Step 11, which took 0.013821 s (model generation: 0.013159,  model checking: 0.000662):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4954, q_gen_4960, q_gen_4961},
Q_f={q_gen_4950},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s, s>(q_gen_4960) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, s, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4950) -> q_gen_4960
<z, z, s>(q_gen_4961) -> q_gen_4960
}

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

-------------------------------------------
Step 12, which took 0.013758 s (model generation: 0.013561,  model checking: 0.000197):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4954
<z, z>() -> q_gen_4954
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
}

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

-------------------------------------------
Step 13, which took 0.011155 s (model generation: 0.009618,  model checking: 0.001537):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
}

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

-------------------------------------------
Step 14, which took 0.018717 s (model generation: 0.017529,  model checking: 0.001188):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4954, q_gen_4960, q_gen_4961, q_gen_4969},
Q_f={q_gen_4950},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, z>() -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4969
<s, s, s>(q_gen_4960) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, s, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4950) -> q_gen_4960
<s, z, s>(q_gen_4969) -> q_gen_4960
<z, s, s>(q_gen_4969) -> q_gen_4960
<z, z, s>(q_gen_4961) -> q_gen_4960
}

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

-------------------------------------------
Step 15, which took 0.019914 s (model generation: 0.019130,  model checking: 0.000784):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963, q_gen_4964},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4964) -> q_gen_4963
<z, z>() -> q_gen_4964
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s, s>(q_gen_4962) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
}

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

-------------------------------------------
Step 16, which took 0.011258 s (model generation: 0.010985,  model checking: 0.000273):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4966},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<z>() -> q_gen_4961
<z, z>() -> q_gen_4954
<s, s>(q_gen_4954) -> q_gen_4966
<z, s>(q_gen_4961) -> q_gen_4966
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4966) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4966) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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

-------------------------------------------
Step 17, which took 0.007850 s (model generation: 0.006817,  model checking: 0.001033):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4966},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<z>() -> q_gen_4961
<s, s>(q_gen_4966) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s>(q_gen_4954) -> q_gen_4966
<z, s>(q_gen_4961) -> q_gen_4966
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4966) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4966) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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]) /\ le([z, n]) /\ plus([n, m, _qda])) -> le([n, _qda]) -> 13  ;  (le([z, z])) -> BOT -> 12  ;  (plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]) -> 16
}
Sat witness: Yes: ((plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]), {
_lda -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 18, which took 0.007736 s (model generation: 0.007372,  model checking: 0.000364):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4966},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<s>(q_gen_4961) -> q_gen_4961
<z>() -> q_gen_4961
<s, s>(q_gen_4966) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s>(q_gen_4954) -> q_gen_4966
<z, s>(q_gen_4961) -> q_gen_4966
<s, s, s>(q_gen_4953) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, z, s>(q_gen_4966) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4966) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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

-------------------------------------------
Step 19, which took 0.009040 s (model generation: 0.008629,  model checking: 0.000411):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4969},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<s>(q_gen_4961) -> q_gen_4961
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, z>() -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4969
<s, s, s>(q_gen_4953) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, z, s>(q_gen_4969) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4969) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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]) /\ le([z, n]) /\ plus([n, m, _qda])) -> le([n, _qda]) -> 16  ;  (le([z, z])) -> BOT -> 14  ;  (plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]) -> 19
}
Sat witness: Yes: ((plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]), {
_lda -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 20, which took 0.009859 s (model generation: 0.009097,  model checking: 0.000762):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4969},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<s>(q_gen_4961) -> q_gen_4961
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<z, z>() -> q_gen_4954
<s, s>(q_gen_4969) -> q_gen_4969
<z, s>(q_gen_4961) -> q_gen_4969
<s, s, s>(q_gen_4953) -> q_gen_4950
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, z, s>(q_gen_4969) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4969) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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]) /\ le([z, n]) /\ plus([n, m, _qda])) -> le([n, _qda]) -> 17  ;  (le([z, z])) -> BOT -> 15  ;  (plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]) -> 22
}
Sat witness: Yes: ((plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]), {
_lda -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.011160 s (model generation: 0.010500,  model checking: 0.000660):

Model:
|_
{
le -> 
{{{
Q={q_gen_4951, q_gen_4952, q_gen_4963},
Q_f={q_gen_4951},
Delta=
{
<s>(q_gen_4952) -> q_gen_4952
<z>() -> q_gen_4952
<s, s>(q_gen_4951) -> q_gen_4951
<z, s>(q_gen_4952) -> q_gen_4951
<s, s>(q_gen_4963) -> q_gen_4963
<z, z>() -> q_gen_4963
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_4950, q_gen_4953, q_gen_4954, q_gen_4961, q_gen_4962, q_gen_4969},
Q_f={q_gen_4950, q_gen_4953},
Delta=
{
<s>(q_gen_4961) -> q_gen_4961
<z>() -> q_gen_4961
<s, s>(q_gen_4954) -> q_gen_4954
<s, s>(q_gen_4969) -> q_gen_4954
<z, z>() -> q_gen_4954
<z, s>(q_gen_4961) -> q_gen_4969
<s, z, s>(q_gen_4954) -> q_gen_4950
<z, z, z>() -> q_gen_4950
<s, s, s>(q_gen_4953) -> q_gen_4953
<s, z, s>(q_gen_4969) -> q_gen_4953
<z, s, s>(q_gen_4954) -> q_gen_4953
<z, s, s>(q_gen_4969) -> q_gen_4953
<z, z, s>(q_gen_4961) -> q_gen_4953
<s, s, s>(q_gen_4950) -> q_gen_4962
<s, s, s>(q_gen_4962) -> q_gen_4962
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 15  ;  () -> plus([n, z, n]) -> 16  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 16  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16  ;  (le([s(nn1), z])) -> BOT -> 16  ;  (le([z, m]) /\ le([z, n]) /\ plus([n, m, _qda])) -> le([n, _qda]) -> 18  ;  (le([z, z])) -> BOT -> 16  ;  (plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]) -> 25
}
Sat witness: Yes: ((plus([n, mm, _lda])) -> plus([n, s(mm), s(_lda)]), {
_lda -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

Total time: 0.283714
Reason for stopping: Proved