Solving ../../benchmarks/true/length_fun_le_cons.smt2...

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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(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}
)
(length, F:
{() -> length([nil, z])
(length([ll, _tr])) -> length([cons(x, ll), s(_tr)])}
(length([_ur, _vr]) /\ length([_ur, _wr])) -> eq_nat([_vr, _wr])
)
(fcons, F:
{() -> fcons([x, l, cons(x, l)])}
(fcons([_xr, _yr, _as]) /\ fcons([_xr, _yr, _zr])) -> eq_natlist([_zr, _as])
)
}

properties:
{(fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds])}


over-approximation: {fcons, length}
under-approximation: {le}

Clause system for inference is:

{
() -> fcons([x, l, cons(x, l)]) -> 0  ;  () -> le([z, s(nn2)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 0
}


Solving took 1.471315 seconds.
Proved
Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3240
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, s>(q_gen_3214) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, cons, z>(q_gen_3222, q_gen_3221) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<s, nil, z>(q_gen_3214) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006478 s (model generation: 0.005999,  model checking: 0.000479):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 0  ;  () -> le([z, s(nn2)]) -> 0  ;  () -> length([nil, z]) -> 3  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 1  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 1, which took 0.009556 s (model generation: 0.009442,  model checking: 0.000114):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 0  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 1  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 1
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.011118 s (model generation: 0.010356,  model checking: 0.000762):

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

}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<z>() -> q_gen_3211
<z, s>(q_gen_3211) -> q_gen_3210
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 1  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 1
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> z
})

-------------------------------------------
Step 3, which took 0.011049 s (model generation: 0.010817,  model checking: 0.000232):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<z>() -> q_gen_3211
<z, s>(q_gen_3211) -> q_gen_3210
}

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

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 1  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 4
}
Sat witness: Yes: ((length([ll, _tr])) -> length([cons(x, ll), s(_tr)]), {
_tr -> z  ;  ll -> nil  ;  x -> z
})

-------------------------------------------
Step 4, which took 0.011489 s (model generation: 0.011209,  model checking: 0.000280):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<z>() -> q_gen_3211
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216},
Q_f={q_gen_3209},
Delta=
{
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 1  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 4
}
Sat witness: Yes: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 5, which took 0.011757 s (model generation: 0.011146,  model checking: 0.000611):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216},
Q_f={q_gen_3209},
Delta=
{
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 3  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 2  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 4
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 6, which took 0.012928 s (model generation: 0.011337,  model checking: 0.001591):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216},
Q_f={q_gen_3209},
Delta=
{
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 6  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 3  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 4
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 7, which took 0.012315 s (model generation: 0.011842,  model checking: 0.000473):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil>() -> q_gen_3221
<z, s>(q_gen_3214) -> q_gen_3222
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216},
Q_f={q_gen_3209},
Delta=
{
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 6  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 4  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 7
}
Sat witness: Yes: ((length([ll, _tr])) -> length([cons(x, ll), s(_tr)]), {
_tr -> z  ;  ll -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 8, which took 0.014489 s (model generation: 0.012057,  model checking: 0.002432):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<z, nil>() -> q_gen_3221
<z, s>(q_gen_3214) -> q_gen_3222
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 9  ;  () -> le([z, s(nn2)]) -> 7  ;  () -> length([nil, z]) -> 5  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 5  ;  (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  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 7
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.013573 s (model generation: 0.012601,  model checking: 0.000972):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 9  ;  () -> le([z, s(nn2)]) -> 7  ;  () -> length([nil, z]) -> 6  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 6  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6  ;  (le([s(nn1), z])) -> BOT -> 6  ;  (le([z, z])) -> BOT -> 6  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 10
}
Sat witness: Yes: ((length([ll, _tr])) -> length([cons(x, ll), s(_tr)]), {
_tr -> z  ;  ll -> nil  ;  x -> s(s(z))
})

-------------------------------------------
Step 10, which took 0.017428 s (model generation: 0.013390,  model checking: 0.004038):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 12  ;  () -> le([z, s(nn2)]) -> 8  ;  () -> length([nil, z]) -> 7  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 7  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 7  ;  (le([s(nn1), z])) -> BOT -> 7  ;  (le([z, z])) -> BOT -> 7  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 10
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, nil)  ;  x -> s(z)
})

-------------------------------------------
Step 11, which took 0.014956 s (model generation: 0.013641,  model checking: 0.001315):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 12  ;  () -> le([z, s(nn2)]) -> 9  ;  () -> length([nil, z]) -> 8  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 8  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8  ;  (le([s(nn1), z])) -> BOT -> 8  ;  (le([z, z])) -> BOT -> 8  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 13
}
Sat witness: Yes: ((length([ll, _tr])) -> length([cons(x, ll), s(_tr)]), {
_tr -> s(z)  ;  ll -> cons(z, nil)  ;  x -> s(z)
})

-------------------------------------------
Step 12, which took 0.030851 s (model generation: 0.014542,  model checking: 0.016309):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 15  ;  () -> le([z, s(nn2)]) -> 10  ;  () -> length([nil, z]) -> 9  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 9  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9  ;  (le([s(nn1), z])) -> BOT -> 9  ;  (le([z, z])) -> BOT -> 9  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 13
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, nil)  ;  x -> z
})

-------------------------------------------
Step 13, which took 0.011936 s (model generation: 0.010454,  model checking: 0.001482):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 15  ;  () -> le([z, s(nn2)]) -> 11  ;  () -> length([nil, z]) -> 10  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10  ;  (le([s(nn1), z])) -> BOT -> 10  ;  (le([z, z])) -> BOT -> 10  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 16
}
Sat witness: Yes: ((length([ll, _tr])) -> length([cons(x, ll), s(_tr)]), {
_tr -> s(z)  ;  ll -> cons(z, nil)  ;  x -> z
})

-------------------------------------------
Step 14, which took 0.030557 s (model generation: 0.015856,  model checking: 0.014701):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 18  ;  () -> le([z, s(nn2)]) -> 12  ;  () -> length([nil, z]) -> 11  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 11  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11  ;  (le([s(nn1), z])) -> BOT -> 11  ;  (le([z, z])) -> BOT -> 11  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 16
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, nil)  ;  x -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.059344 s (model generation: 0.011926,  model checking: 0.047418):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 21  ;  () -> le([z, s(nn2)]) -> 13  ;  () -> length([nil, z]) -> 12  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 12  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12  ;  (le([s(nn1), z])) -> BOT -> 12  ;  (le([z, z])) -> BOT -> 12  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 17
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> nil  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 16, which took 0.053532 s (model generation: 0.006319,  model checking: 0.047213):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 24  ;  () -> le([z, s(nn2)]) -> 14  ;  () -> length([nil, z]) -> 13  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 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, z])) -> BOT -> 13  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 18
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, nil)  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 17, which took 0.031405 s (model generation: 0.007478,  model checking: 0.023927):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 27  ;  () -> le([z, s(nn2)]) -> 15  ;  () -> length([nil, z]) -> 14  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 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, z])) -> BOT -> 14  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 19
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), nil)  ;  x -> z
})

-------------------------------------------
Step 18, which took 0.029240 s (model generation: 0.007657,  model checking: 0.021583):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 30  ;  () -> le([z, s(nn2)]) -> 16  ;  () -> length([nil, z]) -> 15  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 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, z])) -> BOT -> 15  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 20
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), nil)  ;  x -> s(z)
})

-------------------------------------------
Step 19, which took 0.031726 s (model generation: 0.008246,  model checking: 0.023480):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 33  ;  () -> le([z, s(nn2)]) -> 17  ;  () -> length([nil, z]) -> 16  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 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, z])) -> BOT -> 16  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 21
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, nil))  ;  x -> s(z)
})

-------------------------------------------
Step 20, which took 0.028506 s (model generation: 0.008751,  model checking: 0.019755):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 36  ;  () -> le([z, s(nn2)]) -> 18  ;  () -> length([nil, z]) -> 17  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 17  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 17  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 17  ;  (le([s(nn1), z])) -> BOT -> 17  ;  (le([z, z])) -> BOT -> 17  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 22
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), nil)  ;  x -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.027699 s (model generation: 0.009433,  model checking: 0.018266):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 39  ;  () -> le([z, s(nn2)]) -> 19  ;  () -> length([nil, z]) -> 18  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 18  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 18  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 18  ;  (le([s(nn1), z])) -> BOT -> 18  ;  (le([z, z])) -> BOT -> 18  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 23
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), nil)  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 22, which took 0.028294 s (model generation: 0.011276,  model checking: 0.017018):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 42  ;  () -> le([z, s(nn2)]) -> 20  ;  () -> length([nil, z]) -> 19  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 19  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 19  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 19  ;  (le([s(nn1), z])) -> BOT -> 19  ;  (le([z, z])) -> BOT -> 19  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 24
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(s(z)), nil)  ;  x -> s(s(z))
})

-------------------------------------------
Step 23, which took 0.032065 s (model generation: 0.013247,  model checking: 0.018818):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 45  ;  () -> le([z, s(nn2)]) -> 21  ;  () -> length([nil, z]) -> 20  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 20  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 20  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 20  ;  (le([s(nn1), z])) -> BOT -> 20  ;  (le([z, z])) -> BOT -> 20  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 25
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, nil))  ;  x -> z
})

-------------------------------------------
Step 24, which took 0.031025 s (model generation: 0.013847,  model checking: 0.017178):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 48  ;  () -> le([z, s(nn2)]) -> 22  ;  () -> length([nil, z]) -> 21  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 21  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 21  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 21  ;  (le([s(nn1), z])) -> BOT -> 21  ;  (le([z, z])) -> BOT -> 21  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 26
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(s(z)), nil)  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 25, which took 0.036507 s (model generation: 0.016034,  model checking: 0.020473):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 51  ;  () -> le([z, s(nn2)]) -> 23  ;  () -> length([nil, z]) -> 22  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 22  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 22  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 22  ;  (le([s(nn1), z])) -> BOT -> 22  ;  (le([z, z])) -> BOT -> 22  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 27
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, nil))  ;  x -> s(s(z))
})

-------------------------------------------
Step 26, which took 0.188118 s (model generation: 0.018794,  model checking: 0.169324):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 54  ;  () -> le([z, s(nn2)]) -> 24  ;  () -> length([nil, z]) -> 23  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 23  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 23  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 23  ;  (le([s(nn1), z])) -> BOT -> 23  ;  (le([z, z])) -> BOT -> 23  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 28
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), cons(s(z), nil))  ;  x -> s(s(s(s(z))))
})

-------------------------------------------
Step 27, which took 0.126077 s (model generation: 0.024298,  model checking: 0.101779):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 57  ;  () -> le([z, s(nn2)]) -> 25  ;  () -> length([nil, z]) -> 24  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 24  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 24  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 24  ;  (le([s(nn1), z])) -> BOT -> 24  ;  (le([z, z])) -> BOT -> 24  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 29
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), cons(s(s(z)), nil))  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 28, which took 0.139075 s (model generation: 0.038174,  model checking: 0.100901):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 60  ;  () -> le([z, s(nn2)]) -> 26  ;  () -> length([nil, z]) -> 25  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 25  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 25  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 25  ;  (le([s(nn1), z])) -> BOT -> 25  ;  (le([z, z])) -> BOT -> 25  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 30
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), cons(s(s(z)), nil))  ;  x -> s(s(s(s(z))))
})

-------------------------------------------
Step 29, which took 0.050156 s (model generation: 0.045945,  model checking: 0.004211):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 63  ;  () -> le([z, s(nn2)]) -> 27  ;  () -> length([nil, z]) -> 26  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 26  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 26  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 26  ;  (le([s(nn1), z])) -> BOT -> 26  ;  (le([z, z])) -> BOT -> 26  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 31
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), cons(z, nil))  ;  x -> s(z)
})

-------------------------------------------
Step 30, which took 0.053686 s (model generation: 0.049747,  model checking: 0.003939):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, s>(q_gen_3214) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 66  ;  () -> le([z, s(nn2)]) -> 28  ;  () -> length([nil, z]) -> 27  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 27  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 27  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 27  ;  (le([s(nn1), z])) -> BOT -> 27  ;  (le([z, z])) -> BOT -> 27  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 32
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(s(z), cons(z, cons(z, nil)))  ;  x -> s(z)
})

-------------------------------------------
Step 31, which took 0.062827 s (model generation: 0.060337,  model checking: 0.002490):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3240
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, s>(q_gen_3214) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 69  ;  () -> le([z, s(nn2)]) -> 29  ;  () -> length([nil, z]) -> 28  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 28  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 28  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 28  ;  (le([s(nn1), z])) -> BOT -> 28  ;  (le([z, z])) -> BOT -> 28  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 33
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, nil))  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 32, which took 0.069180 s (model generation: 0.066699,  model checking: 0.002481):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3240
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, s>(q_gen_3214) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<s, nil, z>(q_gen_3214) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 72  ;  () -> le([z, s(nn2)]) -> 30  ;  () -> length([nil, z]) -> 29  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 29  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 29  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 29  ;  (le([s(nn1), z])) -> BOT -> 29  ;  (le([z, z])) -> BOT -> 29  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 34
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, cons(z, nil)))  ;  x -> s(s(z))
})

-------------------------------------------
Step 33, which took 0.081495 s (model generation: 0.078444,  model checking: 0.003051):

Model:
|_
{
fcons -> 
{{{
Q={q_gen_3212, q_gen_3213, q_gen_3214, q_gen_3221, q_gen_3222, q_gen_3233, q_gen_3234, q_gen_3235, q_gen_3239, q_gen_3240},
Q_f={q_gen_3212},
Delta=
{
<cons>(q_gen_3214, q_gen_3213) -> q_gen_3213
<nil>() -> q_gen_3213
<s>(q_gen_3214) -> q_gen_3214
<z>() -> q_gen_3214
<s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3221
<s, nil>(q_gen_3214) -> q_gen_3221
<z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3221
<z, nil>() -> q_gen_3221
<s, s>(q_gen_3222) -> q_gen_3222
<s, z>(q_gen_3214) -> q_gen_3222
<z, s>(q_gen_3214) -> q_gen_3222
<z, z>() -> q_gen_3222
<cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3239
<nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3239
<cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3240
<cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3240
<nil, s>(q_gen_3214) -> q_gen_3240
<nil, z>() -> q_gen_3240
<s, cons, cons>(q_gen_3235, q_gen_3234, q_gen_3233, q_gen_3212) -> q_gen_3212
<s, nil, cons>(q_gen_3222, q_gen_3221) -> q_gen_3212
<z, cons, cons>(q_gen_3222, q_gen_3221, q_gen_3240, q_gen_3239) -> q_gen_3212
<z, nil, cons>(q_gen_3214, q_gen_3213) -> q_gen_3212
<s, cons, s>(q_gen_3235, q_gen_3233) -> q_gen_3233
<s, nil, s>(q_gen_3222) -> q_gen_3233
<s, nil, z>(q_gen_3214) -> q_gen_3233
<z, cons, s>(q_gen_3222, q_gen_3240) -> q_gen_3233
<z, cons, z>(q_gen_3214, q_gen_3213) -> q_gen_3233
<z, nil, s>(q_gen_3214) -> q_gen_3233
<z, nil, z>() -> q_gen_3233
<s, s, cons>(q_gen_3235, q_gen_3234) -> q_gen_3234
<s, s, nil>(q_gen_3222) -> q_gen_3234
<s, z, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<s, z, nil>(q_gen_3214) -> q_gen_3234
<z, s, cons>(q_gen_3222, q_gen_3221) -> q_gen_3234
<z, s, nil>(q_gen_3214) -> q_gen_3234
<z, z, cons>(q_gen_3214, q_gen_3213) -> q_gen_3234
<z, z, nil>() -> q_gen_3234
<s, s, s>(q_gen_3235) -> q_gen_3235
<s, s, z>(q_gen_3222) -> q_gen_3235
<s, z, s>(q_gen_3222) -> q_gen_3235
<s, z, z>(q_gen_3214) -> q_gen_3235
<z, s, s>(q_gen_3222) -> q_gen_3235
<z, s, z>(q_gen_3214) -> q_gen_3235
<z, z, s>(q_gen_3214) -> q_gen_3235
<z, z, z>() -> q_gen_3235
}

Datatype: <nat, natlist, natlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_3210, q_gen_3211},
Q_f={q_gen_3210},
Delta=
{
<s>(q_gen_3211) -> q_gen_3211
<z>() -> q_gen_3211
<s, s>(q_gen_3210) -> q_gen_3210
<z, s>(q_gen_3211) -> q_gen_3210
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_3209, q_gen_3216, q_gen_3225},
Q_f={q_gen_3209},
Delta=
{
<s>(q_gen_3225) -> q_gen_3225
<z>() -> q_gen_3225
<cons, s>(q_gen_3216, q_gen_3209) -> q_gen_3209
<nil, z>() -> q_gen_3209
<s, s>(q_gen_3216) -> q_gen_3216
<s, z>(q_gen_3225) -> q_gen_3216
<z, s>(q_gen_3225) -> q_gen_3216
<z, z>() -> q_gen_3216
}

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

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

Teacher's answer:
New clause system:
{
() -> fcons([x, l, cons(x, l)]) -> 75  ;  () -> le([z, s(nn2)]) -> 31  ;  () -> length([nil, z]) -> 30  ;  (fcons([x, l, _cs]) /\ length([_cs, _ds]) /\ length([l, _bs])) -> le([_bs, _ds]) -> 30  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 30  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 30  ;  (le([s(nn1), z])) -> BOT -> 30  ;  (le([z, z])) -> BOT -> 30  ;  (length([ll, _tr])) -> length([cons(x, ll), s(_tr)]) -> 35
}
Sat witness: Yes: (() -> fcons([x, l, cons(x, l)]), {
l -> cons(z, cons(z, cons(z, nil)))  ;  x -> s(s(s(z)))
})

Total time: 1.471315
Reason for stopping: Proved