Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([a, n2])
() -> leq([b, b])
(leq([b, a])) -> BOT}
)
(leqnat, P:
{() -> leqnat([z, n2])
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)])
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2])
(leqnat([s(nn1), z])) -> BOT}
)
(merge, F:
{() -> merge([cons(z, xs), nil, cons(z, xs)])
() -> merge([nil, y, y])
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)])
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)])}
(merge([_yw, _zw, _ax]) /\ merge([_yw, _zw, _bx])) -> eq_eltlist([_ax, _bx])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)])}
(append([_dx, _ex, _fx]) /\ append([_dx, _ex, _gx])) -> eq_eltlist([_fx, _gx])
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)])}
(plus([_ix, _jx, _kx]) /\ plus([_ix, _jx, _lx])) -> eq_nat([_kx, _lx])
)
(length, F:
{() -> length([nil, z])
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)])}
(length([_nx, _ox]) /\ length([_nx, _px])) -> eq_nat([_ox, _px])
)
}

properties:
{(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]), (length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx])}


over-approximation: {append, length, merge, plus}
under-approximation: {append, leqnat, plus}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, n2]) -> 0
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0
() -> merge([nil, y, y]) -> 0
() -> plus([n, z, n]) -> 0
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 0
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 0
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 0
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 0
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 0
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 0
(leq([b, a])) -> BOT -> 0
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 0
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 0
(leqnat([s(nn1), z])) -> BOT -> 0
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 0
}


Solving took 1.596705 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<cons>(q_gen_4383, q_gen_4382) -> q_gen_4382
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<a, b>() -> q_gen_4355
<b, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, a, a>() -> q_gen_4384
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<a, b, b>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005891 s (model generation: 0.004952,  model checking: 0.000939):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, n2]) -> 0
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0
() -> merge([nil, y, y]) -> 0
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.005102 s (model generation: 0.004706,  model checking: 0.000396):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, n2]) -> 0
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 0
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> merge([nil, y, y]), {
y -> nil
})

-------------------------------------------
Step 2, which took 0.005080 s (model generation: 0.004572,  model checking: 0.000508):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326},
Q_f={q_gen_4326},
Delta=
{
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, n2]) -> 0
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> merge([cons(z, xs), nil, cons(z, xs)]), {
xs -> nil  ;  z -> b
})

-------------------------------------------
Step 3, which took 0.004891 s (model generation: 0.004846,  model checking: 0.000045):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 0
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> leqnat([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.004790 s (model generation: 0.004760,  model checking: 0.000030):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 0
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 5, which took 0.009134 s (model generation: 0.009077,  model checking: 0.000057):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> leq([a, n2]), {
n2 -> b
})

-------------------------------------------
Step 6, which took 0.010625 s (model generation: 0.010498,  model checking: 0.000127):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 7, which took 0.011662 s (model generation: 0.011361,  model checking: 0.000301):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 8, which took 0.012211 s (model generation: 0.011998,  model checking: 0.000213):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325},
Q_f={q_gen_4325},
Delta=
{
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1
(leqnat([s(nn1), z])) -> BOT -> 1
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]), {
_hx -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.012439 s (model generation: 0.012171,  model checking: 0.000268):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 1
(leq([b, a])) -> BOT -> 1
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.017647 s (model generation: 0.016885,  model checking: 0.000762):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<s, s>(q_gen_4330) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329},
Q_f={q_gen_4326},
Delta=
{
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 1
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 2
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, nil)  ;  xs -> nil  ;  y2 -> a  ;  ys -> nil  ;  z -> b
})

-------------------------------------------
Step 11, which took 0.017459 s (model generation: 0.013983,  model checking: 0.003476):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, a>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<s, s>(q_gen_4330) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 1
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 2
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(a, nil)  ;  xs -> cons(b, nil)  ;  y2 -> a  ;  ys -> nil  ;  z -> b
})

-------------------------------------------
Step 12, which took 0.015627 s (model generation: 0.015404,  model checking: 0.000223):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333},
Q_f={q_gen_4333},
Delta=
{
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, a>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<s, s>(q_gen_4330) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 1
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 2
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((length([ll, _mx])) -> length([cons(x, ll), s(_mx)]), {
_mx -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 13, which took 0.016419 s (model generation: 0.016090,  model checking: 0.000329):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, a>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330},
Q_f={q_gen_4330},
Delta=
{
<s, s>(q_gen_4330) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 1
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 1
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 2
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]), {
_tx -> z  ;  _ux -> cons(b, nil)  ;  _vx -> s(z)  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 14, which took 0.017432 s (model generation: 0.015244,  model checking: 0.002188):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334},
Q_f={q_gen_4334},
Delta=
{
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, a>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 2
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 2
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2
(leqnat([s(nn1), z])) -> BOT -> 2
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.015690 s (model generation: 0.015459,  model checking: 0.000231):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, a>() -> q_gen_4331
<b, b>() -> q_gen_4331
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 3
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 2
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 3
(leqnat([s(nn1), z])) -> BOT -> 3
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 16, which took 0.017295 s (model generation: 0.015049,  model checking: 0.002246):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<z, z>() -> q_gen_4336
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 3
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 3
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 17, which took 0.017232 s (model generation: 0.015489,  model checking: 0.001743):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<nil, nil>() -> q_gen_4328
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 3
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 3
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: (() -> merge([nil, y, y]), {
y -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 18, which took 0.018508 s (model generation: 0.016802,  model checking: 0.001706):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 3
() -> leq([b, b]) -> 3
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: (() -> leqnat([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 19, which took 0.017641 s (model generation: 0.017521,  model checking: 0.000120):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: (() -> leq([a, n2]), {
n2 -> a
})

-------------------------------------------
Step 20, which took 0.020158 s (model generation: 0.019359,  model checking: 0.000799):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<nil, nil>() -> q_gen_4354
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 21, which took 0.020717 s (model generation: 0.019298,  model checking: 0.001419):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336},
Q_f={q_gen_4325},
Delta=
{
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 4
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4
(leqnat([s(nn1), z])) -> BOT -> 4
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]), {
_hx -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 22, which took 0.019612 s (model generation: 0.016715,  model checking: 0.002897):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 4
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 7
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5
(leqnat([s(nn1), z])) -> BOT -> 5
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 7
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(a, nil)  ;  xs -> nil  ;  y2 -> a  ;  ys -> nil  ;  z -> b
})

-------------------------------------------
Step 23, which took 0.020842 s (model generation: 0.018982,  model checking: 0.001860):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 4
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 7
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 7
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5
(leqnat([s(nn1), z])) -> BOT -> 5
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 7
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(a, nil)  ;  xs -> nil  ;  y2 -> b  ;  ys -> nil  ;  z -> a
})

-------------------------------------------
Step 24, which took 0.029987 s (model generation: 0.029475,  model checking: 0.000512):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 4
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 4
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 4
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 7
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 7
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 7
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5
(leqnat([s(nn1), z])) -> BOT -> 5
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 7
}
Sat witness: Found: ((length([ll, _mx])) -> length([cons(x, ll), s(_mx)]), {
_mx -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 25, which took 0.028344 s (model generation: 0.025504,  model checking: 0.002840):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355},
Q_f={q_gen_4334},
Delta=
{
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, n2]) -> 6
() -> leq([b, b]) -> 4
() -> leqnat([z, n2]) -> 6
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 4
() -> merge([nil, y, y]) -> 6
() -> plus([n, z, n]) -> 6
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 7
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 5
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 5
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 7
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 7
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 7
(leq([b, a])) -> BOT -> 5
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5
(leqnat([s(nn1), z])) -> BOT -> 5
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.016598 s (model generation: 0.013791,  model checking: 0.002807):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 5
() -> leq([a, n2]) -> 7
() -> leq([b, b]) -> 5
() -> leqnat([z, n2]) -> 7
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 5
() -> merge([nil, y, y]) -> 7
() -> plus([n, z, n]) -> 7
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 7
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 6
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 6
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 7
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 7
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 7
(leq([b, a])) -> BOT -> 6
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 6
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 6
(leqnat([s(nn1), z])) -> BOT -> 6
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]), {
_hx -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 27, which took 0.031243 s (model generation: 0.025463,  model checking: 0.005780):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 6
() -> leq([a, n2]) -> 7
() -> leq([b, b]) -> 6
() -> leqnat([z, n2]) -> 7
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 6
() -> merge([nil, y, y]) -> 7
() -> plus([n, z, n]) -> 7
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 7
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 7
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 7
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 7
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 7
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 10
(leq([b, a])) -> BOT -> 7
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 7
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 7
(leqnat([s(nn1), z])) -> BOT -> 7
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 10
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, nil)  ;  xs -> nil  ;  y2 -> a  ;  ys -> cons(a, nil)  ;  z -> b
})

-------------------------------------------
Step 28, which took 0.023474 s (model generation: 0.022275,  model checking: 0.001199):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 7
() -> leq([a, n2]) -> 7
() -> leq([b, b]) -> 7
() -> leqnat([z, n2]) -> 7
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 7
() -> merge([nil, y, y]) -> 7
() -> plus([n, z, n]) -> 7
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 7
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 7
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 7
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 7
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 10
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 10
(leq([b, a])) -> BOT -> 8
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8
(leqnat([s(nn1), z])) -> BOT -> 8
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 10
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(a, nil)  ;  xs -> nil  ;  y2 -> b  ;  ys -> nil  ;  z -> b
})

-------------------------------------------
Step 29, which took 0.019548 s (model generation: 0.018546,  model checking: 0.001002):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 7
() -> leq([a, n2]) -> 7
() -> leq([b, b]) -> 7
() -> leqnat([z, n2]) -> 7
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 7
() -> merge([nil, y, y]) -> 7
() -> plus([n, z, n]) -> 7
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 10
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 8
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 8
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 8
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 10
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 10
(leq([b, a])) -> BOT -> 8
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8
(leqnat([s(nn1), z])) -> BOT -> 8
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 30, which took 0.015520 s (model generation: 0.013480,  model checking: 0.002040):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 8
() -> leq([a, n2]) -> 8
() -> leq([b, b]) -> 8
() -> leqnat([z, n2]) -> 8
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 8
() -> merge([nil, y, y]) -> 8
() -> plus([n, z, n]) -> 8
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 10
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 9
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 9
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 9
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 10
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 10
(leq([b, a])) -> BOT -> 9
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 9
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 9
(leqnat([s(nn1), z])) -> BOT -> 9
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]), {
_hx -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 31, which took 0.018860 s (model generation: 0.016572,  model checking: 0.002288):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 9
() -> leq([a, n2]) -> 9
() -> leq([b, b]) -> 9
() -> leqnat([z, n2]) -> 9
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 9
() -> merge([nil, y, y]) -> 9
() -> plus([n, z, n]) -> 9
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 10
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 10
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 10
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 10
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 10
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 13
(leq([b, a])) -> BOT -> 10
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 10
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 10
(leqnat([s(nn1), z])) -> BOT -> 10
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 13
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, cons(b, nil))  ;  xs -> nil  ;  y2 -> a  ;  ys -> cons(b, nil)  ;  z -> b
})

-------------------------------------------
Step 32, which took 0.020978 s (model generation: 0.018111,  model checking: 0.002867):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 10
() -> leq([a, n2]) -> 10
() -> leq([b, b]) -> 10
() -> leqnat([z, n2]) -> 10
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 10
() -> merge([nil, y, y]) -> 10
() -> plus([n, z, n]) -> 10
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 10
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 10
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 10
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 10
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 13
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 13
(leq([b, a])) -> BOT -> 11
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11
(leqnat([s(nn1), z])) -> BOT -> 11
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 13
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(b, nil)  ;  xs -> nil  ;  y2 -> a  ;  ys -> nil  ;  z -> a
})

-------------------------------------------
Step 33, which took 0.021745 s (model generation: 0.020253,  model checking: 0.001492):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 10
() -> leq([a, n2]) -> 10
() -> leq([b, b]) -> 10
() -> leqnat([z, n2]) -> 10
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 10
() -> merge([nil, y, y]) -> 10
() -> plus([n, z, n]) -> 10
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 13
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 11
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 11
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 11
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 13
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 13
(leq([b, a])) -> BOT -> 11
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11
(leqnat([s(nn1), z])) -> BOT -> 11
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.026730 s (model generation: 0.020108,  model checking: 0.006622):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 11
() -> leq([a, n2]) -> 11
() -> leq([b, b]) -> 11
() -> leqnat([z, n2]) -> 11
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 11
() -> merge([nil, y, y]) -> 11
() -> plus([n, z, n]) -> 11
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 13
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 12
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 12
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 12
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 13
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 16
(leq([b, a])) -> BOT -> 12
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 12
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 12
(leqnat([s(nn1), z])) -> BOT -> 12
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 14
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, cons(b, nil))  ;  xs -> nil  ;  y2 -> a  ;  ys -> nil  ;  z -> b
})

-------------------------------------------
Step 35, which took 0.078763 s (model generation: 0.054316,  model checking: 0.024447):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 12
() -> leq([a, n2]) -> 12
() -> leq([b, b]) -> 12
() -> leqnat([z, n2]) -> 12
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 12
() -> merge([nil, y, y]) -> 12
() -> plus([n, z, n]) -> 12
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 13
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 13
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 13
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 13
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 16
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 16
(leq([b, a])) -> BOT -> 13
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 13
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 13
(leqnat([s(nn1), z])) -> BOT -> 13
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 14
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(a, cons(b, nil))  ;  xs -> cons(b, nil)  ;  y2 -> a  ;  ys -> cons(b, nil)  ;  z -> a
})

-------------------------------------------
Step 36, which took 0.088267 s (model generation: 0.084280,  model checking: 0.003987):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 13
() -> leq([a, n2]) -> 13
() -> leq([b, b]) -> 13
() -> leqnat([z, n2]) -> 13
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 13
() -> merge([nil, y, y]) -> 13
() -> plus([n, z, n]) -> 13
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 16
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 14
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 14
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 14
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 16
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 16
(leq([b, a])) -> BOT -> 14
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 14
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14
(leqnat([s(nn1), z])) -> BOT -> 14
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 14
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.089703 s (model generation: 0.082885,  model checking: 0.006818):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 14
() -> leq([a, n2]) -> 14
() -> leq([b, b]) -> 14
() -> leqnat([z, n2]) -> 14
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 14
() -> merge([nil, y, y]) -> 14
() -> plus([n, z, n]) -> 14
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 16
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 15
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 15
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 15
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 16
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 19
(leq([b, a])) -> BOT -> 15
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 15
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 15
(leqnat([s(nn1), z])) -> BOT -> 15
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 15
}
Sat witness: Found: ((not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]), {
_xw -> cons(b, cons(b, nil))  ;  xs -> cons(a, nil)  ;  y2 -> a  ;  ys -> cons(a, nil)  ;  z -> b
})

-------------------------------------------
Step 38, which took 0.075683 s (model generation: 0.068443,  model checking: 0.007240):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 15
() -> leq([a, n2]) -> 15
() -> leq([b, b]) -> 15
() -> leqnat([z, n2]) -> 15
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 15
() -> merge([nil, y, y]) -> 15
() -> plus([n, z, n]) -> 15
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 16
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 16
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 16
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 16
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 19
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 19
(leq([b, a])) -> BOT -> 16
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 16
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 16
(leqnat([s(nn1), z])) -> BOT -> 16
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 16
}
Sat witness: Found: ((leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]), {
_ww -> cons(b, cons(b, nil))  ;  xs -> cons(a, nil)  ;  y2 -> a  ;  ys -> cons(b, nil)  ;  z -> a
})

-------------------------------------------
Step 39, which took 0.054677 s (model generation: 0.052329,  model checking: 0.002348):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<a, b, b>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> length([nil, z]) -> 16
() -> leq([a, n2]) -> 16
() -> leq([b, b]) -> 16
() -> leqnat([z, n2]) -> 16
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 16
() -> merge([nil, y, y]) -> 16
() -> plus([n, z, n]) -> 16
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 19
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 17
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 17
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 17
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 19
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 19
(leq([b, a])) -> BOT -> 17
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 17
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 17
(leqnat([s(nn1), z])) -> BOT -> 17
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 17
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 40, which took 0.107681 s (model generation: 0.055228,  model checking: 0.052453):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, a, a>() -> q_gen_4384
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<a, b, b>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> length([nil, z]) -> 17
() -> leq([a, n2]) -> 17
() -> leq([b, b]) -> 17
() -> leqnat([z, n2]) -> 17
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 17
() -> merge([nil, y, y]) -> 17
() -> plus([n, z, n]) -> 17
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 22
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 18
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 18
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 18
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 20
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 20
(leq([b, a])) -> BOT -> 18
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 18
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 18
(leqnat([s(nn1), z])) -> BOT -> 18
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 18
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 41, which took 0.138447 s (model generation: 0.055938,  model checking: 0.082509):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<cons>(q_gen_4383, q_gen_4382) -> q_gen_4382
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, a, a>() -> q_gen_4384
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<a, b, b>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 18
() -> leq([a, n2]) -> 18
() -> leq([b, b]) -> 18
() -> leqnat([z, n2]) -> 18
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 18
() -> merge([nil, y, y]) -> 18
() -> plus([n, z, n]) -> 18
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 25
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 19
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 19
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 19
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 21
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 21
(leq([b, a])) -> BOT -> 19
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 19
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 19
(leqnat([s(nn1), z])) -> BOT -> 19
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 42, which took 0.186577 s (model generation: 0.100395,  model checking: 0.086182):

Model:
|_
{
append -> 
{{{
Q={q_gen_4334, q_gen_4354, q_gen_4355, q_gen_4382, q_gen_4383, q_gen_4384},
Q_f={q_gen_4334},
Delta=
{
<cons>(q_gen_4383, q_gen_4382) -> q_gen_4382
<nil>() -> q_gen_4382
<a>() -> q_gen_4383
<b>() -> q_gen_4383
<cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4354
<nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4354
<nil, nil>() -> q_gen_4354
<a, a>() -> q_gen_4355
<b, a>() -> q_gen_4355
<b, b>() -> q_gen_4355
<cons, cons, cons>(q_gen_4384, q_gen_4334) -> q_gen_4334
<cons, nil, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, cons, cons>(q_gen_4355, q_gen_4354) -> q_gen_4334
<nil, nil, cons>(q_gen_4383, q_gen_4382) -> q_gen_4334
<nil, nil, nil>() -> q_gen_4334
<a, a, a>() -> q_gen_4384
<a, b, a>() -> q_gen_4384
<b, a, b>() -> q_gen_4384
<b, b, b>() -> q_gen_4384
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4333, q_gen_4350},
Q_f={q_gen_4333},
Delta=
{
<a>() -> q_gen_4350
<b>() -> q_gen_4350
<cons, s>(q_gen_4350, q_gen_4333) -> q_gen_4333
<nil, z>() -> q_gen_4333
}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_4331, q_gen_4338},
Q_f={q_gen_4331},
Delta=
{
<a, a>() -> q_gen_4331
<a, b>() -> q_gen_4331
<b, b>() -> q_gen_4331
<b, a>() -> q_gen_4338
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  leqnat -> 
{{{
Q={q_gen_4330, q_gen_4352},
Q_f={q_gen_4330},
Delta=
{
<s>(q_gen_4352) -> q_gen_4352
<z>() -> q_gen_4352
<s, s>(q_gen_4330) -> q_gen_4330
<z, s>(q_gen_4352) -> q_gen_4330
<z, z>() -> q_gen_4330
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  merge -> 
{{{
Q={q_gen_4326, q_gen_4328, q_gen_4329, q_gen_4341, q_gen_4342, q_gen_4343},
Q_f={q_gen_4326},
Delta=
{
<cons>(q_gen_4342, q_gen_4341) -> q_gen_4341
<nil>() -> q_gen_4341
<a>() -> q_gen_4342
<b>() -> q_gen_4342
<cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4328
<nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4328
<nil, nil>() -> q_gen_4328
<a, a>() -> q_gen_4329
<a, b>() -> q_gen_4329
<b, a>() -> q_gen_4329
<b, b>() -> q_gen_4329
<cons, cons, cons>(q_gen_4343, q_gen_4326) -> q_gen_4326
<cons, nil, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, cons, cons>(q_gen_4329, q_gen_4328) -> q_gen_4326
<nil, nil, cons>(q_gen_4342, q_gen_4341) -> q_gen_4326
<nil, nil, nil>() -> q_gen_4326
<a, a, a>() -> q_gen_4343
<a, a, b>() -> q_gen_4343
<a, b, a>() -> q_gen_4343
<a, b, b>() -> q_gen_4343
<b, a, a>() -> q_gen_4343
<b, a, b>() -> q_gen_4343
<b, b, a>() -> q_gen_4343
<b, b, b>() -> q_gen_4343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_4325, q_gen_4336, q_gen_4370},
Q_f={q_gen_4325},
Delta=
{
<s>(q_gen_4370) -> q_gen_4370
<z>() -> q_gen_4370
<s, s>(q_gen_4336) -> q_gen_4336
<z, s>(q_gen_4370) -> q_gen_4336
<z, z>() -> q_gen_4336
<s, s, s>(q_gen_4325) -> q_gen_4325
<s, z, s>(q_gen_4336) -> q_gen_4325
<z, s, s>(q_gen_4336) -> q_gen_4325
<z, z, s>(q_gen_4370) -> q_gen_4325
<z, z, z>() -> q_gen_4325
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 19
() -> leq([a, n2]) -> 19
() -> leq([b, b]) -> 19
() -> leqnat([z, n2]) -> 19
() -> merge([cons(z, xs), nil, cons(z, xs)]) -> 19
() -> merge([nil, y, y]) -> 19
() -> plus([n, z, n]) -> 19
(append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]) -> 28
(length([_rx, _sx]) /\ length([l1, _qx]) /\ merge([l1, l2, _rx])) -> leqnat([_qx, _sx]) -> 20
(length([_ux, _vx]) /\ length([l2, _tx]) /\ merge([l1, l2, _ux])) -> leqnat([_tx, _vx]) -> 20
(length([ll, _mx])) -> length([cons(x, ll), s(_mx)]) -> 20
(leq([z, y2]) /\ merge([xs, cons(y2, ys), _ww])) -> merge([cons(z, xs), cons(y2, ys), cons(z, _ww)]) -> 22
(not leq([z, y2]) /\ merge([cons(z, xs), ys, _xw])) -> merge([cons(z, xs), cons(y2, ys), cons(y2, _xw)]) -> 22
(leq([b, a])) -> BOT -> 20
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 20
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 20
(leqnat([s(nn1), z])) -> BOT -> 20
(plus([n, mm, _hx])) -> plus([n, s(mm), s(_hx)]) -> 20
}
Sat witness: Found: ((append([t1, l2, _cx])) -> append([cons(h1, t1), l2, cons(h1, _cx)]), {
_cx -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 1.596705
Reason for stopping: Proved