Solving ../../benchmarks/true/append_length_leq.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)])}
(append([_la, _ma, _na]) /\ append([_la, _ma, _oa])) -> eq_eltlist([_na, _oa])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)])}
(length([_qa, _ra]) /\ length([_qa, _sa])) -> eq_nat([_ra, _sa])
)
}

properties:
{(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]), (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya])}


over-approximation: {append, length}
under-approximation: {leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> length([nil, z]) -> 0  ;  () -> leq([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 0  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 0  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 0  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 0  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 0  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0  ;  (leq([s(nn1), z])) -> BOT -> 0
}


Solving took 30.002678 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_256, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_263, q_gen_264, q_gen_265, q_gen_266, q_gen_269, q_gen_270, q_gen_271, q_gen_272, q_gen_273, q_gen_274, q_gen_275, q_gen_276, q_gen_277, q_gen_278, q_gen_279, q_gen_280, q_gen_284, q_gen_285, q_gen_286, q_gen_287, q_gen_288, q_gen_289, q_gen_290, q_gen_291, q_gen_294, q_gen_295, q_gen_296, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303, q_gen_308, q_gen_309, q_gen_310, q_gen_311, q_gen_312, q_gen_313, q_gen_314, q_gen_315, q_gen_316, q_gen_317, q_gen_318, q_gen_319, q_gen_320, q_gen_321, q_gen_322, q_gen_323, q_gen_324, q_gen_325, q_gen_326, q_gen_327, q_gen_328, q_gen_329, q_gen_330, q_gen_331, q_gen_332, q_gen_333, q_gen_334, q_gen_335, q_gen_336, q_gen_337, q_gen_338, q_gen_339, q_gen_340, q_gen_341, q_gen_342, q_gen_343, q_gen_344, q_gen_345, q_gen_346, q_gen_347, q_gen_348, q_gen_349, q_gen_350, q_gen_351, q_gen_352, q_gen_353, q_gen_354, q_gen_355, q_gen_356, q_gen_357, q_gen_358, q_gen_359, q_gen_360, q_gen_361, q_gen_362, q_gen_363, q_gen_364, q_gen_365, q_gen_366, q_gen_367, q_gen_368, q_gen_369, q_gen_370, q_gen_371, q_gen_372, q_gen_373, q_gen_374, q_gen_375, q_gen_376, q_gen_377, q_gen_378},
Q_f={},
Delta=
{
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_279
<cons>(q_gen_279, q_gen_273) -> q_gen_290
<cons>(q_gen_274, q_gen_273) -> q_gen_336
<nil, nil>() -> q_gen_257
<nil, b>() -> q_gen_258
<b, nil>() -> q_gen_259
<b, b>() -> q_gen_260
<nil, a>() -> q_gen_264
<a, nil>() -> q_gen_265
<a, a>() -> q_gen_266
<cons, cons>(q_gen_266, q_gen_265, q_gen_264, q_gen_257) -> q_gen_271
<cons, b>(q_gen_274, q_gen_273) -> q_gen_272
<b, cons>(q_gen_274, q_gen_273) -> q_gen_275
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_277
<cons, b>(q_gen_279, q_gen_273) -> q_gen_278
<b, cons>(q_gen_279, q_gen_273) -> q_gen_280
<cons, a>(q_gen_279, q_gen_273) -> q_gen_285
<a, cons>(q_gen_279, q_gen_273) -> q_gen_286
<cons, cons>(q_gen_260, q_gen_280, q_gen_278, q_gen_277) -> q_gen_288
<cons, b>(q_gen_279, q_gen_290) -> q_gen_289
<b, cons>(q_gen_279, q_gen_290) -> q_gen_291
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_310
<a, cons>(q_gen_274, q_gen_273) -> q_gen_332
<a, b>() -> q_gen_333
<nil, cons>(q_gen_279, q_gen_273) -> q_gen_343
<b, a>() -> q_gen_344
<nil, nil, nil>() -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_256
<nil, cons, cons>(q_gen_266, q_gen_265, q_gen_264, q_gen_257) -> q_gen_263
<cons, nil, cons>(q_gen_266, q_gen_265, q_gen_264, q_gen_257) -> q_gen_269
<cons, nil, cons>(q_gen_260, q_gen_275, q_gen_272, q_gen_271) -> q_gen_270
<nil, cons, cons>(q_gen_260, q_gen_280, q_gen_278, q_gen_277) -> q_gen_276
<cons, nil, cons>(q_gen_266, q_gen_286, q_gen_285, q_gen_277) -> q_gen_284
<nil, cons, cons>(q_gen_260, q_gen_291, q_gen_289, q_gen_288) -> q_gen_287
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_294
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_296) -> q_gen_295
<nil, nil, cons>(q_gen_279, q_gen_273) -> q_gen_296
<nil, nil, b>() -> q_gen_297
<nil, b, cons>(q_gen_279, q_gen_273) -> q_gen_298
<nil, b, b>() -> q_gen_299
<b, nil, cons>(q_gen_279, q_gen_273) -> q_gen_300
<b, nil, b>() -> q_gen_301
<b, b, cons>(q_gen_279, q_gen_273) -> q_gen_302
<b, b, b>() -> q_gen_303
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_308
<cons, nil, cons>(q_gen_260, q_gen_275, q_gen_258, q_gen_310) -> q_gen_309
<cons, cons, cons>(q_gen_316, q_gen_315, q_gen_301, q_gen_314, q_gen_313, q_gen_312, q_gen_297, q_gen_308) -> q_gen_311
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_312
<nil, a, b>() -> q_gen_313
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_314
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_315
<b, a, b>() -> q_gen_316
<cons, cons, cons>(q_gen_323, q_gen_322, q_gen_321, q_gen_320, q_gen_319, q_gen_298, q_gen_318, q_gen_296) -> q_gen_317
<nil, nil, a>() -> q_gen_318
<nil, b, a>() -> q_gen_319
<a, nil, cons>(q_gen_279, q_gen_273) -> q_gen_320
<a, nil, a>() -> q_gen_321
<a, b, cons>(q_gen_279, q_gen_273) -> q_gen_322
<a, b, a>() -> q_gen_323
<cons, cons, cons>(q_gen_328, q_gen_327, q_gen_321, q_gen_326, q_gen_325, q_gen_312, q_gen_318, q_gen_308) -> q_gen_324
<nil, a, a>() -> q_gen_325
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_326
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_327
<a, a, a>() -> q_gen_328
<nil, cons, cons>(q_gen_260, q_gen_275, q_gen_272, q_gen_271) -> q_gen_329
<cons, cons, cons>(q_gen_303, q_gen_339, q_gen_338, q_gen_337, q_gen_299, q_gen_335, q_gen_334, q_gen_331) -> q_gen_330
<nil, cons, cons>(q_gen_333, q_gen_332, q_gen_258, q_gen_310) -> q_gen_331
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_334
<nil, b, cons>(q_gen_279, q_gen_336) -> q_gen_335
<b, cons, cons>(q_gen_333, q_gen_332, q_gen_258, q_gen_310) -> q_gen_337
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_338
<b, b, cons>(q_gen_279, q_gen_336) -> q_gen_339
<nil, cons, cons>(q_gen_266, q_gen_286, q_gen_285, q_gen_277) -> q_gen_340
<cons, cons, cons>(q_gen_328, q_gen_349, q_gen_348, q_gen_347, q_gen_325, q_gen_346, q_gen_345, q_gen_342) -> q_gen_341
<nil, cons, cons>(q_gen_344, q_gen_280, q_gen_264, q_gen_343) -> q_gen_342
<nil, cons, a>(q_gen_279, q_gen_273) -> q_gen_345
<nil, a, cons>(q_gen_274, q_gen_290) -> q_gen_346
<a, cons, cons>(q_gen_344, q_gen_280, q_gen_264, q_gen_343) -> q_gen_347
<a, cons, a>(q_gen_279, q_gen_273) -> q_gen_348
<a, a, cons>(q_gen_274, q_gen_290) -> q_gen_349
<cons, cons, cons>(q_gen_303, q_gen_356, q_gen_301, q_gen_355, q_gen_354, q_gen_353, q_gen_352, q_gen_351) -> q_gen_350
<cons, nil, cons>(q_gen_260, q_gen_280, q_gen_258, q_gen_343) -> q_gen_351
<cons, nil, b>(q_gen_279, q_gen_273) -> q_gen_352
<cons, b, cons>(q_gen_260, q_gen_280, q_gen_258, q_gen_343) -> q_gen_353
<cons, b, b>(q_gen_279, q_gen_273) -> q_gen_354
<b, nil, cons>(q_gen_279, q_gen_290) -> q_gen_355
<b, b, cons>(q_gen_279, q_gen_290) -> q_gen_356
<cons, cons, cons>(q_gen_316, q_gen_359, q_gen_301, q_gen_300, q_gen_313, q_gen_358, q_gen_297, q_gen_296) -> q_gen_357
<nil, a, cons>(q_gen_279, q_gen_273) -> q_gen_358
<b, a, cons>(q_gen_279, q_gen_273) -> q_gen_359
<cons, cons, cons>(q_gen_316, q_gen_363, q_gen_301, q_gen_355, q_gen_362, q_gen_361, q_gen_352, q_gen_351) -> q_gen_360
<cons, a, cons>(q_gen_260, q_gen_280, q_gen_258, q_gen_343) -> q_gen_361
<cons, a, b>(q_gen_279, q_gen_273) -> q_gen_362
<b, a, cons>(q_gen_279, q_gen_290) -> q_gen_363
<cons, cons, cons>(q_gen_323, q_gen_368, q_gen_321, q_gen_367, q_gen_366, q_gen_353, q_gen_365, q_gen_351) -> q_gen_364
<cons, nil, a>(q_gen_279, q_gen_273) -> q_gen_365
<cons, b, a>(q_gen_279, q_gen_273) -> q_gen_366
<a, nil, cons>(q_gen_279, q_gen_290) -> q_gen_367
<a, b, cons>(q_gen_279, q_gen_290) -> q_gen_368
<cons, cons, cons>(q_gen_328, q_gen_371, q_gen_321, q_gen_367, q_gen_370, q_gen_361, q_gen_365, q_gen_351) -> q_gen_369
<cons, a, a>(q_gen_279, q_gen_273) -> q_gen_370
<a, a, cons>(q_gen_279, q_gen_290) -> q_gen_371
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_375, q_gen_374, q_gen_299, q_gen_298, q_gen_373, q_gen_294) -> q_gen_372
<nil, cons, b>(q_gen_279, q_gen_273) -> q_gen_373
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_374
<b, cons, b>(q_gen_279, q_gen_273) -> q_gen_375
<cons, cons, cons>(q_gen_323, q_gen_368, q_gen_348, q_gen_378, q_gen_366, q_gen_353, q_gen_377, q_gen_295) -> q_gen_376
<cons, cons, a>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_377
<a, cons, cons>(q_gen_260, q_gen_280, q_gen_258, q_gen_343) -> q_gen_378
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_254, q_gen_255, q_gen_267, q_gen_268, q_gen_281, q_gen_282, q_gen_283, q_gen_292, q_gen_293, q_gen_304, q_gen_305, q_gen_306, q_gen_307},
Q_f={},
Delta=
{
<z>() -> q_gen_283
<s>(q_gen_283) -> q_gen_307
<nil, z>() -> q_gen_251
<cons, s>(q_gen_255, q_gen_251) -> q_gen_254
<b, z>() -> q_gen_255
<cons, s>(q_gen_268, q_gen_251) -> q_gen_267
<a, z>() -> q_gen_268
<cons, s>(q_gen_282, q_gen_267) -> q_gen_281
<b, s>(q_gen_283) -> q_gen_282
<cons, s>(q_gen_293, q_gen_254) -> q_gen_292
<a, s>(q_gen_283) -> q_gen_293
<cons, s>(q_gen_282, q_gen_254) -> q_gen_304
<cons, s>(q_gen_306, q_gen_304) -> q_gen_305
<b, s>(q_gen_307) -> q_gen_306
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_249, q_gen_250, q_gen_253, q_gen_261, q_gen_262},
Q_f={},
Delta=
{
<z>() -> q_gen_250
<s>(q_gen_250) -> q_gen_262
<z, z>() -> q_gen_248
<z, s>(q_gen_250) -> q_gen_249
<s, s>(q_gen_248) -> q_gen_253
<z, s>(q_gen_262) -> q_gen_261
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004226 s (model generation: 0.003836,  model checking: 0.000390):

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

}

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

}

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

}

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

}
--
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([z, s(nn2)]) -> 0  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([z, z]), {

})

-------------------------------------------
Step 1, which took 0.003537 s (model generation: 0.003494,  model checking: 0.000043):

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

}

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

}

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

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.003468 s (model generation: 0.003423,  model checking: 0.000045):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.003830 s (model generation: 0.003419,  model checking: 0.000411):

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

}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1  ;  (leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 4, which took 0.003711 s (model generation: 0.003628,  model checking: 0.000083):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 5, which took 0.004032 s (model generation: 0.003937,  model checking: 0.000095):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 6, which took 0.006894 s (model generation: 0.006239,  model checking: 0.000655):

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

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 3  ;  () -> leq([z, z]) -> 3  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009549 s (model generation: 0.009275,  model checking: 0.000274):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260},
Q_f={q_gen_252},
Delta=
{
<nil, nil>() -> q_gen_257
<nil, b>() -> q_gen_258
<b, nil>() -> q_gen_259
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 2  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 2  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3  ;  (leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Yes: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 8, which took 0.009452 s (model generation: 0.008201,  model checking: 0.001251):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260},
Q_f={q_gen_252},
Delta=
{
<nil, nil>() -> q_gen_257
<nil, b>() -> q_gen_258
<b, nil>() -> q_gen_259
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 3  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 3  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4  ;  (leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 9, which took 0.007940 s (model generation: 0.007675,  model checking: 0.000265):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260},
Q_f={q_gen_252},
Delta=
{
<nil, nil>() -> q_gen_257
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, nil>() -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 4  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 4  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 7  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 10, which took 0.017697 s (model generation: 0.011344,  model checking: 0.006353):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260},
Q_f={q_gen_252},
Delta=
{
<nil, nil>() -> q_gen_257
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, nil>() -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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([z, s(nn2)]) -> 6  ;  () -> leq([z, z]) -> 4  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 4  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 4  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 7  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 7  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 11, which took 0.031739 s (model generation: 0.011132,  model checking: 0.020607):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<nil>() -> q_gen_273
<a>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 5  ;  () -> leq([z, s(nn2)]) -> 7  ;  () -> leq([z, z]) -> 5  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 5  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 5  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 7  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 7  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6  ;  (leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 12, which took 0.005889 s (model generation: 0.005473,  model checking: 0.000416):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

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

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 6  ;  () -> leq([z, s(nn2)]) -> 7  ;  () -> leq([z, z]) -> 6  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 6  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 6  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 7  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7  ;  (leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Yes: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 13, which took 0.015113 s (model generation: 0.006727,  model checking: 0.008386):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 7  ;  () -> leq([z, s(nn2)]) -> 7  ;  () -> leq([z, z]) -> 7  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 7  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 7  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 10  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8  ;  (leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.016105 s (model generation: 0.006398,  model checking: 0.009707):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 8  ;  () -> leq([z, s(nn2)]) -> 8  ;  () -> leq([z, z]) -> 8  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 8  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 8  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 10  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9  ;  (leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 15, which took 0.007432 s (model generation: 0.006694,  model checking: 0.000738):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 9  ;  () -> leq([z, s(nn2)]) -> 9  ;  () -> leq([z, z]) -> 9  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 9  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 9  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 10  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Yes: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 16, which took 0.014991 s (model generation: 0.007616,  model checking: 0.007375):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 10  ;  () -> leq([z, s(nn2)]) -> 10  ;  () -> leq([z, z]) -> 10  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 10  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 10  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 13  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11  ;  (leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.014110 s (model generation: 0.009165,  model checking: 0.004945):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, b>() -> q_gen_297
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, b>() -> q_gen_299
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, b>() -> q_gen_301
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 11  ;  () -> leq([z, s(nn2)]) -> 11  ;  () -> leq([z, z]) -> 11  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 11  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 11  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 13  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 16  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12  ;  (leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Yes: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 18, which took 0.092511 s (model generation: 0.011475,  model checking: 0.081036):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, b>() -> q_gen_297
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, b>() -> q_gen_299
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, b>() -> q_gen_301
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 12  ;  () -> leq([z, s(nn2)]) -> 12  ;  () -> leq([z, z]) -> 12  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 12  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 12  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 16  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 16  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.075044 s (model generation: 0.010123,  model checking: 0.064921):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, b>() -> q_gen_297
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, b>() -> q_gen_299
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, b>() -> q_gen_301
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 13  ;  () -> leq([z, s(nn2)]) -> 13  ;  () -> leq([z, z]) -> 13  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 13  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 13  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 19  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 17  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14  ;  (leq([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.202435 s (model generation: 0.010525,  model checking: 0.191910):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, b>() -> q_gen_297
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, a, b>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, b>() -> q_gen_301
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 14  ;  () -> leq([z, s(nn2)]) -> 14  ;  () -> leq([z, z]) -> 14  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 14  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 14  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 22  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 18  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15  ;  (leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.067043 s (model generation: 0.011247,  model checking: 0.055796):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, nil, a>() -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 15  ;  () -> leq([z, s(nn2)]) -> 15  ;  () -> leq([z, z]) -> 15  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 15  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 15  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 25  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 19  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16  ;  (leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 1.040983 s (model generation: 0.011752,  model checking: 1.029231):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, nil, a>() -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 16  ;  () -> leq([z, s(nn2)]) -> 16  ;  () -> leq([z, z]) -> 16  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 16  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 16  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 28  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 20  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17  ;  (leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.550004 s (model generation: 0.014890,  model checking: 0.535114):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 17  ;  () -> leq([z, s(nn2)]) -> 17  ;  () -> leq([z, z]) -> 17  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 17  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 17  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 31  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 21  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18  ;  (leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 3.223906 s (model generation: 0.018064,  model checking: 3.205842):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<nil, cons, a>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, cons, a>(q_gen_274, q_gen_273) -> q_gen_301
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

}
--
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]) -> 18  ;  () -> leq([z, s(nn2)]) -> 18  ;  () -> leq([z, z]) -> 18  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 18  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 18  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 34  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 22  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19  ;  (leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 25, which took 1.478178 s (model generation: 0.020232,  model checking: 1.457946):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<cons, nil, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, a>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<cons, b, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<cons, b, b>(q_gen_274, q_gen_273) -> q_gen_299
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, cons, a>(q_gen_274, q_gen_273) -> q_gen_301
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> length([nil, z]) -> 19  ;  () -> leq([z, s(nn2)]) -> 19  ;  () -> leq([z, z]) -> 19  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 19  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 19  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 37  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 23  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20  ;  (leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 26, which took 3.109134 s (model generation: 0.024111,  model checking: 3.085023):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<cons, nil, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, a>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<cons, a, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<cons, b, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<cons, a, b>(q_gen_274, q_gen_273) -> q_gen_299
<cons, b, b>(q_gen_274, q_gen_273) -> q_gen_299
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, cons, a>(q_gen_274, q_gen_273) -> q_gen_301
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> length([nil, z]) -> 20  ;  () -> leq([z, s(nn2)]) -> 20  ;  () -> leq([z, z]) -> 20  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 20  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 20  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 40  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 24  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21  ;  (leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 3.124699 s (model generation: 0.034020,  model checking: 3.090679):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<cons, nil, a>(q_gen_274, q_gen_273) -> q_gen_297
<cons, nil, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, a>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<cons, a, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<cons, b, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<cons, a, b>(q_gen_274, q_gen_273) -> q_gen_299
<cons, b, a>(q_gen_274, q_gen_273) -> q_gen_299
<cons, b, b>(q_gen_274, q_gen_273) -> q_gen_299
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, cons, a>(q_gen_274, q_gen_273) -> q_gen_301
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> length([nil, z]) -> 21  ;  () -> leq([z, s(nn2)]) -> 21  ;  () -> leq([z, z]) -> 21  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 21  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 21  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 43  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 25  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22  ;  (leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 1.631215 s (model generation: 0.037463,  model checking: 1.593752):

Model:
|_
{
append -> 
{{{
Q={q_gen_252, q_gen_257, q_gen_258, q_gen_259, q_gen_260, q_gen_273, q_gen_274, q_gen_297, q_gen_298, q_gen_299, q_gen_300, q_gen_301, q_gen_302, q_gen_303},
Q_f={q_gen_252},
Delta=
{
<cons>(q_gen_274, q_gen_273) -> q_gen_273
<nil>() -> q_gen_273
<a>() -> q_gen_274
<b>() -> q_gen_274
<cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_257
<nil, cons>(q_gen_274, q_gen_273) -> q_gen_257
<nil, nil>() -> q_gen_257
<cons, a>(q_gen_274, q_gen_273) -> q_gen_258
<cons, b>(q_gen_274, q_gen_273) -> q_gen_258
<nil, a>() -> q_gen_258
<nil, b>() -> q_gen_258
<a, cons>(q_gen_274, q_gen_273) -> q_gen_259
<a, nil>() -> q_gen_259
<b, cons>(q_gen_274, q_gen_273) -> q_gen_259
<b, nil>() -> q_gen_259
<a, a>() -> q_gen_260
<a, b>() -> q_gen_260
<b, a>() -> q_gen_260
<b, b>() -> q_gen_260
<cons, cons, cons>(q_gen_303, q_gen_302, q_gen_301, q_gen_300, q_gen_299, q_gen_298, q_gen_297, q_gen_252) -> q_gen_252
<cons, nil, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_252
<nil, nil, cons>(q_gen_274, q_gen_273) -> q_gen_252
<nil, nil, nil>() -> q_gen_252
<cons, nil, a>(q_gen_274, q_gen_273) -> q_gen_297
<cons, nil, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, a>(q_gen_274, q_gen_273) -> q_gen_297
<nil, cons, b>(q_gen_274, q_gen_273) -> q_gen_297
<nil, nil, a>() -> q_gen_297
<nil, nil, b>() -> q_gen_297
<cons, a, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<cons, b, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_298
<nil, a, cons>(q_gen_274, q_gen_273) -> q_gen_298
<nil, b, cons>(q_gen_274, q_gen_273) -> q_gen_298
<cons, a, a>(q_gen_274, q_gen_273) -> q_gen_299
<cons, a, b>(q_gen_274, q_gen_273) -> q_gen_299
<cons, b, a>(q_gen_274, q_gen_273) -> q_gen_299
<cons, b, b>(q_gen_274, q_gen_273) -> q_gen_299
<nil, a, a>() -> q_gen_299
<nil, a, b>() -> q_gen_299
<nil, b, a>() -> q_gen_299
<nil, b, b>() -> q_gen_299
<a, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<a, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<b, cons, cons>(q_gen_260, q_gen_259, q_gen_258, q_gen_257) -> q_gen_300
<b, nil, cons>(q_gen_274, q_gen_273) -> q_gen_300
<a, cons, a>(q_gen_274, q_gen_273) -> q_gen_301
<a, nil, a>() -> q_gen_301
<b, cons, b>(q_gen_274, q_gen_273) -> q_gen_301
<b, nil, b>() -> q_gen_301
<a, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, a, cons>(q_gen_274, q_gen_273) -> q_gen_302
<b, b, cons>(q_gen_274, q_gen_273) -> q_gen_302
<a, a, a>() -> q_gen_303
<a, b, a>() -> q_gen_303
<b, a, b>() -> q_gen_303
<b, b, b>() -> q_gen_303
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_251, q_gen_255, q_gen_283},
Q_f={q_gen_251},
Delta=
{
<s>(q_gen_283) -> q_gen_283
<z>() -> q_gen_283
<cons, s>(q_gen_255, q_gen_251) -> q_gen_251
<nil, z>() -> q_gen_251
<a, s>(q_gen_283) -> q_gen_255
<a, z>() -> q_gen_255
<b, s>(q_gen_283) -> q_gen_255
<b, z>() -> q_gen_255
}

Datatype: <eltlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_248, q_gen_250},
Q_f={q_gen_248},
Delta=
{
<s>(q_gen_250) -> q_gen_250
<z>() -> q_gen_250
<s, s>(q_gen_248) -> q_gen_248
<z, s>(q_gen_250) -> q_gen_248
<z, z>() -> q_gen_248
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> length([nil, z]) -> 22  ;  () -> leq([z, s(nn2)]) -> 22  ;  () -> leq([z, z]) -> 22  ;  (append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 22  ;  (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 22  ;  (append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 46  ;  (length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 26  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23  ;  (leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Yes: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

Total time: 30.002678
Reason for stopping: DontKnow. Stopped because: timeout