Solving ../../benchmarks/true/isaplanner_prop13.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(drop, F:
{() -> drop([s(u), nil, nil])
() -> drop([z, l, l])
(drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um])}
(drop([_vm, _wm, _xm]) /\ drop([_vm, _wm, _ym])) -> eq_eltlist([_xm, _ym])
)
}

properties:
{(drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an])}


over-approximation: {drop}
under-approximation: {}

Clause system for inference is:

{
() -> drop([s(u), nil, nil]) -> 0  ;  () -> drop([z, l, l]) -> 0  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 0  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 0
}


Solving took 42.154259 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1132, q_gen_1133, q_gen_1134, q_gen_1135, q_gen_1136, q_gen_1137, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1142, q_gen_1143, q_gen_1144, q_gen_1145, q_gen_1146, q_gen_1147, q_gen_1148, q_gen_1149, q_gen_1150, q_gen_1151, q_gen_1152, q_gen_1153, q_gen_1154, q_gen_1155, q_gen_1156, q_gen_1157, q_gen_1158, q_gen_1159, q_gen_1160, q_gen_1161, q_gen_1162, q_gen_1163, q_gen_1164, q_gen_1165, q_gen_1166, q_gen_1167, q_gen_1168, q_gen_1169, q_gen_1170, q_gen_1171, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1176, q_gen_1177, q_gen_1178, q_gen_1179, q_gen_1180, q_gen_1181, q_gen_1182, q_gen_1183, q_gen_1184, q_gen_1185, q_gen_1186, q_gen_1187, q_gen_1188, q_gen_1189, q_gen_1190, q_gen_1191, q_gen_1192, q_gen_1193, q_gen_1194, q_gen_1195, q_gen_1196, q_gen_1197, q_gen_1198, q_gen_1199, q_gen_1200, q_gen_1201, q_gen_1202, q_gen_1203, q_gen_1204, q_gen_1205, q_gen_1206, q_gen_1207, q_gen_1208, q_gen_1209, q_gen_1210, q_gen_1211, q_gen_1212, q_gen_1213, q_gen_1214, q_gen_1215, q_gen_1216, q_gen_1217, q_gen_1218, q_gen_1219, q_gen_1220, q_gen_1221, q_gen_1222, q_gen_1223, q_gen_1224, q_gen_1225, q_gen_1226, q_gen_1227, q_gen_1228, q_gen_1229, q_gen_1230, q_gen_1231, q_gen_1232, q_gen_1233, q_gen_1234, q_gen_1235, q_gen_1236, q_gen_1237, q_gen_1238, q_gen_1239, q_gen_1240, q_gen_1241, q_gen_1242, q_gen_1243, q_gen_1244, q_gen_1245, q_gen_1246, q_gen_1247, q_gen_1248, q_gen_1249, q_gen_1250, q_gen_1251, q_gen_1252, q_gen_1253, q_gen_1254, q_gen_1255, q_gen_1256, q_gen_1257, q_gen_1258, q_gen_1259, q_gen_1260, q_gen_1261, q_gen_1262, q_gen_1263, q_gen_1264, q_gen_1265, q_gen_1266, q_gen_1267, q_gen_1268, q_gen_1269, q_gen_1270, q_gen_1271, q_gen_1272, q_gen_1273, q_gen_1274, q_gen_1275, q_gen_1276, q_gen_1277, q_gen_1278, q_gen_1279, q_gen_1280, q_gen_1281, q_gen_1282, q_gen_1283, q_gen_1284, q_gen_1285, q_gen_1286, q_gen_1287, q_gen_1288, q_gen_1289, q_gen_1290, q_gen_1291, q_gen_1292, q_gen_1293, q_gen_1294, q_gen_1295, q_gen_1296, q_gen_1297, q_gen_1298, q_gen_1299, q_gen_1300, q_gen_1301, q_gen_1302, q_gen_1303, q_gen_1304, q_gen_1305, q_gen_1306},
Q_f={},
Delta=
{
<z>() -> q_gen_1133
<s>(q_gen_1133) -> q_gen_1143
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1199
<cons>(q_gen_1164, q_gen_1199) -> q_gen_1202
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1221
<cons>(q_gen_1164, q_gen_1221) -> q_gen_1224
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1243
<cons>(q_gen_1164, q_gen_1243) -> q_gen_1246
<cons>(q_gen_1157, q_gen_1199) -> q_gen_1251
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, b>() -> q_gen_1139
<b, nil>() -> q_gen_1140
<b, b>() -> q_gen_1141
<z, a>() -> q_gen_1145
<nil, a>() -> q_gen_1147
<a, nil>() -> q_gen_1148
<a, a>() -> q_gen_1149
<s, nil>(q_gen_1133) -> q_gen_1151
<s, b>(q_gen_1133) -> q_gen_1152
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1154
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1155
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1158
<s, a>(q_gen_1133) -> q_gen_1160
<cons, cons>(q_gen_1149, q_gen_1148, q_gen_1147, q_gen_1138) -> q_gen_1162
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1163
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1165
<s, cons>(q_gen_1145, q_gen_1135) -> q_gen_1167
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1169
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1170
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1180
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1181
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<cons, cons>(q_gen_1141, q_gen_1158, q_gen_1155, q_gen_1154) -> q_gen_1185
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1186
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1188
<cons, cons>(q_gen_1141, q_gen_1200, q_gen_1198, q_gen_1197) -> q_gen_1196
<cons, cons>(q_gen_1149, q_gen_1181, q_gen_1180, q_gen_1162) -> q_gen_1197
<cons, b>(q_gen_1164, q_gen_1199) -> q_gen_1198
<b, cons>(q_gen_1164, q_gen_1199) -> q_gen_1200
<cons, b>(q_gen_1157, q_gen_1202) -> q_gen_1201
<b, cons>(q_gen_1157, q_gen_1202) -> q_gen_1203
<z, cons>(q_gen_1164, q_gen_1199) -> q_gen_1206
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1208
<cons, cons>(q_gen_1149, q_gen_1170, q_gen_1169, q_gen_1154) -> q_gen_1210
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1211
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1212
<cons, cons>(q_gen_1149, q_gen_1222, q_gen_1220, q_gen_1217) -> q_gen_1216
<cons, cons>(q_gen_1149, q_gen_1219, q_gen_1218, q_gen_1210) -> q_gen_1217
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1218
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1219
<cons, a>(q_gen_1164, q_gen_1221) -> q_gen_1220
<a, cons>(q_gen_1164, q_gen_1221) -> q_gen_1222
<cons, b>(q_gen_1164, q_gen_1224) -> q_gen_1223
<b, cons>(q_gen_1164, q_gen_1224) -> q_gen_1225
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1234
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1235
<cons, cons>(q_gen_1149, q_gen_1235, q_gen_1234, q_gen_1185) -> q_gen_1241
<cons, b>(q_gen_1164, q_gen_1243) -> q_gen_1242
<b, cons>(q_gen_1164, q_gen_1243) -> q_gen_1244
<z, cons>(q_gen_1157, q_gen_1246) -> q_gen_1248
<cons, cons>(q_gen_1141, q_gen_1165, q_gen_1163, q_gen_1162) -> q_gen_1254
<cons, a>(q_gen_1157, q_gen_1199) -> q_gen_1255
<a, cons>(q_gen_1157, q_gen_1199) -> q_gen_1256
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1259
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1267
<s, cons>(q_gen_1136, q_gen_1259) -> q_gen_1273
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1281
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1301
<z, nil, nil>() -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1132
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1134
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1137
<s, nil, nil>(q_gen_1143) -> q_gen_1142
<s, cons, nil>(q_gen_1145, q_gen_1135) -> q_gen_1144
<z, cons, cons>(q_gen_1149, q_gen_1148, q_gen_1147, q_gen_1138) -> q_gen_1146
<s, cons, nil>(q_gen_1152, q_gen_1151) -> q_gen_1150
<z, cons, cons>(q_gen_1141, q_gen_1158, q_gen_1155, q_gen_1154) -> q_gen_1153
<s, cons, nil>(q_gen_1160, q_gen_1151) -> q_gen_1159
<z, cons, cons>(q_gen_1141, q_gen_1165, q_gen_1163, q_gen_1162) -> q_gen_1161
<s, cons, nil>(q_gen_1152, q_gen_1167) -> q_gen_1166
<z, cons, cons>(q_gen_1149, q_gen_1170, q_gen_1169, q_gen_1154) -> q_gen_1168
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1171
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1177) -> q_gen_1176
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1177
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
<z, cons, cons>(q_gen_1149, q_gen_1181, q_gen_1180, q_gen_1162) -> q_gen_1179
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1182
<z, cons, cons>(q_gen_1141, q_gen_1188, q_gen_1186, q_gen_1185) -> q_gen_1184
<s, cons, cons>(q_gen_1191, q_gen_1174, q_gen_1190, q_gen_1177) -> q_gen_1189
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1190
<z, b, a>() -> q_gen_1191
<s, cons, cons>(q_gen_1191, q_gen_1174, q_gen_1194, q_gen_1193) -> q_gen_1192
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1193
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1194
<z, cons, cons>(q_gen_1141, q_gen_1203, q_gen_1201, q_gen_1196) -> q_gen_1195
<z, cons, nil>(q_gen_1164, q_gen_1199) -> q_gen_1204
<s, cons, nil>(q_gen_1136, q_gen_1206) -> q_gen_1205
<s, cons, nil>(q_gen_1136, q_gen_1208) -> q_gen_1207
<z, cons, cons>(q_gen_1141, q_gen_1212, q_gen_1211, q_gen_1210) -> q_gen_1209
<s, cons, cons>(q_gen_1191, q_gen_1174, q_gen_1214, q_gen_1204) -> q_gen_1213
<z, cons, a>(q_gen_1164, q_gen_1199) -> q_gen_1214
<z, cons, cons>(q_gen_1141, q_gen_1225, q_gen_1223, q_gen_1216) -> q_gen_1215
<s, cons, cons>(q_gen_1228, q_gen_1227, q_gen_1173, q_gen_1172) -> q_gen_1226
<z, a, nil>() -> q_gen_1227
<z, a, b>() -> q_gen_1228
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1231, q_gen_1230) -> q_gen_1229
<z, cons, nil>(q_gen_1157, q_gen_1202) -> q_gen_1230
<z, cons, b>(q_gen_1157, q_gen_1202) -> q_gen_1231
<z, cons, cons>(q_gen_1141, q_gen_1200, q_gen_1198, q_gen_1197) -> q_gen_1232
<z, cons, cons>(q_gen_1149, q_gen_1235, q_gen_1234, q_gen_1185) -> q_gen_1233
<s, cons, cons>(q_gen_1239, q_gen_1238, q_gen_1237, q_gen_1182) -> q_gen_1236
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1237
<s, b, nil>(q_gen_1133) -> q_gen_1238
<s, b, a>(q_gen_1133) -> q_gen_1239
<z, cons, cons>(q_gen_1141, q_gen_1244, q_gen_1242, q_gen_1241) -> q_gen_1240
<z, cons, nil>(q_gen_1157, q_gen_1246) -> q_gen_1245
<s, cons, nil>(q_gen_1136, q_gen_1248) -> q_gen_1247
<s, cons, cons>(q_gen_1191, q_gen_1174, q_gen_1252, q_gen_1250) -> q_gen_1249
<z, cons, nil>(q_gen_1164, q_gen_1251) -> q_gen_1250
<z, cons, a>(q_gen_1164, q_gen_1251) -> q_gen_1252
<z, cons, cons>(q_gen_1149, q_gen_1256, q_gen_1255, q_gen_1254) -> q_gen_1253
<s, cons, cons>(q_gen_1261, q_gen_1238, q_gen_1260, q_gen_1258) -> q_gen_1257
<s, cons, nil>(q_gen_1136, q_gen_1259) -> q_gen_1258
<s, cons, b>(q_gen_1136, q_gen_1259) -> q_gen_1260
<s, b, b>(q_gen_1133) -> q_gen_1261
<s, cons, cons>(q_gen_1239, q_gen_1238, q_gen_1264, q_gen_1263) -> q_gen_1262
<s, cons, nil>(q_gen_1145, q_gen_1259) -> q_gen_1263
<s, cons, a>(q_gen_1145, q_gen_1259) -> q_gen_1264
<s, cons, cons>(q_gen_1270, q_gen_1269, q_gen_1268, q_gen_1266) -> q_gen_1265
<s, cons, nil>(q_gen_1152, q_gen_1267) -> q_gen_1266
<s, cons, a>(q_gen_1152, q_gen_1267) -> q_gen_1268
<s, b, nil>(q_gen_1143) -> q_gen_1269
<s, b, a>(q_gen_1143) -> q_gen_1270
<s, cons, cons>(q_gen_1276, q_gen_1275, q_gen_1274, q_gen_1272) -> q_gen_1271
<s, cons, nil>(q_gen_1152, q_gen_1273) -> q_gen_1272
<s, cons, b>(q_gen_1152, q_gen_1273) -> q_gen_1274
<s, a, nil>(q_gen_1143) -> q_gen_1275
<s, a, b>(q_gen_1143) -> q_gen_1276
<s, cons, cons>(q_gen_1239, q_gen_1238, q_gen_1278, q_gen_1134) -> q_gen_1277
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1278
<s, cons, cons>(q_gen_1283, q_gen_1275, q_gen_1282, q_gen_1280) -> q_gen_1279
<s, cons, nil>(q_gen_1152, q_gen_1281) -> q_gen_1280
<s, cons, a>(q_gen_1152, q_gen_1281) -> q_gen_1282
<s, a, a>(q_gen_1143) -> q_gen_1283
<s, cons, cons>(q_gen_1261, q_gen_1238, q_gen_1285, q_gen_1144) -> q_gen_1284
<s, cons, b>(q_gen_1145, q_gen_1135) -> q_gen_1285
<s, cons, cons>(q_gen_1289, q_gen_1288, q_gen_1287, q_gen_1134) -> q_gen_1286
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1287
<s, a, nil>(q_gen_1133) -> q_gen_1288
<s, a, b>(q_gen_1133) -> q_gen_1289
<s, cons, cons>(q_gen_1293, q_gen_1269, q_gen_1292, q_gen_1291) -> q_gen_1290
<s, cons, nil>(q_gen_1160, q_gen_1281) -> q_gen_1291
<s, cons, b>(q_gen_1160, q_gen_1281) -> q_gen_1292
<s, b, b>(q_gen_1143) -> q_gen_1293
<s, cons, cons>(q_gen_1239, q_gen_1238, q_gen_1295, q_gen_1258) -> q_gen_1294
<s, cons, a>(q_gen_1136, q_gen_1259) -> q_gen_1295
<s, cons, cons>(q_gen_1261, q_gen_1238, q_gen_1297, q_gen_1182) -> q_gen_1296
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1297
<s, cons, cons>(q_gen_1293, q_gen_1269, q_gen_1299, q_gen_1266) -> q_gen_1298
<s, cons, b>(q_gen_1152, q_gen_1267) -> q_gen_1299
<s, cons, nil>(q_gen_1136, q_gen_1301) -> q_gen_1300
<s, cons, cons>(q_gen_1303, q_gen_1227, q_gen_1190, q_gen_1177) -> q_gen_1302
<z, a, a>() -> q_gen_1303
<s, cons, cons>(q_gen_1261, q_gen_1238, q_gen_1306, q_gen_1305) -> q_gen_1304
<s, cons, nil>(q_gen_1145, q_gen_1183) -> q_gen_1305
<s, cons, b>(q_gen_1145, q_gen_1183) -> q_gen_1306
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.003727 s (model generation: 0.003287,  model checking: 0.000440):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 0  ;  () -> drop([z, l, l]) -> 3  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 1
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> nil
})

-------------------------------------------
Step 1, which took 0.003514 s (model generation: 0.003301,  model checking: 0.000213):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131},
Q_f={q_gen_1131},
Delta=
{
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 3  ;  () -> drop([z, l, l]) -> 3  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 1
}
Sat witness: Yes: (() -> drop([s(u), nil, nil]), {
u -> z
})

-------------------------------------------
Step 2, which took 0.003663 s (model generation: 0.003301,  model checking: 0.000362):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133},
Q_f={q_gen_1131},
Delta=
{
<z>() -> q_gen_1133
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 3  ;  () -> drop([z, l, l]) -> 3  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 1  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 3, which took 0.005944 s (model generation: 0.005229,  model checking: 0.000715):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136},
Q_f={q_gen_1131},
Delta=
{
<z>() -> q_gen_1133
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 3  ;  () -> drop([z, l, l]) -> 6  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 2  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, nil)
})

-------------------------------------------
Step 4, which took 0.009200 s (model generation: 0.007950,  model checking: 0.001250):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141},
Q_f={q_gen_1131},
Delta=
{
<z>() -> q_gen_1133
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, b>() -> q_gen_1139
<b, nil>() -> q_gen_1140
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 6  ;  () -> drop([z, l, l]) -> 6  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 3  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 4
}
Sat witness: Yes: (() -> drop([s(u), nil, nil]), {
u -> s(z)
})

-------------------------------------------
Step 5, which took 0.013038 s (model generation: 0.011514,  model checking: 0.001524):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, b>() -> q_gen_1139
<b, nil>() -> q_gen_1140
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 6  ;  () -> drop([z, l, l]) -> 6  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 4  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 7
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 6, which took 0.014830 s (model generation: 0.012275,  model checking: 0.002555):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<z, nil>() -> q_gen_1135
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, b>() -> q_gen_1139
<b, nil>() -> q_gen_1140
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 6  ;  () -> drop([z, l, l]) -> 9  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 5  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 7
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.016821 s (model generation: 0.013741,  model checking: 0.003080):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<z, nil>() -> q_gen_1135
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 7  ;  () -> drop([z, l, l]) -> 9  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 6  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 10
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> nil
})

-------------------------------------------
Step 8, which took 0.019191 s (model generation: 0.013814,  model checking: 0.005377):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<nil, nil>() -> q_gen_1138
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 8  ;  () -> drop([z, l, l]) -> 12  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 7  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 10
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.019043 s (model generation: 0.015497,  model checking: 0.003546):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 9  ;  () -> drop([z, l, l]) -> 12  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 8  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 13
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> s(z)  ;  x2 -> a  ;  x3 -> nil
})

-------------------------------------------
Step 10, which took 0.036609 s (model generation: 0.015954,  model checking: 0.020655):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 10  ;  () -> drop([z, l, l]) -> 15  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 9  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 13
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 11, which took 0.007522 s (model generation: 0.005850,  model checking: 0.001672):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<a>() -> q_gen_1157
<b>() -> q_gen_1157
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 11  ;  () -> drop([z, l, l]) -> 15  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 10  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 12, which took 0.018408 s (model generation: 0.010906,  model checking: 0.007502):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<a>() -> q_gen_1157
<b>() -> q_gen_1157
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 12  ;  () -> drop([z, l, l]) -> 18  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 11  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 16
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 13, which took 0.036788 s (model generation: 0.016472,  model checking: 0.020316):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<a>() -> q_gen_1157
<b>() -> q_gen_1157
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 13  ;  () -> drop([z, l, l]) -> 18  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 12  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.008357 s (model generation: 0.007672,  model checking: 0.000685):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1173, q_gen_1174, q_gen_1175},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<a>() -> q_gen_1157
<b>() -> q_gen_1157
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 13  ;  () -> drop([z, l, l]) -> 18  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 15  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> nil  ;  _zm -> cons(b, nil)  ;  l1 -> cons(a, nil)  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 15, which took 0.018587 s (model generation: 0.015147,  model checking: 0.003440):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<a>() -> q_gen_1157
<b>() -> q_gen_1157
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 14  ;  () -> drop([z, l, l]) -> 18  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 18  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, nil)  ;  _zm -> cons(b, nil)  ;  l1 -> cons(a, nil)  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 16, which took 0.025747 s (model generation: 0.023826,  model checking: 0.001921):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1176},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1176) -> q_gen_1176
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1176
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 15  ;  () -> drop([z, l, l]) -> 18  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 21  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> nil  ;  _zm -> cons(b, nil)  ;  l1 -> cons(b, nil)  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 17, which took 0.039018 s (model generation: 0.021617,  model checking: 0.017401):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 16  ;  () -> drop([z, l, l]) -> 21  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 21  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 19
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 18, which took 0.016868 s (model generation: 0.013159,  model checking: 0.003709):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 17  ;  () -> drop([z, l, l]) -> 21  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 21  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 22
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 19, which took 0.025307 s (model generation: 0.023489,  model checking: 0.001818):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 18  ;  () -> drop([z, l, l]) -> 21  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 24  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 22
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, nil)  ;  _zm -> nil  ;  l1 -> cons(a, nil)  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 20, which took 0.083312 s (model generation: 0.013897,  model checking: 0.069415):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 19  ;  () -> drop([z, l, l]) -> 24  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 24  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 22
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 21, which took 0.079403 s (model generation: 0.011581,  model checking: 0.067822):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1176, q_gen_1183},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, b>() -> q_gen_1175
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1176) -> q_gen_1176
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1176
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 20  ;  () -> drop([z, l, l]) -> 24  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 24  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 25
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(a, nil)  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 22, which took 0.015106 s (model generation: 0.012022,  model checking: 0.003084):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 21  ;  () -> drop([z, l, l]) -> 24  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 27  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 25
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, cons(b, nil))  ;  _zm -> cons(a, nil)  ;  l1 -> cons(a, cons(b, nil))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 23, which took 0.605179 s (model generation: 0.013256,  model checking: 0.591923):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 22  ;  () -> drop([z, l, l]) -> 27  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 27  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 25
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(b, cons(a, cons(a, nil))))
})

-------------------------------------------
Step 24, which took 0.020437 s (model generation: 0.016057,  model checking: 0.004380):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 23  ;  () -> drop([z, l, l]) -> 27  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 27  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 28
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 25, which took 0.027029 s (model generation: 0.017167,  model checking: 0.009862):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 24  ;  () -> drop([z, l, l]) -> 27  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 30  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 28
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, cons(b, nil))  ;  _zm -> nil  ;  l1 -> cons(a, cons(b, nil))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 26, which took 0.521395 s (model generation: 0.018634,  model checking: 0.502761):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 25  ;  () -> drop([z, l, l]) -> 30  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 30  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 28
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 27, which took 0.023353 s (model generation: 0.021443,  model checking: 0.001910):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 26  ;  () -> drop([z, l, l]) -> 30  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 30  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.027472 s (model generation: 0.020512,  model checking: 0.006960):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 27  ;  () -> drop([z, l, l]) -> 30  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 33  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, cons(a, nil))  ;  _zm -> cons(a, nil)  ;  l1 -> cons(a, cons(a, nil))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 29, which took 0.771673 s (model generation: 0.022300,  model checking: 0.749373):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 28  ;  () -> drop([z, l, l]) -> 33  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 33  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 31
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(a, cons(a, cons(a, cons(b, nil)))))
})

-------------------------------------------
Step 30, which took 0.940912 s (model generation: 0.026023,  model checking: 0.914889):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, b, nil>() -> q_gen_1174
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 29  ;  () -> drop([z, l, l]) -> 33  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 33  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 34
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(b, nil)
})

-------------------------------------------
Step 31, which took 0.068955 s (model generation: 0.028392,  model checking: 0.040563):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 30  ;  () -> drop([z, l, l]) -> 33  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 36  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 34
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, cons(a, cons(a, nil)))  ;  _zm -> cons(b, nil)  ;  l1 -> cons(b, cons(a, cons(a, nil)))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 32, which took 0.703381 s (model generation: 0.037102,  model checking: 0.666279):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 31  ;  () -> drop([z, l, l]) -> 36  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 36  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 34
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 33, which took 1.591368 s (model generation: 0.035762,  model checking: 1.555606):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 32  ;  () -> drop([z, l, l]) -> 36  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 36  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 37
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(a, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 34, which took 2.381836 s (model generation: 0.040816,  model checking: 2.341020):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 33  ;  () -> drop([z, l, l]) -> 39  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 37  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 37
}
Sat witness: Yes: (() -> drop([z, l, l]), {
l -> cons(b, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 35, which took 0.049303 s (model generation: 0.044601,  model checking: 0.004702):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 34  ;  () -> drop([z, l, l]) -> 39  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 37  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 40
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> nil  ;  u -> z  ;  x2 -> b  ;  x3 -> cons(b, cons(a, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 36, which took 0.212926 s (model generation: 0.050891,  model checking: 0.162035):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1156
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 35  ;  () -> drop([z, l, l]) -> 39  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 40  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 40
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, cons(b, cons(a, nil)))  ;  _zm -> cons(a, nil)  ;  l1 -> cons(a, cons(b, cons(a, nil)))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 37, which took 0.194548 s (model generation: 0.083346,  model checking: 0.111202):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 36  ;  () -> drop([z, l, l]) -> 40  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 40  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 43
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> s(z)  ;  x2 -> b  ;  x3 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.125778 s (model generation: 0.088500,  model checking: 0.037278):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 37  ;  () -> drop([z, l, l]) -> 40  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 43  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 43
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, nil)  ;  _zm -> cons(a, nil)  ;  l1 -> cons(a, cons(b, nil))  ;  n -> s(z)  ;  x -> b
})

-------------------------------------------
Step 39, which took 0.251102 s (model generation: 0.107398,  model checking: 0.143704):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 38  ;  () -> drop([z, l, l]) -> 41  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 43  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 46
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 40, which took 0.113855 s (model generation: 0.107840,  model checking: 0.006015):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 39  ;  () -> drop([z, l, l]) -> 42  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 46  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 46
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, nil)  ;  _zm -> nil  ;  l1 -> cons(b, nil)  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 41, which took 0.258657 s (model generation: 0.150302,  model checking: 0.108355):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1248},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1248
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1248
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1248) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1248) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1248) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 40  ;  () -> drop([z, l, l]) -> 43  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 46  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 49
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 42, which took 0.168923 s (model generation: 0.161220,  model checking: 0.007703):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1145, q_gen_1151, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1151) -> q_gen_1135
<s, cons>(q_gen_1145, q_gen_1135) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, a>(q_gen_1133) -> q_gen_1145
<s, b>(q_gen_1133) -> q_gen_1145
<z, a>() -> q_gen_1145
<s, nil>(q_gen_1133) -> q_gen_1151
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1151
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1151
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1151
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, cons, nil>(q_gen_1145, q_gen_1135) -> q_gen_1131
<s, cons, nil>(q_gen_1145, q_gen_1151) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1151) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1151) -> q_gen_1173
<s, cons, a>(q_gen_1145, q_gen_1135) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1151) -> q_gen_1173
<s, cons, b>(q_gen_1145, q_gen_1135) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1145, q_gen_1151) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 41  ;  () -> drop([z, l, l]) -> 44  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 49  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 49
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, nil)  ;  _zm -> nil  ;  l1 -> cons(b, nil)  ;  n -> z  ;  x -> a
})

-------------------------------------------
Step 43, which took 0.154411 s (model generation: 0.139705,  model checking: 0.014706):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1248},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons>(q_gen_1136, q_gen_1248) -> q_gen_1248
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1248
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1248
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1248) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1248) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1248) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 42  ;  () -> drop([z, l, l]) -> 45  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 49  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 52
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(a, nil)  ;  u -> s(s(z))  ;  x2 -> a  ;  x3 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 44, which took 0.449896 s (model generation: 0.443026,  model checking: 0.006870):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1145, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1135
<s, cons>(q_gen_1145, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, a>(q_gen_1133) -> q_gen_1145
<s, b>(q_gen_1133) -> q_gen_1145
<z, a>() -> q_gen_1145
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, cons, nil>(q_gen_1145, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1145, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1145, q_gen_1135) -> q_gen_1178
<s, cons, a>(q_gen_1145, q_gen_1183) -> q_gen_1178
<s, cons, b>(q_gen_1145, q_gen_1135) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 43  ;  () -> drop([z, l, l]) -> 46  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 52  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 52
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> nil  ;  _zm -> cons(b, nil)  ;  l1 -> cons(a, nil)  ;  n -> s(z)  ;  x -> b
})

-------------------------------------------
Step 45, which took 0.347839 s (model generation: 0.335276,  model checking: 0.012563):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1145, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1135
<s, cons>(q_gen_1145, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, b>(q_gen_1133) -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, a>(q_gen_1133) -> q_gen_1145
<z, a>() -> q_gen_1145
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, cons, nil>(q_gen_1145, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1145, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1145, q_gen_1183) -> q_gen_1178
<s, cons, b>(q_gen_1145, q_gen_1135) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 44  ;  () -> drop([z, l, l]) -> 47  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 52  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 55
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 46, which took 0.454902 s (model generation: 0.419575,  model checking: 0.035327):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1145, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, cons>(q_gen_1145, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, b>(q_gen_1133) -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, a>(q_gen_1133) -> q_gen_1145
<z, a>() -> q_gen_1145
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, cons, nil>(q_gen_1145, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1145, q_gen_1183) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1145, q_gen_1135) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1178
<s, cons, a>(q_gen_1145, q_gen_1183) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 45  ;  () -> drop([z, l, l]) -> 48  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 55  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 55
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, nil)  ;  _zm -> cons(a, nil)  ;  l1 -> cons(b, cons(b, nil))  ;  n -> s(z)  ;  x -> b
})

-------------------------------------------
Step 47, which took 0.420458 s (model generation: 0.408628,  model checking: 0.011830):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1259},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons>(q_gen_1136, q_gen_1259) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1259
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1259) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1259) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1178
<s, cons, a>(q_gen_1136, q_gen_1259) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 46  ;  () -> drop([z, l, l]) -> 49  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 55  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 58
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(b, nil)  ;  u -> s(s(z))  ;  x2 -> b  ;  x3 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 48, which took 0.594018 s (model generation: 0.514008,  model checking: 0.080010):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1259},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<s, cons>(q_gen_1136, q_gen_1259) -> q_gen_1259
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1259
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1259) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1259) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1178
<s, cons, a>(q_gen_1136, q_gen_1259) -> q_gen_1178
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1178
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 47  ;  () -> drop([z, l, l]) -> 50  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 58  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 58
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(b, cons(b, nil))  ;  _zm -> nil  ;  l1 -> cons(b, cons(b, nil))  ;  n -> z  ;  x -> b
})

-------------------------------------------
Step 49, which took 0.502239 s (model generation: 0.419338,  model checking: 0.082901):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1248},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1183
<s, cons>(q_gen_1136, q_gen_1248) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1248
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1248
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1248) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1248) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1248) -> q_gen_1178
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 48  ;  () -> drop([z, l, l]) -> 51  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 58  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 61
}
Sat witness: Yes: ((drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]), {
_um -> cons(a, nil)  ;  u -> z  ;  x2 -> a  ;  x3 -> cons(a, nil)
})

-------------------------------------------
Step 50, which took 0.296730 s (model generation: 0.263065,  model checking: 0.033665):

Model:
|_
{
drop -> 
{{{
Q={q_gen_1131, q_gen_1133, q_gen_1135, q_gen_1136, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1156, q_gen_1157, q_gen_1164, q_gen_1172, q_gen_1173, q_gen_1174, q_gen_1175, q_gen_1178, q_gen_1183, q_gen_1187, q_gen_1248},
Q_f={q_gen_1131},
Delta=
{
<s>(q_gen_1133) -> q_gen_1133
<z>() -> q_gen_1133
<nil>() -> q_gen_1156
<b>() -> q_gen_1157
<a>() -> q_gen_1164
<cons>(q_gen_1157, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1157, q_gen_1187) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1156) -> q_gen_1187
<cons>(q_gen_1164, q_gen_1187) -> q_gen_1187
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1135
<s, nil>(q_gen_1133) -> q_gen_1135
<z, nil>() -> q_gen_1135
<s, a>(q_gen_1133) -> q_gen_1136
<s, b>(q_gen_1133) -> q_gen_1136
<z, a>() -> q_gen_1136
<z, b>() -> q_gen_1136
<cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1138
<nil, nil>() -> q_gen_1138
<cons, a>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1139
<cons, b>(q_gen_1164, q_gen_1187) -> q_gen_1139
<nil, a>() -> q_gen_1139
<nil, b>() -> q_gen_1139
<a, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<a, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<a, nil>() -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1157, q_gen_1187) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1156) -> q_gen_1140
<b, cons>(q_gen_1164, q_gen_1187) -> q_gen_1140
<b, nil>() -> q_gen_1140
<a, a>() -> q_gen_1141
<b, b>() -> q_gen_1141
<s, cons>(q_gen_1136, q_gen_1183) -> q_gen_1183
<s, cons>(q_gen_1136, q_gen_1248) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1156) -> q_gen_1183
<z, cons>(q_gen_1164, q_gen_1187) -> q_gen_1183
<z, cons>(q_gen_1157, q_gen_1156) -> q_gen_1248
<z, cons>(q_gen_1157, q_gen_1187) -> q_gen_1248
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1172) -> q_gen_1131
<s, cons, nil>(q_gen_1136, q_gen_1135) -> q_gen_1131
<s, nil, nil>(q_gen_1133) -> q_gen_1131
<z, cons, cons>(q_gen_1141, q_gen_1140, q_gen_1139, q_gen_1138) -> q_gen_1131
<z, nil, nil>() -> q_gen_1131
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1173, q_gen_1131) -> q_gen_1172
<s, cons, cons>(q_gen_1175, q_gen_1174, q_gen_1178, q_gen_1172) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1183) -> q_gen_1172
<s, cons, nil>(q_gen_1136, q_gen_1248) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1157, q_gen_1187) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1156) -> q_gen_1172
<z, cons, nil>(q_gen_1164, q_gen_1187) -> q_gen_1172
<s, cons, a>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, a>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1135) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1183) -> q_gen_1173
<s, cons, b>(q_gen_1136, q_gen_1248) -> q_gen_1173
<z, cons, a>(q_gen_1164, q_gen_1156) -> q_gen_1173
<z, cons, b>(q_gen_1157, q_gen_1156) -> q_gen_1173
<s, a, nil>(q_gen_1133) -> q_gen_1174
<s, b, nil>(q_gen_1133) -> q_gen_1174
<z, a, nil>() -> q_gen_1174
<z, b, nil>() -> q_gen_1174
<s, a, a>(q_gen_1133) -> q_gen_1175
<s, a, b>(q_gen_1133) -> q_gen_1175
<s, b, a>(q_gen_1133) -> q_gen_1175
<s, b, b>(q_gen_1133) -> q_gen_1175
<z, a, a>() -> q_gen_1175
<z, a, b>() -> q_gen_1175
<z, b, a>() -> q_gen_1175
<z, b, b>() -> q_gen_1175
<s, cons, a>(q_gen_1136, q_gen_1248) -> q_gen_1178
<z, cons, a>(q_gen_1164, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1157, q_gen_1187) -> q_gen_1178
<z, cons, b>(q_gen_1164, q_gen_1156) -> q_gen_1178
}

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

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

Teacher's answer:
New clause system:
{
() -> drop([s(u), nil, nil]) -> 49  ;  () -> drop([z, l, l]) -> 52  ;  (drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]) -> 61  ;  (drop([u, x3, _um])) -> drop([s(u), cons(x2, x3), _um]) -> 61
}
Sat witness: Yes: ((drop([n, l1, _an]) /\ drop([s(n), cons(x, l1), _zm])) -> eq_eltlist([_zm, _an]), {
_an -> cons(a, nil)  ;  _zm -> cons(b, nil)  ;  l1 -> cons(a, cons(a, nil))  ;  n -> s(z)  ;  x -> b
})

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