Solving ../../benchmarks/true/append_length_leq_natlist.smt2...

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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)])}
(append([_tb, _ub, _vb]) /\ append([_tb, _ub, _wb])) -> eq_natlist([_vb, _wb])
)
(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, _xb])) -> length([cons(x, ll), s(_xb)])}
(length([_yb, _ac]) /\ length([_yb, _zb])) -> eq_nat([_zb, _ac])
)
}

properties:
{(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc])}


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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 0  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 0  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.000049 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_387, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_394, q_gen_395, q_gen_396, q_gen_397, q_gen_398, q_gen_402, q_gen_403, q_gen_404, q_gen_405, q_gen_406, q_gen_407, q_gen_408, q_gen_409, q_gen_410, q_gen_411, q_gen_415, q_gen_416, q_gen_417, q_gen_418, q_gen_419, q_gen_420, q_gen_421, q_gen_422, q_gen_425, q_gen_426, q_gen_427, q_gen_428, q_gen_429, q_gen_432, q_gen_433, q_gen_434, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441, q_gen_442, q_gen_443, q_gen_444, q_gen_445, q_gen_446, q_gen_447, q_gen_448, q_gen_449, q_gen_450, q_gen_451, q_gen_452, q_gen_453, q_gen_454, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_459, q_gen_460, q_gen_461, q_gen_462, q_gen_463, q_gen_464, q_gen_465, q_gen_466, q_gen_467, q_gen_468, q_gen_469, q_gen_470, q_gen_471, q_gen_472, q_gen_473, q_gen_474, q_gen_475, q_gen_476, q_gen_477, q_gen_478, q_gen_479, q_gen_480, q_gen_481, q_gen_482, q_gen_483, q_gen_484, q_gen_485, q_gen_486, q_gen_487, q_gen_488, q_gen_489, q_gen_490, q_gen_491, q_gen_492, q_gen_493, q_gen_494, q_gen_495, q_gen_496, q_gen_497, q_gen_498, q_gen_499, q_gen_500, q_gen_501, q_gen_502, q_gen_503, q_gen_504, q_gen_505, q_gen_506, q_gen_507, q_gen_508, q_gen_509, q_gen_510, q_gen_511, q_gen_512, q_gen_513, q_gen_514, q_gen_515, q_gen_516, q_gen_517, q_gen_518, q_gen_519, q_gen_520},
Q_f={},
Delta=
{
<z>() -> q_gen_396
<s>(q_gen_396) -> q_gen_404
<nil>() -> q_gen_410
<cons>(q_gen_396, q_gen_410) -> q_gen_421
<nil, nil>() -> q_gen_388
<nil, z>() -> q_gen_389
<z, nil>() -> q_gen_390
<z, z>() -> q_gen_391
<nil, s>(q_gen_396) -> q_gen_395
<s, nil>(q_gen_396) -> q_gen_397
<s, s>(q_gen_391) -> q_gen_398
<nil, s>(q_gen_404) -> q_gen_403
<s, nil>(q_gen_404) -> q_gen_405
<s, s>(q_gen_398) -> q_gen_406
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_408
<cons, z>(q_gen_396, q_gen_410) -> q_gen_409
<z, cons>(q_gen_396, q_gen_410) -> q_gen_411
<cons, s>(q_gen_391, q_gen_389) -> q_gen_416
<s, cons>(q_gen_391, q_gen_390) -> q_gen_417
<cons, cons>(q_gen_391, q_gen_411, q_gen_409, q_gen_408) -> q_gen_419
<cons, z>(q_gen_396, q_gen_421) -> q_gen_420
<z, cons>(q_gen_396, q_gen_421) -> q_gen_422
<cons, s>(q_gen_427, q_gen_395) -> q_gen_426
<z, s>(q_gen_396) -> q_gen_427
<s, cons>(q_gen_429, q_gen_397) -> q_gen_428
<s, z>(q_gen_396) -> q_gen_429
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_443
<s, z>(q_gen_404) -> q_gen_472
<s, s>(q_gen_429) -> q_gen_492
<nil, nil, nil>() -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_387
<nil, cons, cons>(q_gen_398, q_gen_397, q_gen_395, q_gen_388) -> q_gen_394
<cons, nil, cons>(q_gen_406, q_gen_405, q_gen_403, q_gen_388) -> q_gen_402
<nil, cons, cons>(q_gen_391, q_gen_411, q_gen_409, q_gen_408) -> q_gen_407
<cons, nil, cons>(q_gen_398, q_gen_417, q_gen_416, q_gen_408) -> q_gen_415
<nil, cons, cons>(q_gen_391, q_gen_422, q_gen_420, q_gen_419) -> q_gen_418
<cons, nil, cons>(q_gen_406, q_gen_428, q_gen_426, q_gen_408) -> q_gen_425
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_432
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_434) -> q_gen_433
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_434
<nil, nil, z>() -> q_gen_435
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, z, z>() -> q_gen_437
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<z, nil, z>() -> q_gen_439
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, z>() -> q_gen_441
<cons, nil, cons>(q_gen_391, q_gen_411, q_gen_389, q_gen_443) -> q_gen_442
<nil, cons, cons>(q_gen_429, q_gen_397, q_gen_389, q_gen_388) -> q_gen_444
<cons, cons, cons>(q_gen_454, q_gen_451, q_gen_450, q_gen_449, q_gen_448, q_gen_447, q_gen_446, q_gen_434) -> q_gen_445
<nil, nil, s>(q_gen_404) -> q_gen_446
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_447
<nil, s, s>(q_gen_427) -> q_gen_448
<s, nil, cons>(q_gen_429, q_gen_397) -> q_gen_449
<s, nil, s>(q_gen_398) -> q_gen_450
<s, s, cons>(q_gen_453, q_gen_452) -> q_gen_451
<s, z, nil>(q_gen_396) -> q_gen_452
<s, z, z>(q_gen_396) -> q_gen_453
<s, s, s>(q_gen_455) -> q_gen_454
<s, z, s>(q_gen_391) -> q_gen_455
<cons, cons, cons>(q_gen_455, q_gen_461, q_gen_460, q_gen_459, q_gen_458, q_gen_436, q_gen_457, q_gen_434) -> q_gen_456
<nil, nil, s>(q_gen_396) -> q_gen_457
<nil, z, s>(q_gen_396) -> q_gen_458
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_459
<s, nil, s>(q_gen_391) -> q_gen_460
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_461
<cons, cons, cons>(q_gen_466, q_gen_464, q_gen_460, q_gen_459, q_gen_463, q_gen_447, q_gen_457, q_gen_434) -> q_gen_462
<nil, s, s>(q_gen_391) -> q_gen_463
<s, s, cons>(q_gen_441, q_gen_465) -> q_gen_464
<z, z, nil>() -> q_gen_465
<s, s, s>(q_gen_441) -> q_gen_466
<cons, cons, cons>(q_gen_470, q_gen_469, q_gen_439, q_gen_438, q_gen_468, q_gen_447, q_gen_435, q_gen_434) -> q_gen_467
<nil, s, z>(q_gen_396) -> q_gen_468
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_469
<z, s, z>(q_gen_396) -> q_gen_470
<nil, cons, cons>(q_gen_472, q_gen_405, q_gen_389, q_gen_388) -> q_gen_471
<cons, cons, cons>(q_gen_478, q_gen_476, q_gen_460, q_gen_459, q_gen_475, q_gen_474, q_gen_457, q_gen_434) -> q_gen_473
<nil, s, cons>(q_gen_429, q_gen_397) -> q_gen_474
<nil, s, s>(q_gen_429) -> q_gen_475
<s, s, cons>(q_gen_470, q_gen_477) -> q_gen_476
<z, s, nil>(q_gen_396) -> q_gen_477
<s, s, s>(q_gen_470) -> q_gen_478
<cons, cons, cons>(q_gen_484, q_gen_481, q_gen_450, q_gen_449, q_gen_480, q_gen_474, q_gen_446, q_gen_434) -> q_gen_479
<nil, s, s>(q_gen_398) -> q_gen_480
<s, s, cons>(q_gen_483, q_gen_482) -> q_gen_481
<s, s, nil>(q_gen_391) -> q_gen_482
<s, s, z>(q_gen_391) -> q_gen_483
<s, s, s>(q_gen_466) -> q_gen_484
<cons, cons, cons>(q_gen_466, q_gen_489, q_gen_460, q_gen_488, q_gen_463, q_gen_487, q_gen_457, q_gen_486) -> q_gen_485
<nil, nil, cons>(q_gen_404, q_gen_410) -> q_gen_486
<nil, s, cons>(q_gen_427, q_gen_390) -> q_gen_487
<s, nil, cons>(q_gen_427, q_gen_390) -> q_gen_488
<s, s, cons>(q_gen_490, q_gen_465) -> q_gen_489
<z, z, s>(q_gen_396) -> q_gen_490
<nil, cons, cons>(q_gen_492, q_gen_405, q_gen_395, q_gen_388) -> q_gen_491
<cons, cons, cons>(q_gen_478, q_gen_495, q_gen_460, q_gen_488, q_gen_475, q_gen_494, q_gen_457, q_gen_486) -> q_gen_493
<nil, s, cons>(q_gen_398, q_gen_397) -> q_gen_494
<s, s, cons>(q_gen_496, q_gen_477) -> q_gen_495
<z, s, s>(q_gen_391) -> q_gen_496
<cons, cons, cons>(q_gen_441, q_gen_503, q_gen_502, q_gen_501, q_gen_437, q_gen_500, q_gen_499, q_gen_498) -> q_gen_497
<nil, cons, cons>(q_gen_391, q_gen_411, q_gen_389, q_gen_443) -> q_gen_498
<nil, cons, z>(q_gen_396, q_gen_410) -> q_gen_499
<nil, z, cons>(q_gen_396, q_gen_421) -> q_gen_500
<z, cons, cons>(q_gen_391, q_gen_411, q_gen_389, q_gen_443) -> q_gen_501
<z, cons, z>(q_gen_396, q_gen_410) -> q_gen_502
<z, z, cons>(q_gen_396, q_gen_421) -> q_gen_503
<cons, cons, cons>(q_gen_441, q_gen_503, q_gen_439, q_gen_508, q_gen_507, q_gen_506, q_gen_505, q_gen_442) -> q_gen_504
<cons, nil, z>(q_gen_396, q_gen_410) -> q_gen_505
<cons, z, cons>(q_gen_391, q_gen_411, q_gen_389, q_gen_443) -> q_gen_506
<cons, z, z>(q_gen_396, q_gen_410) -> q_gen_507
<z, nil, cons>(q_gen_396, q_gen_421) -> q_gen_508
<cons, cons, cons>(q_gen_455, q_gen_513, q_gen_460, q_gen_512, q_gen_511, q_gen_506, q_gen_510, q_gen_442) -> q_gen_509
<cons, nil, s>(q_gen_391, q_gen_389) -> q_gen_510
<cons, z, s>(q_gen_391, q_gen_389) -> q_gen_511
<s, nil, cons>(q_gen_391, q_gen_411) -> q_gen_512
<s, z, cons>(q_gen_391, q_gen_411) -> q_gen_513
<cons, cons, cons>(q_gen_470, q_gen_517, q_gen_439, q_gen_508, q_gen_516, q_gen_515, q_gen_505, q_gen_442) -> q_gen_514
<cons, s, cons>(q_gen_441, q_gen_440, q_gen_437, q_gen_436) -> q_gen_515
<cons, s, z>(q_gen_391, q_gen_389) -> q_gen_516
<z, s, cons>(q_gen_391, q_gen_411) -> q_gen_517
<cons, cons, cons>(q_gen_466, q_gen_520, q_gen_460, q_gen_512, q_gen_519, q_gen_515, q_gen_510, q_gen_442) -> q_gen_518
<cons, s, s>(q_gen_441, q_gen_437) -> q_gen_519
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_520
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_385, q_gen_386, q_gen_399, q_gen_400, q_gen_401, q_gen_412, q_gen_413, q_gen_414, q_gen_423, q_gen_424, q_gen_430, q_gen_431},
Q_f={},
Delta=
{
<z>() -> q_gen_401
<s>(q_gen_401) -> q_gen_414
<nil, z>() -> q_gen_382
<cons, s>(q_gen_386, q_gen_382) -> q_gen_385
<z, z>() -> q_gen_386
<cons, s>(q_gen_400, q_gen_382) -> q_gen_399
<s, z>(q_gen_401) -> q_gen_400
<cons, s>(q_gen_413, q_gen_382) -> q_gen_412
<s, z>(q_gen_414) -> q_gen_413
<cons, s>(q_gen_424, q_gen_385) -> q_gen_423
<s, s>(q_gen_386) -> q_gen_424
<cons, s>(q_gen_431, q_gen_385) -> q_gen_430
<z, s>(q_gen_401) -> q_gen_431
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_380, q_gen_381, q_gen_384, q_gen_392, q_gen_393},
Q_f={},
Delta=
{
<z>() -> q_gen_381
<s>(q_gen_381) -> q_gen_393
<z, z>() -> q_gen_379
<z, s>(q_gen_381) -> q_gen_380
<s, s>(q_gen_379) -> q_gen_384
<z, s>(q_gen_393) -> q_gen_392
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004366 s (model generation: 0.003903,  model checking: 0.000463):

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

}

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

}

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

}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.003589 s (model generation: 0.003542,  model checking: 0.000047):

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

}

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

}

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

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.003408 s (model generation: 0.003367,  model checking: 0.000041):

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

}

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

}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.003923 s (model generation: 0.003451,  model checking: 0.000472):

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

}

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

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.003467 s (model generation: 0.003388,  model checking: 0.000079):

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

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

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.004589 s (model generation: 0.004227,  model checking: 0.000362):

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

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

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> z  ;  ll -> nil  ;  x -> z
})

-------------------------------------------
Step 6, which took 0.006076 s (model generation: 0.005653,  model checking: 0.000423):

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

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386},
Q_f={q_gen_382},
Delta=
{
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009775 s (model generation: 0.008447,  model checking: 0.001328):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_383},
Delta=
{
<nil, nil>() -> q_gen_388
<nil, z>() -> q_gen_389
<z, nil>() -> q_gen_390
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386},
Q_f={q_gen_382},
Delta=
{
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 2  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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.025933 s (model generation: 0.011076,  model checking: 0.014857):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391},
Q_f={q_gen_383},
Delta=
{
<nil, nil>() -> q_gen_388
<nil, z>() -> q_gen_389
<z, nil>() -> q_gen_390
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386},
Q_f={q_gen_382},
Delta=
{
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 3  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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(s(z), nil)
})

-------------------------------------------
Step 9, which took 0.004812 s (model generation: 0.004521,  model checking: 0.000291):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396},
Q_f={q_gen_383},
Delta=
{
<z>() -> q_gen_396
<nil, nil>() -> q_gen_388
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, nil>(q_gen_396) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386},
Q_f={q_gen_382},
Delta=
{
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 4  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> z  ;  ll -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 10, which took 0.005898 s (model generation: 0.004400,  model checking: 0.001498):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396},
Q_f={q_gen_383},
Delta=
{
<z>() -> q_gen_396
<nil, nil>() -> q_gen_388
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, nil>(q_gen_396) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 4  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 7  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> nil  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.030198 s (model generation: 0.005640,  model checking: 0.024558):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<nil, nil>() -> q_gen_388
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, nil>(q_gen_396) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 5  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 7  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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(z, cons(z, nil))
})

-------------------------------------------
Step 12, which took 0.005840 s (model generation: 0.005459,  model checking: 0.000381):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 6  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 7  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> z  ;  ll -> nil  ;  x -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.008876 s (model generation: 0.005234,  model checking: 0.003642):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 7  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 10  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 14, which took 0.042809 s (model generation: 0.005565,  model checking: 0.037244):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 8  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 10  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 15, which took 0.007188 s (model generation: 0.006757,  model checking: 0.000431):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 9  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 10  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> s(z)  ;  ll -> cons(z, nil)  ;  x -> s(z)
})

-------------------------------------------
Step 16, which took 0.010411 s (model generation: 0.006373,  model checking: 0.004038):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 10  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 13  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 17, which took 0.008573 s (model generation: 0.007189,  model checking: 0.001384):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 11  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 13  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> s(z)  ;  ll -> cons(z, nil)  ;  x -> z
})

-------------------------------------------
Step 18, which took 0.013919 s (model generation: 0.008418,  model checking: 0.005501):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 12  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 16  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.042330 s (model generation: 0.011840,  model checking: 0.030490):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, z>() -> q_gen_435
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, z, z>() -> q_gen_437
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<z, nil, z>() -> q_gen_439
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 13  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 19  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.545806 s (model generation: 0.009130,  model checking: 0.536676):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, z>() -> q_gen_435
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, z, z>() -> q_gen_437
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<z, nil, z>() -> q_gen_439
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 14  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 22  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.164776 s (model generation: 0.010732,  model checking: 0.154044):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 15  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 25  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.167977 s (model generation: 0.011550,  model checking: 0.156427):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 16  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 28  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.210683 s (model generation: 0.012886,  model checking: 0.197797):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 17  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 31  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.167233 s (model generation: 0.013252,  model checking: 0.153981):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 18  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 34  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.385206 s (model generation: 0.016024,  model checking: 0.369182):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 19  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 37  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.554803 s (model generation: 0.018058,  model checking: 0.536745):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 20  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 40  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.543953 s (model generation: 0.021253,  model checking: 0.522700):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 21  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 43  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 28, which took 0.567407 s (model generation: 0.025325,  model checking: 0.542082):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, s>(q_gen_391) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

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, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 22  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 46  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, cons(z, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 1.676846 s (model generation: 0.026811,  model checking: 1.650035):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<nil, cons, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, cons, z>(q_gen_396, q_gen_410) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, s>(q_gen_391) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> length([nil, z]) -> 23  ;  () -> leq([z, s(nn2)]) -> 23  ;  () -> leq([z, z]) -> 23  ;  (append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 23  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 49  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 27  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24  ;  (leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Yes: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 30, which took 1.545559 s (model generation: 0.039191,  model checking: 1.506368):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<cons, nil, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, cons, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<cons, z, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_436
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<cons, z, z>(q_gen_396, q_gen_410) -> q_gen_437
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, cons, z>(q_gen_396, q_gen_410) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, s>(q_gen_391) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> length([nil, z]) -> 24  ;  () -> leq([z, s(nn2)]) -> 24  ;  () -> leq([z, z]) -> 24  ;  (append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 24  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 52  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 28  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25  ;  (leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Yes: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 31, which took 10.973050 s (model generation: 0.040078,  model checking: 10.932972):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<cons, nil, s>(q_gen_391, q_gen_389) -> q_gen_435
<cons, nil, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, cons, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<cons, z, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_436
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<cons, z, s>(q_gen_391, q_gen_389) -> q_gen_437
<cons, z, z>(q_gen_396, q_gen_410) -> q_gen_437
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, cons, z>(q_gen_396, q_gen_410) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, s>(q_gen_391) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26  ;  () -> length([nil, z]) -> 25  ;  () -> leq([z, s(nn2)]) -> 25  ;  () -> leq([z, z]) -> 25  ;  (append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 25  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 55  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 29  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26  ;  (leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Yes: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 32, which took 10.844603 s (model generation: 0.042300,  model checking: 10.802303):

Model:
|_
{
append -> 
{{{
Q={q_gen_383, q_gen_388, q_gen_389, q_gen_390, q_gen_391, q_gen_396, q_gen_410, q_gen_435, q_gen_436, q_gen_437, q_gen_438, q_gen_439, q_gen_440, q_gen_441},
Q_f={q_gen_383},
Delta=
{
<s>(q_gen_396) -> q_gen_396
<z>() -> q_gen_396
<cons>(q_gen_396, q_gen_410) -> q_gen_410
<nil>() -> q_gen_410
<cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_388
<nil, cons>(q_gen_396, q_gen_410) -> q_gen_388
<nil, nil>() -> q_gen_388
<cons, s>(q_gen_391, q_gen_389) -> q_gen_389
<cons, z>(q_gen_396, q_gen_410) -> q_gen_389
<nil, s>(q_gen_396) -> q_gen_389
<nil, z>() -> q_gen_389
<s, cons>(q_gen_391, q_gen_390) -> q_gen_390
<s, nil>(q_gen_396) -> q_gen_390
<z, cons>(q_gen_396, q_gen_410) -> q_gen_390
<z, nil>() -> q_gen_390
<s, s>(q_gen_391) -> q_gen_391
<s, z>(q_gen_396) -> q_gen_391
<z, s>(q_gen_396) -> q_gen_391
<z, z>() -> q_gen_391
<cons, cons, cons>(q_gen_441, q_gen_440, q_gen_439, q_gen_438, q_gen_437, q_gen_436, q_gen_435, q_gen_383) -> q_gen_383
<cons, nil, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_383
<nil, nil, cons>(q_gen_396, q_gen_410) -> q_gen_383
<nil, nil, nil>() -> q_gen_383
<cons, nil, s>(q_gen_391, q_gen_389) -> q_gen_435
<cons, nil, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, cons, z>(q_gen_396, q_gen_410) -> q_gen_435
<nil, nil, s>(q_gen_396) -> q_gen_435
<nil, nil, z>() -> q_gen_435
<cons, s, cons>(q_gen_441, q_gen_440, q_gen_437, q_gen_436) -> q_gen_436
<cons, z, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_436
<nil, s, cons>(q_gen_391, q_gen_390) -> q_gen_436
<nil, z, cons>(q_gen_396, q_gen_410) -> q_gen_436
<cons, s, z>(q_gen_391, q_gen_389) -> q_gen_437
<cons, z, s>(q_gen_391, q_gen_389) -> q_gen_437
<cons, z, z>(q_gen_396, q_gen_410) -> q_gen_437
<nil, s, s>(q_gen_391) -> q_gen_437
<nil, s, z>(q_gen_396) -> q_gen_437
<nil, z, s>(q_gen_396) -> q_gen_437
<nil, z, z>() -> q_gen_437
<s, nil, cons>(q_gen_391, q_gen_390) -> q_gen_438
<z, cons, cons>(q_gen_391, q_gen_390, q_gen_389, q_gen_388) -> q_gen_438
<z, nil, cons>(q_gen_396, q_gen_410) -> q_gen_438
<s, nil, s>(q_gen_391) -> q_gen_439
<z, cons, z>(q_gen_396, q_gen_410) -> q_gen_439
<z, nil, z>() -> q_gen_439
<s, s, cons>(q_gen_441, q_gen_440) -> q_gen_440
<s, s, nil>(q_gen_391) -> q_gen_440
<s, z, cons>(q_gen_391, q_gen_390) -> q_gen_440
<s, z, nil>(q_gen_396) -> q_gen_440
<z, s, cons>(q_gen_391, q_gen_390) -> q_gen_440
<z, s, nil>(q_gen_396) -> q_gen_440
<z, z, cons>(q_gen_396, q_gen_410) -> q_gen_440
<z, z, nil>() -> q_gen_440
<s, s, s>(q_gen_441) -> q_gen_441
<s, s, z>(q_gen_391) -> q_gen_441
<s, z, s>(q_gen_391) -> q_gen_441
<s, z, z>(q_gen_396) -> q_gen_441
<z, s, s>(q_gen_391) -> q_gen_441
<z, s, z>(q_gen_396) -> q_gen_441
<z, z, s>(q_gen_396) -> q_gen_441
<z, z, z>() -> q_gen_441
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_382, q_gen_386, q_gen_401},
Q_f={q_gen_382},
Delta=
{
<s>(q_gen_401) -> q_gen_401
<z>() -> q_gen_401
<cons, s>(q_gen_386, q_gen_382) -> q_gen_382
<nil, z>() -> q_gen_382
<s, s>(q_gen_386) -> q_gen_386
<s, z>(q_gen_401) -> q_gen_386
<z, s>(q_gen_401) -> q_gen_386
<z, z>() -> q_gen_386
}

Datatype: <natlist, nat>
Convolution form: complete
}}}
  ;  leq -> 
{{{
Q={q_gen_379, q_gen_381},
Q_f={q_gen_379},
Delta=
{
<s>(q_gen_381) -> q_gen_381
<z>() -> q_gen_381
<s, s>(q_gen_379) -> q_gen_379
<z, s>(q_gen_381) -> q_gen_379
<z, z>() -> q_gen_379
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27  ;  () -> length([nil, z]) -> 26  ;  () -> leq([z, s(nn2)]) -> 26  ;  () -> leq([z, z]) -> 26  ;  (append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 26  ;  (append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 58  ;  (length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 30  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27  ;  (leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Yes: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, nil)
})

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