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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(butlast, F:
{() -> butlast([cons(y, nil), nil])
() -> butlast([nil, nil])
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)])}
(butlast([_af, _bf]) /\ butlast([_af, _cf])) -> eq_eltlist([_bf, _cf])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)])}
(append([_ef, _ff, _gf]) /\ append([_ef, _ff, _hf])) -> eq_eltlist([_gf, _hf])
)
}

properties:
{(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys])}


over-approximation: {append, butlast}
under-approximation: {}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> butlast([cons(y, nil), nil]) -> 0
() -> butlast([nil, nil]) -> 0
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 0
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 0
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 0
}


Solving took 64.766361 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1325, q_gen_1326, q_gen_1330, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1339, q_gen_1340, q_gen_1341, q_gen_1342, q_gen_1343, q_gen_1344, q_gen_1345, q_gen_1346, q_gen_1347, q_gen_1348, q_gen_1349, q_gen_1350, q_gen_1351, q_gen_1352, q_gen_1353, q_gen_1354, q_gen_1356, q_gen_1357, q_gen_1358, q_gen_1359, q_gen_1360, q_gen_1361, q_gen_1363, q_gen_1364, q_gen_1365, q_gen_1366, q_gen_1368, q_gen_1369, q_gen_1370, q_gen_1371, q_gen_1375, q_gen_1376, q_gen_1377, q_gen_1378, q_gen_1379, q_gen_1380, q_gen_1381, q_gen_1382, q_gen_1383, q_gen_1384, q_gen_1385, q_gen_1386, q_gen_1387, q_gen_1388, q_gen_1389, q_gen_1390, q_gen_1391, q_gen_1392, q_gen_1393, q_gen_1394, q_gen_1395, q_gen_1396, q_gen_1397, q_gen_1398, q_gen_1399, q_gen_1400, q_gen_1401, q_gen_1402, q_gen_1403, q_gen_1404, q_gen_1405, q_gen_1406, q_gen_1407, q_gen_1408, q_gen_1409, q_gen_1410, q_gen_1411, q_gen_1412, q_gen_1413, q_gen_1414, q_gen_1415, q_gen_1416, q_gen_1417, q_gen_1418, q_gen_1419, q_gen_1420, q_gen_1421, q_gen_1422, q_gen_1423, q_gen_1424, q_gen_1427, q_gen_1428, q_gen_1429, q_gen_1430, q_gen_1431, q_gen_1432, q_gen_1433, q_gen_1434, q_gen_1435, q_gen_1436, q_gen_1437, q_gen_1438, q_gen_1439, q_gen_1440, q_gen_1441, q_gen_1442, q_gen_1443, q_gen_1444, q_gen_1445, q_gen_1446, q_gen_1447, q_gen_1448, q_gen_1449, q_gen_1450, q_gen_1451, q_gen_1452, q_gen_1453, q_gen_1454, q_gen_1455, q_gen_1456, q_gen_1457, q_gen_1458, q_gen_1459, q_gen_1461, q_gen_1462, q_gen_1463, q_gen_1464},
Q_f={},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<a>() -> q_gen_1351
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons>(q_gen_1334, q_gen_1360) -> q_gen_1464
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1325
<a, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons>(q_gen_1321, q_gen_1377) -> q_gen_1376
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1377
<nil, cons>(q_gen_1351, q_gen_1333) -> q_gen_1385
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1400
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1412
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1428
<cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1430
<cons, cons>(q_gen_1386, q_gen_1385) -> q_gen_1433
<cons, cons>(q_gen_1400, q_gen_1320) -> q_gen_1441
<cons, cons>(q_gen_1400, q_gen_1341) -> q_gen_1446
<cons, cons>(q_gen_1321, q_gen_1446) -> q_gen_1450
<cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1453
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1457
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1326, q_gen_1325) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1330
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, cons, cons>(q_gen_1335, q_gen_1340) -> q_gen_1339
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1340
<cons, cons, cons>(q_gen_1343, q_gen_1332) -> q_gen_1342
<a, b, a>() -> q_gen_1343
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1344
<cons, cons, cons>(q_gen_1335, q_gen_1346) -> q_gen_1345
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1346
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1348
<cons, cons, cons>(q_gen_1352, q_gen_1350) -> q_gen_1349
<nil, nil, cons>(q_gen_1351, q_gen_1333) -> q_gen_1350
<b, a, b>() -> q_gen_1352
<cons, cons, cons>(q_gen_1354, q_gen_1350) -> q_gen_1353
<a, a, a>() -> q_gen_1354
<cons, cons, cons>(q_gen_1343, q_gen_1344) -> q_gen_1356
<cons, cons, cons>(q_gen_1343, q_gen_1358) -> q_gen_1357
<cons, cons, cons>(q_gen_1343, q_gen_1359) -> q_gen_1358
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1359
<cons, cons, cons>(q_gen_1335, q_gen_1359) -> q_gen_1361
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1363
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1365
<cons, cons, cons>(q_gen_1335, q_gen_1363) -> q_gen_1366
<cons, cons, cons>(q_gen_1335, q_gen_1369) -> q_gen_1368
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1369
<cons, cons, cons>(q_gen_1343, q_gen_1371) -> q_gen_1370
<cons, cons, cons>(q_gen_1335, q_gen_1365) -> q_gen_1371
<nil, cons, cons>(q_gen_1321, q_gen_1376) -> q_gen_1375
<cons, cons, cons>(q_gen_1352, q_gen_1379) -> q_gen_1378
<cons, cons, cons>(q_gen_1343, q_gen_1330) -> q_gen_1379
<cons, cons, cons>(q_gen_1354, q_gen_1381) -> q_gen_1380
<cons, cons, cons>(q_gen_1335, q_gen_1342) -> q_gen_1381
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1382
<cons, cons, cons>(q_gen_1335, q_gen_1384) -> q_gen_1383
<nil, cons, cons>(q_gen_1386, q_gen_1385) -> q_gen_1384
<cons, cons, cons>(q_gen_1335, q_gen_1388) -> q_gen_1387
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1388
<nil, cons, cons>(q_gen_1321, q_gen_1377) -> q_gen_1389
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1390
<cons, nil, cons>(q_gen_1321, q_gen_1385) -> q_gen_1391
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1392
<cons, cons, cons>(q_gen_1335, q_gen_1394) -> q_gen_1393
<cons, cons, cons>(q_gen_1343, q_gen_1389) -> q_gen_1394
<cons, cons, cons>(q_gen_1335, q_gen_1396) -> q_gen_1395
<cons, cons, cons>(q_gen_1335, q_gen_1356) -> q_gen_1396
<nil, cons, cons>(q_gen_1326, q_gen_1377) -> q_gen_1397
<cons, cons, cons>(q_gen_1354, q_gen_1399) -> q_gen_1398
<nil, cons, cons>(q_gen_1400, q_gen_1341) -> q_gen_1399
<cons, cons, cons>(q_gen_1354, q_gen_1402) -> q_gen_1401
<cons, cons, cons>(q_gen_1343, q_gen_1316) -> q_gen_1402
<cons, cons, cons>(q_gen_1354, q_gen_1404) -> q_gen_1403
<cons, cons, cons>(q_gen_1343, q_gen_1405) -> q_gen_1404
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1405
<cons, cons, cons>(q_gen_1354, q_gen_1407) -> q_gen_1406
<cons, cons, cons>(q_gen_1352, q_gen_1408) -> q_gen_1407
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1408
<cons, cons, cons>(q_gen_1354, q_gen_1410) -> q_gen_1409
<cons, cons, cons>(q_gen_1354, q_gen_1411) -> q_gen_1410
<cons, nil, cons>(q_gen_1321, q_gen_1412) -> q_gen_1411
<cons, cons, cons>(q_gen_1354, q_gen_1414) -> q_gen_1413
<cons, cons, cons>(q_gen_1354, q_gen_1408) -> q_gen_1414
<cons, cons, cons>(q_gen_1354, q_gen_1416) -> q_gen_1415
<cons, cons, cons>(q_gen_1354, q_gen_1417) -> q_gen_1416
<cons, nil, cons>(q_gen_1326, q_gen_1412) -> q_gen_1417
<cons, cons, cons>(q_gen_1335, q_gen_1419) -> q_gen_1418
<cons, nil, cons>(q_gen_1400, q_gen_1320) -> q_gen_1419
<cons, cons, cons>(q_gen_1335, q_gen_1421) -> q_gen_1420
<cons, nil, cons>(q_gen_1321, q_gen_1377) -> q_gen_1421
<cons, cons, cons>(q_gen_1354, q_gen_1332) -> q_gen_1422
<cons, cons, cons>(q_gen_1335, q_gen_1424) -> q_gen_1423
<cons, nil, cons>(q_gen_1400, q_gen_1341) -> q_gen_1424
<cons, nil, cons>(q_gen_1321, q_gen_1428) -> q_gen_1427
<nil, cons, cons>(q_gen_1321, q_gen_1430) -> q_gen_1429
<cons, cons, cons>(q_gen_1343, q_gen_1432) -> q_gen_1431
<nil, cons, cons>(q_gen_1321, q_gen_1433) -> q_gen_1432
<cons, cons, cons>(q_gen_1343, q_gen_1369) -> q_gen_1434
<cons, cons, cons>(q_gen_1335, q_gen_1427) -> q_gen_1435
<cons, cons, cons>(q_gen_1335, q_gen_1437) -> q_gen_1436
<cons, cons, cons>(q_gen_1352, q_gen_1419) -> q_gen_1437
<cons, cons, cons>(q_gen_1343, q_gen_1439) -> q_gen_1438
<cons, cons, cons>(q_gen_1352, q_gen_1440) -> q_gen_1439
<cons, nil, cons>(q_gen_1321, q_gen_1441) -> q_gen_1440
<cons, cons, cons>(q_gen_1335, q_gen_1440) -> q_gen_1442
<cons, cons, cons>(q_gen_1352, q_gen_1444) -> q_gen_1443
<cons, cons, cons>(q_gen_1352, q_gen_1445) -> q_gen_1444
<cons, nil, cons>(q_gen_1321, q_gen_1446) -> q_gen_1445
<cons, cons, cons>(q_gen_1354, q_gen_1448) -> q_gen_1447
<cons, cons, cons>(q_gen_1352, q_gen_1449) -> q_gen_1448
<cons, nil, cons>(q_gen_1321, q_gen_1450) -> q_gen_1449
<cons, cons, cons>(q_gen_1335, q_gen_1452) -> q_gen_1451
<nil, cons, cons>(q_gen_1321, q_gen_1453) -> q_gen_1452
<cons, cons, cons>(q_gen_1335, q_gen_1455) -> q_gen_1454
<cons, cons, cons>(q_gen_1335, q_gen_1456) -> q_gen_1455
<nil, cons, cons>(q_gen_1321, q_gen_1457) -> q_gen_1456
<cons, cons, cons>(q_gen_1335, q_gen_1459) -> q_gen_1458
<cons, nil, cons>(q_gen_1321, q_gen_1457) -> q_gen_1459
<cons, cons, cons>(q_gen_1343, q_gen_1462) -> q_gen_1461
<cons, cons, cons>(q_gen_1335, q_gen_1463) -> q_gen_1462
<nil, nil, cons>(q_gen_1334, q_gen_1464) -> q_gen_1463
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1317, q_gen_1318, q_gen_1322, q_gen_1323, q_gen_1327, q_gen_1328, q_gen_1329, q_gen_1336, q_gen_1337, q_gen_1355, q_gen_1362, q_gen_1367, q_gen_1372, q_gen_1373, q_gen_1374, q_gen_1425, q_gen_1426, q_gen_1460, q_gen_1465},
Q_f={},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<a>() -> q_gen_1323
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1317
<b, b>() -> q_gen_1318
<cons, nil>(q_gen_1323, q_gen_1314) -> q_gen_1322
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1329, q_gen_1327) -> q_gen_1328
<a, a>() -> q_gen_1329
<cons, cons>(q_gen_1318, q_gen_1322) -> q_gen_1336
<cons, cons>(q_gen_1318, q_gen_1336) -> q_gen_1337
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1355
<cons, cons>(q_gen_1318, q_gen_1317) -> q_gen_1362
<cons, cons>(q_gen_1318, q_gen_1362) -> q_gen_1367
<cons, cons>(q_gen_1318, q_gen_1373) -> q_gen_1372
<cons, cons>(q_gen_1329, q_gen_1322) -> q_gen_1373
<cons, cons>(q_gen_1318, q_gen_1372) -> q_gen_1374
<cons, cons>(q_gen_1318, q_gen_1426) -> q_gen_1425
<cons, cons>(q_gen_1329, q_gen_1313) -> q_gen_1426
<cons, cons>(q_gen_1318, q_gen_1367) -> q_gen_1460
<cons, cons>(q_gen_1318, q_gen_1425) -> q_gen_1465
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008028 s (model generation: 0.007791,  model checking: 0.000237):

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

}

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

}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> butlast([cons(y, nil), nil]) -> 0
() -> butlast([nil, nil]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 1
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 1
}
Sat witness: Found: (() -> butlast([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.008075 s (model generation: 0.007430,  model checking: 0.000645):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312},
Q_f={q_gen_1312},
Delta=
{
<nil, nil>() -> q_gen_1312
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> butlast([cons(y, nil), nil]) -> 3
() -> butlast([nil, nil]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 1
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 1
}
Sat witness: Found: (() -> butlast([cons(y, nil), nil]), {
y -> b
})

-------------------------------------------
Step 2, which took 0.007626 s (model generation: 0.007486,  model checking: 0.000140):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> butlast([cons(y, nil), nil]) -> 3
() -> butlast([nil, nil]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 1
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.007695 s (model generation: 0.007519,  model checking: 0.000176):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> butlast([cons(y, nil), nil]) -> 3
() -> butlast([nil, nil]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 1
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 1
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 4
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> nil  ;  x2 -> b  ;  x3 -> nil  ;  y -> b
})

-------------------------------------------
Step 4, which took 0.008349 s (model generation: 0.008113,  model checking: 0.000236):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> butlast([cons(y, nil), nil]) -> 3
() -> butlast([nil, nil]) -> 3
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 2
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.009426 s (model generation: 0.008068,  model checking: 0.001358):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321},
Q_f={q_gen_1316},
Delta=
{
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> butlast([cons(y, nil), nil]) -> 6
() -> butlast([nil, nil]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 3
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 4
}
Sat witness: Found: (() -> butlast([cons(y, nil), nil]), {
y -> a
})

-------------------------------------------
Step 6, which took 0.009317 s (model generation: 0.008765,  model checking: 0.000552):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321},
Q_f={q_gen_1316},
Delta=
{
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> butlast([cons(y, nil), nil]) -> 6
() -> butlast([nil, nil]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 4
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 7, which took 0.009598 s (model generation: 0.008719,  model checking: 0.000879):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321},
Q_f={q_gen_1316},
Delta=
{
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> butlast([cons(y, nil), nil]) -> 6
() -> butlast([nil, nil]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 4
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 7
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> cons(b, nil)  ;  x2 -> b  ;  x3 -> nil  ;  y -> a
})

-------------------------------------------
Step 8, which took 0.009641 s (model generation: 0.009503,  model checking: 0.000138):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321},
Q_f={q_gen_1316},
Delta=
{
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> butlast([cons(y, nil), nil]) -> 6
() -> butlast([nil, nil]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 4
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 7
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 7
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, nil)  ;  _jf -> cons(b, nil)  ;  x -> b  ;  ys -> nil
})

-------------------------------------------
Step 9, which took 0.013315 s (model generation: 0.011810,  model checking: 0.001505):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321},
Q_f={q_gen_1316},
Delta=
{
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> butlast([cons(y, nil), nil]) -> 6
() -> butlast([nil, nil]) -> 4
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 7
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.010936 s (model generation: 0.010244,  model checking: 0.000692):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1325, q_gen_1330, q_gen_1333, q_gen_1334, q_gen_1335},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1325
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1330) -> q_gen_1330
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1330
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1330
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1314, q_gen_1315, q_gen_1318},
Q_f={q_gen_1312},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> butlast([cons(y, nil), nil]) -> 7
() -> butlast([nil, nil]) -> 5
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 7
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 7
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.012451 s (model generation: 0.011724,  model checking: 0.000727):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1333, q_gen_1334, q_gen_1335},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> butlast([cons(y, nil), nil]) -> 7
() -> butlast([nil, nil]) -> 6
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 7
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 10
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(a, nil)  ;  y -> b
})

-------------------------------------------
Step 12, which took 0.012119 s (model generation: 0.011516,  model checking: 0.000603):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1333, q_gen_1334, q_gen_1335},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> butlast([cons(y, nil), nil]) -> 7
() -> butlast([nil, nil]) -> 7
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 7
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 10
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 10
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, nil)  ;  _jf -> nil  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.013541 s (model generation: 0.011761,  model checking: 0.001780):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> butlast([cons(y, nil), nil]) -> 7
() -> butlast([nil, nil]) -> 7
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 10
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 10
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.020719 s (model generation: 0.015778,  model checking: 0.004941):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> butlast([cons(y, nil), nil]) -> 8
() -> butlast([nil, nil]) -> 8
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 11
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 11
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.016206 s (model generation: 0.014348,  model checking: 0.001858):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338},
Q_f={q_gen_1316, q_gen_1319},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1319
<a, b, a>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> butlast([cons(y, nil), nil]) -> 9
() -> butlast([nil, nil]) -> 9
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 13
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 14
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 12
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, nil))  ;  _jf -> cons(b, nil)  ;  x -> b  ;  ys -> nil
})

-------------------------------------------
Step 16, which took 0.021955 s (model generation: 0.014578,  model checking: 0.007377):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, b, a>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> butlast([cons(y, nil), nil]) -> 10
() -> butlast([nil, nil]) -> 10
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 16
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 14
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.025312 s (model generation: 0.017650,  model checking: 0.007662):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, b, a>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> butlast([cons(y, nil), nil]) -> 11
() -> butlast([nil, nil]) -> 11
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 19
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 15
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 14
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.027862 s (model generation: 0.019349,  model checking: 0.008513):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> butlast([cons(y, nil), nil]) -> 12
() -> butlast([nil, nil]) -> 12
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 16
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 15
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.029287 s (model generation: 0.024147,  model checking: 0.005140):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> butlast([cons(y, nil), nil]) -> 13
() -> butlast([nil, nil]) -> 13
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 22
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 19
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 16
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, nil))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 0.042631 s (model generation: 0.023852,  model checking: 0.018779):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> butlast([cons(y, nil), nil]) -> 14
() -> butlast([nil, nil]) -> 14
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 20
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 17
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 21, which took 0.032380 s (model generation: 0.029689,  model checking: 0.002691):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1333
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> butlast([cons(y, nil), nil]) -> 15
() -> butlast([nil, nil]) -> 15
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 25
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 23
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 18
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, nil)))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 22, which took 0.043999 s (model generation: 0.033083,  model checking: 0.010916):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> butlast([cons(y, nil), nil]) -> 16
() -> butlast([nil, nil]) -> 16
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 24
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.039656 s (model generation: 0.036471,  model checking: 0.003185):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> butlast([cons(y, nil), nil]) -> 17
() -> butlast([nil, nil]) -> 17
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 27
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 20
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, nil)))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> nil
})

-------------------------------------------
Step 24, which took 0.038546 s (model generation: 0.036974,  model checking: 0.001572):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1333
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1323, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<a>() -> q_gen_1323
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1312
<cons, nil>(q_gen_1323, q_gen_1314) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> butlast([cons(y, nil), nil]) -> 18
() -> butlast([nil, nil]) -> 18
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 27
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 23
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> nil  ;  x2 -> a  ;  x3 -> nil  ;  y -> b
})

-------------------------------------------
Step 25, which took 0.042333 s (model generation: 0.037973,  model checking: 0.004360):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
() -> butlast([cons(y, nil), nil]) -> 19
() -> butlast([nil, nil]) -> 19
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 28
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 30
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 24
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _jf -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 26, which took 0.048849 s (model generation: 0.041642,  model checking: 0.007207):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> butlast([cons(y, nil), nil]) -> 20
() -> butlast([nil, nil]) -> 20
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 30
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 25
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 0.054694 s (model generation: 0.053017,  model checking: 0.001677):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1341
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1317, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313, q_gen_1317},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<cons, cons>(q_gen_1318, q_gen_1317) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1317
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> butlast([cons(y, nil), nil]) -> 21
() -> butlast([nil, nil]) -> 21
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 30
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 28
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> cons(b, cons(a, nil))  ;  x2 -> b  ;  x3 -> cons(a, cons(a, nil))  ;  y -> b
})

-------------------------------------------
Step 28, which took 0.068041 s (model generation: 0.064864,  model checking: 0.003177):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341},
Q_f={q_gen_1316, q_gen_1319},
Delta=
{
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1333
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1319
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1319
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1322, q_gen_1323, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313, q_gen_1322},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<a>() -> q_gen_1323
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1322) -> q_gen_1322
<cons, nil>(q_gen_1323, q_gen_1314) -> q_gen_1322
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
() -> butlast([cons(y, nil), nil]) -> 22
() -> butlast([nil, nil]) -> 22
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 30
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 31
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(b, nil)  ;  y -> b
})

-------------------------------------------
Step 29, which took 0.065196 s (model generation: 0.064155,  model checking: 0.001041):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1325, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1325
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1325
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1325) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> butlast([cons(y, nil), nil]) -> 23
() -> butlast([nil, nil]) -> 23
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 31
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 30
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 31
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 30, which took 0.062378 s (model generation: 0.056488,  model checking: 0.005890):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> butlast([cons(y, nil), nil]) -> 24
() -> butlast([nil, nil]) -> 24
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 34
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 31
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 32
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(a, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 31, which took 0.086653 s (model generation: 0.069834,  model checking: 0.016819):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> butlast([cons(y, nil), nil]) -> 25
() -> butlast([nil, nil]) -> 25
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 32
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 33
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 32, which took 0.087569 s (model generation: 0.085815,  model checking: 0.001754):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<a, b>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> butlast([cons(y, nil), nil]) -> 26
() -> butlast([nil, nil]) -> 26
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 35
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 33
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, nil)))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 33, which took 0.139776 s (model generation: 0.138521,  model checking: 0.001255):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1325, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360},
Q_f={q_gen_1316, q_gen_1319},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1325
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1325
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1325) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1319
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1326, q_gen_1325) -> q_gen_1319
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1319
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1319
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
() -> butlast([cons(y, nil), nil]) -> 27
() -> butlast([nil, nil]) -> 27
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 35
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 33
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 34, which took 0.131224 s (model generation: 0.129008,  model checking: 0.002216):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1319},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1319
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1319
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1319
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> butlast([cons(y, nil), nil]) -> 28
() -> butlast([nil, nil]) -> 28
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 35
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 34
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 35, which took 0.160856 s (model generation: 0.158841,  model checking: 0.002015):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1319},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1319
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1319
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> butlast([cons(y, nil), nil]) -> 29
() -> butlast([nil, nil]) -> 29
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 37
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 38
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 35
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, nil))  ;  _jf -> cons(b, nil)  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 36, which took 0.201015 s (model generation: 0.198838,  model checking: 0.002177):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
() -> butlast([cons(y, nil), nil]) -> 30
() -> butlast([nil, nil]) -> 30
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 40
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 38
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 36
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.174457 s (model generation: 0.172006,  model checking: 0.002451):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1338
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> butlast([cons(y, nil), nil]) -> 31
() -> butlast([nil, nil]) -> 31
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 40
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 41
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 37
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, nil))  ;  _jf -> cons(b, nil)  ;  x -> a  ;  ys -> nil
})

-------------------------------------------
Step 38, which took 0.171777 s (model generation: 0.163510,  model checking: 0.008267):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> butlast([cons(y, nil), nil]) -> 32
() -> butlast([nil, nil]) -> 32
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 43
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 41
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 38
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(a, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 39, which took 0.269500 s (model generation: 0.240538,  model checking: 0.028962):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> butlast([cons(y, nil), nil]) -> 33
() -> butlast([nil, nil]) -> 33
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 46
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 42
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 39
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 40, which took 0.311661 s (model generation: 0.278721,  model checking: 0.032940):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> butlast([cons(y, nil), nil]) -> 34
() -> butlast([nil, nil]) -> 34
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 49
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 43
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 40
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 41, which took 0.422870 s (model generation: 0.363635,  model checking: 0.059235):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
() -> butlast([cons(y, nil), nil]) -> 35
() -> butlast([nil, nil]) -> 35
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 52
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 44
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 41
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, cons(a, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(a, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 42, which took 0.807715 s (model generation: 0.657257,  model checking: 0.150458):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
() -> butlast([cons(y, nil), nil]) -> 36
() -> butlast([nil, nil]) -> 36
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 45
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 42
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(a, cons(a, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(a, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 43, which took 0.753405 s (model generation: 0.750950,  model checking: 0.002455):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1326, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1338, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1338) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1324
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1324
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1338
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1338
<cons, nil, cons>(q_gen_1326, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1338
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1338
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1338
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
() -> butlast([cons(y, nil), nil]) -> 37
() -> butlast([nil, nil]) -> 37
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 48
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 43
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(a, nil))  ;  _jf -> cons(b, nil)  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 44, which took 0.949544 s (model generation: 0.947538,  model checking: 0.002006):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1325, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1325
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1325
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1325) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1325) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 47
() -> butlast([cons(y, nil), nil]) -> 38
() -> butlast([nil, nil]) -> 38
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 48
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 44
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 45, which took 1.097361 s (model generation: 1.095313,  model checking: 0.002048):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1343, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, cons, cons>(q_gen_1343, q_gen_1316) -> q_gen_1316
<cons, cons, cons>(q_gen_1343, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<a, a, a>() -> q_gen_1343
<a, b, a>() -> q_gen_1343
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 48
() -> butlast([cons(y, nil), nil]) -> 39
() -> butlast([nil, nil]) -> 39
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 51
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 45
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(a, nil)  ;  _jf -> nil  ;  x -> b  ;  ys -> cons(a, nil)
})

-------------------------------------------
Step 46, which took 0.873634 s (model generation: 0.872189,  model checking: 0.001445):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1347, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1347
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1347) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 51
() -> butlast([cons(y, nil), nil]) -> 40
() -> butlast([nil, nil]) -> 40
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 51
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 46
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 47, which took 0.733421 s (model generation: 0.731078,  model checking: 0.002343):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1347, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1347
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1347) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 51
() -> butlast([cons(y, nil), nil]) -> 41
() -> butlast([nil, nil]) -> 41
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 55
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 54
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 47
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, nil)))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 48, which took 0.868486 s (model generation: 0.861153,  model checking: 0.007333):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1347, q_gen_1360, q_gen_1364},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<a, a>() -> q_gen_1326
<a, b>() -> q_gen_1326
<b, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1316
<cons, nil, cons>(q_gen_1326, q_gen_1364) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 52
() -> butlast([cons(y, nil), nil]) -> 42
() -> butlast([nil, nil]) -> 42
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 58
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 55
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 48
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 49, which took 1.066754 s (model generation: 1.064477,  model checking: 0.002277):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1359, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, cons, cons>(q_gen_1335, q_gen_1359) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1359
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1359
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1359
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1359
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
() -> butlast([cons(y, nil), nil]) -> 43
() -> butlast([nil, nil]) -> 43
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 58
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 58
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 49
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(a, cons(b, nil)))  ;  _jf -> cons(b, cons(a, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 50, which took 1.374904 s (model generation: 1.360373,  model checking: 0.014531):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1365, q_gen_1386},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, cons, cons>(q_gen_1335, q_gen_1365) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1365
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1365
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 54
() -> butlast([cons(y, nil), nil]) -> 44
() -> butlast([nil, nil]) -> 44
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 61
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 59
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 50
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 51, which took 1.198808 s (model generation: 1.186781,  model checking: 0.012027):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1365, q_gen_1386},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, cons, cons>(q_gen_1335, q_gen_1365) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1365
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 55
() -> butlast([cons(y, nil), nil]) -> 45
() -> butlast([nil, nil]) -> 45
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 64
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 60
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 51
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 52, which took 2.525816 s (model generation: 2.514636,  model checking: 0.011180):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1347, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 56
() -> butlast([cons(y, nil), nil]) -> 46
() -> butlast([nil, nil]) -> 46
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 67
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 61
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 52
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 53, which took 1.402525 s (model generation: 1.400026,  model checking: 0.002499):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1359, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, cons, cons>(q_gen_1335, q_gen_1359) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1359
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1359
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1359
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1359
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 57
() -> butlast([cons(y, nil), nil]) -> 47
() -> butlast([nil, nil]) -> 47
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 67
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 64
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 53
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _jf -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 54, which took 1.439721 s (model generation: 1.414010,  model checking: 0.025711):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 58
() -> butlast([cons(y, nil), nil]) -> 48
() -> butlast([nil, nil]) -> 48
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 70
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 65
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 54
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 55, which took 3.052016 s (model generation: 3.049719,  model checking: 0.002297):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 59
() -> butlast([cons(y, nil), nil]) -> 49
() -> butlast([nil, nil]) -> 49
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 70
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 68
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 55
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(a, nil)))  ;  _jf -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 56, which took 2.902821 s (model generation: 2.861826,  model checking: 0.040995):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 60
() -> butlast([cons(y, nil), nil]) -> 50
() -> butlast([nil, nil]) -> 50
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 73
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 69
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 56
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(b, cons(b, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 57, which took 2.611149 s (model generation: 2.603649,  model checking: 0.007500):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1320
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 61
() -> butlast([cons(y, nil), nil]) -> 51
() -> butlast([nil, nil]) -> 51
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 76
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 70
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 57
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 58, which took 13.368411 s (model generation: 13.365660,  model checking: 0.002751):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1324, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1324},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, cons, cons>(q_gen_1335, q_gen_1324) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1324
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1324
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1324
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 62
() -> butlast([cons(y, nil), nil]) -> 52
() -> butlast([nil, nil]) -> 52
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 76
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 73
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 58
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  _jf -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 59, which took 6.988793 s (model generation: 6.947165,  model checking: 0.041628):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1320
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 63
() -> butlast([cons(y, nil), nil]) -> 53
() -> butlast([nil, nil]) -> 53
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 79
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 74
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 59
}
Sat witness: Found: ((append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]), {
_df -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 60, which took 8.601885 s (model generation: 8.598590,  model checking: 0.003295):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1320, q_gen_1321, q_gen_1331, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1360, q_gen_1364, q_gen_1386},
Q_f={q_gen_1316, q_gen_1331},
Delta=
{
<cons>(q_gen_1334, q_gen_1360) -> q_gen_1333
<nil>() -> q_gen_1333
<a>() -> q_gen_1334
<b>() -> q_gen_1334
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1320
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1320
<nil, nil>() -> q_gen_1320
<a, a>() -> q_gen_1321
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1341
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1386, q_gen_1320) -> q_gen_1364
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1364
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1386
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1320) -> q_gen_1316
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1316
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1331) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1331
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1332
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<a, a, a>() -> q_gen_1335
<a, b, a>() -> q_gen_1335
<b, a, b>() -> q_gen_1335
<b, b, b>() -> q_gen_1335
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1318, q_gen_1327},
Q_f={q_gen_1312, q_gen_1313},
Delta=
{
<nil>() -> q_gen_1314
<a>() -> q_gen_1315
<b>() -> q_gen_1315
<nil, nil>() -> q_gen_1312
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1313
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 64
() -> butlast([cons(y, nil), nil]) -> 54
() -> butlast([nil, nil]) -> 54
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 79
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 77
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 60
}
Sat witness: Found: ((append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]), {
_if -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _jf -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 61, which took 4.029459 s (model generation: 4.025652,  model checking: 0.003807):

Model:
|_
{
append -> 
{{{
Q={q_gen_1316, q_gen_1319, q_gen_1320, q_gen_1321, q_gen_1325, q_gen_1326, q_gen_1332, q_gen_1333, q_gen_1334, q_gen_1335, q_gen_1341, q_gen_1342, q_gen_1343, q_gen_1344, q_gen_1347, q_gen_1351, q_gen_1354, q_gen_1357, q_gen_1358, q_gen_1360, q_gen_1361, q_gen_1364, q_gen_1365, q_gen_1377, q_gen_1379, q_gen_1380, q_gen_1381, q_gen_1384, q_gen_1385, q_gen_1386, q_gen_1387, q_gen_1389, q_gen_1390, q_gen_1392, q_gen_1394, q_gen_1395, q_gen_1396, q_gen_1399, q_gen_1400, q_gen_1401, q_gen_1402, q_gen_1403, q_gen_1405, q_gen_1406, q_gen_1407, q_gen_1408, q_gen_1412, q_gen_1414, q_gen_1415, q_gen_1416, q_gen_1417, q_gen_1418, q_gen_1419, q_gen_1420, q_gen_1422, q_gen_1423, q_gen_1424, q_gen_1427, q_gen_1428, q_gen_1429, q_gen_1432, q_gen_1435, q_gen_1436, q_gen_1437, q_gen_1438, q_gen_1439, q_gen_1440, q_gen_1442, q_gen_1443, q_gen_1444, q_gen_1447, q_gen_1454},
Q_f={q_gen_1316, q_gen_1319, q_gen_1342, q_gen_1380, q_gen_1389, q_gen_1427},
Delta=
{
<cons>(q_gen_1334, q_gen_1360) -> q_gen_1333
<nil>() -> q_gen_1333
<b>() -> q_gen_1334
<a>() -> q_gen_1351
<cons>(q_gen_1334, q_gen_1333) -> q_gen_1360
<nil, nil>() -> q_gen_1320
<b, b>() -> q_gen_1321
<cons, cons>(q_gen_1321, q_gen_1377) -> q_gen_1325
<cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1325
<cons, cons>(q_gen_1400, q_gen_1320) -> q_gen_1325
<a, a>() -> q_gen_1326
<nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1341
<cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1347
<nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1364
<cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1377
<cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1385
<cons, cons>(q_gen_1321, q_gen_1428) -> q_gen_1385
<nil, cons>(q_gen_1351, q_gen_1333) -> q_gen_1385
<a, b>() -> q_gen_1386
<b, a>() -> q_gen_1400
<cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1412
<cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1412
<cons, cons>(q_gen_1326, q_gen_1341) -> q_gen_1412
<cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1428
<cons, cons>(q_gen_1386, q_gen_1385) -> q_gen_1428
<cons, cons>(q_gen_1400, q_gen_1341) -> q_gen_1428
<cons, cons, cons>(q_gen_1335, q_gen_1332) -> q_gen_1316
<cons, cons, cons>(q_gen_1335, q_gen_1384) -> q_gen_1316
<cons, cons, cons>(q_gen_1343, q_gen_1342) -> q_gen_1316
<cons, cons, cons>(q_gen_1354, q_gen_1342) -> q_gen_1316
<cons, cons, cons>(q_gen_1354, q_gen_1399) -> q_gen_1316
<nil, cons, cons>(q_gen_1321, q_gen_1325) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1320) -> q_gen_1316
<nil, cons, cons>(q_gen_1326, q_gen_1377) -> q_gen_1316
<nil, nil, nil>() -> q_gen_1316
<cons, nil, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1321, q_gen_1320) -> q_gen_1319
<nil, cons, cons>(q_gen_1326, q_gen_1325) -> q_gen_1319
<cons, cons, cons>(q_gen_1335, q_gen_1316) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1341) -> q_gen_1332
<cons, nil, cons>(q_gen_1321, q_gen_1347) -> q_gen_1332
<nil, nil, cons>(q_gen_1334, q_gen_1333) -> q_gen_1332
<b, b, b>() -> q_gen_1335
<cons, cons, cons>(q_gen_1343, q_gen_1332) -> q_gen_1342
<nil, nil, cons>(q_gen_1351, q_gen_1333) -> q_gen_1342
<a, b, a>() -> q_gen_1343
<b, a, b>() -> q_gen_1343
<cons, cons, cons>(q_gen_1343, q_gen_1344) -> q_gen_1344
<nil, cons, cons>(q_gen_1321, q_gen_1341) -> q_gen_1344
<a, a, a>() -> q_gen_1354
<cons, cons, cons>(q_gen_1343, q_gen_1358) -> q_gen_1357
<nil, nil, cons>(q_gen_1334, q_gen_1360) -> q_gen_1357
<cons, cons, cons>(q_gen_1343, q_gen_1357) -> q_gen_1358
<cons, cons, cons>(q_gen_1335, q_gen_1357) -> q_gen_1361
<cons, nil, cons>(q_gen_1321, q_gen_1364) -> q_gen_1361
<nil, cons, cons>(q_gen_1321, q_gen_1347) -> q_gen_1361
<cons, cons, cons>(q_gen_1335, q_gen_1361) -> q_gen_1365
<cons, cons, cons>(q_gen_1335, q_gen_1365) -> q_gen_1365
<cons, cons, cons>(q_gen_1343, q_gen_1365) -> q_gen_1365
<cons, cons, cons>(q_gen_1343, q_gen_1379) -> q_gen_1365
<nil, cons, cons>(q_gen_1321, q_gen_1364) -> q_gen_1365
<cons, cons, cons>(q_gen_1343, q_gen_1319) -> q_gen_1379
<cons, cons, cons>(q_gen_1354, q_gen_1381) -> q_gen_1380
<cons, nil, cons>(q_gen_1321, q_gen_1385) -> q_gen_1380
<cons, cons, cons>(q_gen_1335, q_gen_1342) -> q_gen_1381
<nil, cons, cons>(q_gen_1386, q_gen_1385) -> q_gen_1384
<cons, cons, cons>(q_gen_1335, q_gen_1387) -> q_gen_1387
<cons, cons, cons>(q_gen_1335, q_gen_1394) -> q_gen_1387
<cons, nil, cons>(q_gen_1386, q_gen_1341) -> q_gen_1387
<nil, cons, cons>(q_gen_1321, q_gen_1377) -> q_gen_1389
<cons, cons, cons>(q_gen_1335, q_gen_1319) -> q_gen_1390
<nil, cons, cons>(q_gen_1386, q_gen_1341) -> q_gen_1392
<cons, cons, cons>(q_gen_1343, q_gen_1389) -> q_gen_1394
<cons, cons, cons>(q_gen_1335, q_gen_1396) -> q_gen_1395
<cons, cons, cons>(q_gen_1335, q_gen_1344) -> q_gen_1396
<nil, cons, cons>(q_gen_1400, q_gen_1341) -> q_gen_1399
<cons, cons, cons>(q_gen_1354, q_gen_1402) -> q_gen_1401
<cons, cons, cons>(q_gen_1343, q_gen_1316) -> q_gen_1402
<cons, cons, cons>(q_gen_1343, q_gen_1405) -> q_gen_1403
<cons, cons, cons>(q_gen_1354, q_gen_1403) -> q_gen_1403
<cons, nil, cons>(q_gen_1326, q_gen_1320) -> q_gen_1405
<cons, cons, cons>(q_gen_1354, q_gen_1407) -> q_gen_1406
<cons, cons, cons>(q_gen_1343, q_gen_1408) -> q_gen_1407
<cons, nil, cons>(q_gen_1321, q_gen_1412) -> q_gen_1407
<cons, cons, cons>(q_gen_1354, q_gen_1406) -> q_gen_1408
<cons, cons, cons>(q_gen_1354, q_gen_1414) -> q_gen_1408
<cons, nil, cons>(q_gen_1326, q_gen_1341) -> q_gen_1408
<cons, cons, cons>(q_gen_1354, q_gen_1408) -> q_gen_1414
<cons, cons, cons>(q_gen_1354, q_gen_1416) -> q_gen_1415
<cons, cons, cons>(q_gen_1354, q_gen_1417) -> q_gen_1416
<cons, nil, cons>(q_gen_1326, q_gen_1412) -> q_gen_1417
<cons, cons, cons>(q_gen_1335, q_gen_1419) -> q_gen_1418
<cons, nil, cons>(q_gen_1400, q_gen_1320) -> q_gen_1419
<cons, cons, cons>(q_gen_1335, q_gen_1420) -> q_gen_1420
<cons, nil, cons>(q_gen_1321, q_gen_1377) -> q_gen_1420
<cons, cons, cons>(q_gen_1354, q_gen_1332) -> q_gen_1422
<cons, cons, cons>(q_gen_1335, q_gen_1424) -> q_gen_1423
<cons, nil, cons>(q_gen_1400, q_gen_1341) -> q_gen_1424
<cons, cons, cons>(q_gen_1343, q_gen_1361) -> q_gen_1427
<cons, nil, cons>(q_gen_1321, q_gen_1428) -> q_gen_1427
<cons, cons, cons>(q_gen_1343, q_gen_1432) -> q_gen_1429
<nil, cons, cons>(q_gen_1321, q_gen_1412) -> q_gen_1429
<nil, cons, cons>(q_gen_1321, q_gen_1428) -> q_gen_1432
<cons, cons, cons>(q_gen_1335, q_gen_1427) -> q_gen_1435
<cons, cons, cons>(q_gen_1335, q_gen_1437) -> q_gen_1436
<cons, cons, cons>(q_gen_1343, q_gen_1419) -> q_gen_1437
<cons, cons, cons>(q_gen_1343, q_gen_1439) -> q_gen_1438
<cons, cons, cons>(q_gen_1343, q_gen_1440) -> q_gen_1439
<cons, nil, cons>(q_gen_1321, q_gen_1325) -> q_gen_1440
<cons, cons, cons>(q_gen_1335, q_gen_1440) -> q_gen_1442
<cons, cons, cons>(q_gen_1343, q_gen_1444) -> q_gen_1443
<cons, cons, cons>(q_gen_1343, q_gen_1427) -> q_gen_1444
<cons, cons, cons>(q_gen_1335, q_gen_1447) -> q_gen_1447
<cons, cons, cons>(q_gen_1343, q_gen_1380) -> q_gen_1447
<cons, cons, cons>(q_gen_1354, q_gen_1447) -> q_gen_1447
<nil, cons, cons>(q_gen_1321, q_gen_1385) -> q_gen_1447
<cons, cons, cons>(q_gen_1335, q_gen_1407) -> q_gen_1454
<cons, cons, cons>(q_gen_1335, q_gen_1429) -> q_gen_1454
<cons, cons, cons>(q_gen_1335, q_gen_1454) -> q_gen_1454
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  butlast -> 
{{{
Q={q_gen_1312, q_gen_1313, q_gen_1314, q_gen_1315, q_gen_1317, q_gen_1318, q_gen_1322, q_gen_1323, q_gen_1327, q_gen_1336},
Q_f={q_gen_1312, q_gen_1313, q_gen_1317, q_gen_1322, q_gen_1336},
Delta=
{
<nil>() -> q_gen_1314
<b>() -> q_gen_1315
<a>() -> q_gen_1323
<cons, cons>(q_gen_1318, q_gen_1317) -> q_gen_1312
<nil, nil>() -> q_gen_1312
<cons, nil>(q_gen_1315, q_gen_1314) -> q_gen_1313
<cons, cons>(q_gen_1318, q_gen_1313) -> q_gen_1317
<a, a>() -> q_gen_1318
<b, b>() -> q_gen_1318
<cons, nil>(q_gen_1323, q_gen_1314) -> q_gen_1322
<cons, cons>(q_gen_1318, q_gen_1312) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1327) -> q_gen_1327
<cons, cons>(q_gen_1318, q_gen_1322) -> q_gen_1336
<cons, cons>(q_gen_1318, q_gen_1336) -> q_gen_1336
}

Datatype: <eltlist, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 64
() -> butlast([cons(y, nil), nil]) -> 55
() -> butlast([nil, nil]) -> 55
(append([t1, l2, _df])) -> append([cons(h1, t1), l2, cons(h1, _df)]) -> 79
(append([ys, cons(x, nil), _if]) /\ butlast([_if, _jf])) -> eq_eltlist([_jf, ys]) -> 77
(butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]) -> 63
}
Sat witness: Found: ((butlast([cons(x2, x3), _ze])) -> butlast([cons(y, cons(x2, x3)), cons(y, _ze)]), {
_ze -> cons(b, cons(a, nil))  ;  x2 -> b  ;  x3 -> cons(a, cons(b, nil))  ;  y -> b
})

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