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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(butlast, F:
{() -> butlast([cons(y, nil), nil])
() -> butlast([nil, nil])
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)])}
(butlast([_nfa, _ofa]) /\ butlast([_nfa, _pfa])) -> eq_eltlist([_ofa, _pfa])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)])}
(append([_rfa, _sfa, _tfa]) /\ append([_rfa, _sfa, _ufa])) -> eq_eltlist([_tfa, _ufa])
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> butlast([cons(y, nil), nil]) -> 0
() -> butlast([nil, nil]) -> 0
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 0
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 0
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 0
}


Solving took 68.120540 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6142, q_gen_6143, q_gen_6147, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6156, q_gen_6157, q_gen_6158, q_gen_6159, q_gen_6160, q_gen_6161, q_gen_6162, q_gen_6163, q_gen_6164, q_gen_6165, q_gen_6166, q_gen_6167, q_gen_6168, q_gen_6169, q_gen_6170, q_gen_6171, q_gen_6173, q_gen_6174, q_gen_6175, q_gen_6176, q_gen_6177, q_gen_6178, q_gen_6180, q_gen_6181, q_gen_6182, q_gen_6183, q_gen_6185, q_gen_6186, q_gen_6187, q_gen_6188, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6196, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6201, q_gen_6202, q_gen_6203, q_gen_6204, q_gen_6205, q_gen_6206, q_gen_6207, q_gen_6208, q_gen_6209, q_gen_6210, q_gen_6215, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6219, q_gen_6220, q_gen_6221, q_gen_6222, q_gen_6223, q_gen_6224, q_gen_6225, q_gen_6226, q_gen_6227, q_gen_6228, q_gen_6229, q_gen_6230, q_gen_6231, q_gen_6232, q_gen_6233, q_gen_6234, q_gen_6235, q_gen_6236, q_gen_6237, q_gen_6238, q_gen_6239, q_gen_6240, q_gen_6241, q_gen_6243, q_gen_6244, q_gen_6245, q_gen_6246, q_gen_6247, q_gen_6248, q_gen_6249, q_gen_6250, q_gen_6251, q_gen_6252, q_gen_6253, q_gen_6254, q_gen_6255, q_gen_6256, q_gen_6257, q_gen_6258, q_gen_6259, q_gen_6260, q_gen_6261, q_gen_6262, q_gen_6263, q_gen_6264, q_gen_6265, q_gen_6266, q_gen_6267, q_gen_6268, q_gen_6269, q_gen_6270, q_gen_6271, q_gen_6272, q_gen_6273, q_gen_6274, q_gen_6275, q_gen_6276, q_gen_6277, q_gen_6278, q_gen_6279, q_gen_6280, q_gen_6281, q_gen_6282, q_gen_6283, q_gen_6284, q_gen_6285, q_gen_6286, q_gen_6287, q_gen_6288, q_gen_6289, q_gen_6290, q_gen_6291, q_gen_6292, q_gen_6293, q_gen_6294, q_gen_6295, q_gen_6296, q_gen_6297, q_gen_6298, q_gen_6299, q_gen_6300, q_gen_6301, q_gen_6302, q_gen_6303, q_gen_6304, q_gen_6305, q_gen_6306, q_gen_6307},
Q_f={},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<a>() -> q_gen_6168
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6142
<a, a>() -> q_gen_6143
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6164
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons>(q_gen_6138, q_gen_6194) -> q_gen_6193
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6194
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6200
<cons, cons>(q_gen_6143, q_gen_6164) -> q_gen_6203
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6207
<b, a>() -> q_gen_6208
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6217
<nil, cons>(q_gen_6168, q_gen_6150) -> q_gen_6221
<a, b>() -> q_gen_6222
<cons, cons>(q_gen_6138, q_gen_6217) -> q_gen_6231
<cons, cons>(q_gen_6222, q_gen_6158) -> q_gen_6234
<cons, cons>(q_gen_6208, q_gen_6194) -> q_gen_6236
<cons, cons>(q_gen_6222, q_gen_6181) -> q_gen_6241
<cons, cons>(q_gen_6222, q_gen_6217) -> q_gen_6245
<cons, cons>(q_gen_6138, q_gen_6250) -> q_gen_6249
<nil, cons>(q_gen_6168, q_gen_6177) -> q_gen_6250
<cons, cons>(q_gen_6208, q_gen_6217) -> q_gen_6268
<cons, cons>(q_gen_6208, q_gen_6250) -> q_gen_6271
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6281
<cons, cons>(q_gen_6222, q_gen_6137) -> q_gen_6284
<cons, cons>(q_gen_6222, q_gen_6291) -> q_gen_6290
<cons, cons>(q_gen_6138, q_gen_6284) -> q_gen_6291
<cons, cons>(q_gen_6138, q_gen_6234) -> q_gen_6294
<cons, cons>(q_gen_6138, q_gen_6300) -> q_gen_6299
<cons, cons>(q_gen_6143, q_gen_6301) -> q_gen_6300
<cons, cons>(q_gen_6143, q_gen_6194) -> q_gen_6301
<cons, cons>(q_gen_6222, q_gen_6305) -> q_gen_6304
<cons, cons>(q_gen_6143, q_gen_6217) -> q_gen_6305
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6147
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6148
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, cons, cons>(q_gen_6152, q_gen_6157) -> q_gen_6156
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6157
<cons, cons, cons>(q_gen_6160, q_gen_6149) -> q_gen_6159
<a, b, a>() -> q_gen_6160
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6161
<cons, cons, cons>(q_gen_6152, q_gen_6163) -> q_gen_6162
<cons, nil, cons>(q_gen_6138, q_gen_6164) -> q_gen_6163
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6165
<cons, cons, cons>(q_gen_6169, q_gen_6167) -> q_gen_6166
<nil, nil, cons>(q_gen_6168, q_gen_6150) -> q_gen_6167
<b, a, b>() -> q_gen_6169
<cons, cons, cons>(q_gen_6171, q_gen_6167) -> q_gen_6170
<a, a, a>() -> q_gen_6171
<cons, cons, cons>(q_gen_6160, q_gen_6161) -> q_gen_6173
<cons, cons, cons>(q_gen_6160, q_gen_6175) -> q_gen_6174
<cons, cons, cons>(q_gen_6160, q_gen_6176) -> q_gen_6175
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6178
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6180
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6182
<cons, cons, cons>(q_gen_6152, q_gen_6180) -> q_gen_6183
<cons, cons, cons>(q_gen_6152, q_gen_6186) -> q_gen_6185
<nil, cons, cons>(q_gen_6138, q_gen_6164) -> q_gen_6186
<cons, cons, cons>(q_gen_6160, q_gen_6188) -> q_gen_6187
<cons, cons, cons>(q_gen_6152, q_gen_6182) -> q_gen_6188
<nil, cons, cons>(q_gen_6138, q_gen_6193) -> q_gen_6192
<cons, cons, cons>(q_gen_6152, q_gen_6196) -> q_gen_6195
<cons, cons, cons>(q_gen_6160, q_gen_6147) -> q_gen_6196
<cons, cons, cons>(q_gen_6160, q_gen_6198) -> q_gen_6197
<cons, cons, cons>(q_gen_6152, q_gen_6159) -> q_gen_6198
<cons, nil, cons>(q_gen_6138, q_gen_6200) -> q_gen_6199
<cons, cons, cons>(q_gen_6152, q_gen_6202) -> q_gen_6201
<nil, cons, cons>(q_gen_6143, q_gen_6203) -> q_gen_6202
<cons, cons, cons>(q_gen_6160, q_gen_6205) -> q_gen_6204
<cons, cons, cons>(q_gen_6169, q_gen_6206) -> q_gen_6205
<nil, cons, cons>(q_gen_6143, q_gen_6207) -> q_gen_6206
<cons, cons, cons>(q_gen_6152, q_gen_6210) -> q_gen_6209
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6210
<nil, cons, cons>(q_gen_6138, q_gen_6194) -> q_gen_6215
<cons, nil, cons>(q_gen_6138, q_gen_6217) -> q_gen_6216
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6218
<cons, cons, cons>(q_gen_6160, q_gen_6220) -> q_gen_6219
<nil, cons, cons>(q_gen_6222, q_gen_6221) -> q_gen_6220
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6223
<nil, cons, cons>(q_gen_6222, q_gen_6181) -> q_gen_6224
<nil, cons, cons>(q_gen_6222, q_gen_6158) -> q_gen_6225
<cons, cons, cons>(q_gen_6169, q_gen_6227) -> q_gen_6226
<cons, cons, cons>(q_gen_6169, q_gen_6216) -> q_gen_6227
<cons, cons, cons>(q_gen_6169, q_gen_6229) -> q_gen_6228
<cons, cons, cons>(q_gen_6169, q_gen_6230) -> q_gen_6229
<cons, nil, cons>(q_gen_6138, q_gen_6231) -> q_gen_6230
<cons, cons, cons>(q_gen_6152, q_gen_6233) -> q_gen_6232
<cons, nil, cons>(q_gen_6138, q_gen_6234) -> q_gen_6233
<nil, cons, cons>(q_gen_6222, q_gen_6236) -> q_gen_6235
<cons, cons, cons>(q_gen_6169, q_gen_6238) -> q_gen_6237
<nil, cons, cons>(q_gen_6138, q_gen_6217) -> q_gen_6238
<cons, cons, cons>(q_gen_6152, q_gen_6240) -> q_gen_6239
<cons, nil, cons>(q_gen_6138, q_gen_6241) -> q_gen_6240
<cons, cons, cons>(q_gen_6169, q_gen_6244) -> q_gen_6243
<nil, cons, cons>(q_gen_6143, q_gen_6245) -> q_gen_6244
<cons, cons, cons>(q_gen_6171, q_gen_6247) -> q_gen_6246
<cons, cons, cons>(q_gen_6169, q_gen_6248) -> q_gen_6247
<nil, cons, cons>(q_gen_6143, q_gen_6249) -> q_gen_6248
<cons, cons, cons>(q_gen_6169, q_gen_6252) -> q_gen_6251
<cons, cons, cons>(q_gen_6152, q_gen_6215) -> q_gen_6252
<cons, cons, cons>(q_gen_6169, q_gen_6254) -> q_gen_6253
<cons, cons, cons>(q_gen_6152, q_gen_6255) -> q_gen_6254
<cons, cons, cons>(q_gen_6152, q_gen_6161) -> q_gen_6255
<cons, cons, cons>(q_gen_6171, q_gen_6257) -> q_gen_6256
<cons, cons, cons>(q_gen_6160, q_gen_6133) -> q_gen_6257
<cons, cons, cons>(q_gen_6171, q_gen_6259) -> q_gen_6258
<cons, cons, cons>(q_gen_6160, q_gen_6260) -> q_gen_6259
<cons, nil, cons>(q_gen_6143, q_gen_6137) -> q_gen_6260
<cons, cons, cons>(q_gen_6152, q_gen_6262) -> q_gen_6261
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6262
<cons, cons, cons>(q_gen_6169, q_gen_6133) -> q_gen_6263
<cons, cons, cons>(q_gen_6171, q_gen_6149) -> q_gen_6264
<cons, cons, cons>(q_gen_6169, q_gen_6266) -> q_gen_6265
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6266
<nil, cons, cons>(q_gen_6138, q_gen_6268) -> q_gen_6267
<cons, cons, cons>(q_gen_6160, q_gen_6270) -> q_gen_6269
<nil, cons, cons>(q_gen_6138, q_gen_6271) -> q_gen_6270
<cons, cons, cons>(q_gen_6152, q_gen_6273) -> q_gen_6272
<cons, nil, cons>(q_gen_6138, q_gen_6194) -> q_gen_6273
<cons, cons, cons>(q_gen_6152, q_gen_6275) -> q_gen_6274
<nil, cons, cons>(q_gen_6143, q_gen_6164) -> q_gen_6275
<cons, cons, cons>(q_gen_6160, q_gen_6277) -> q_gen_6276
<cons, cons, cons>(q_gen_6169, q_gen_6278) -> q_gen_6277
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6278
<cons, cons, cons>(q_gen_6152, q_gen_6280) -> q_gen_6279
<cons, nil, cons>(q_gen_6138, q_gen_6281) -> q_gen_6280
<cons, nil, cons>(q_gen_6222, q_gen_6137) -> q_gen_6282
<cons, nil, cons>(q_gen_6138, q_gen_6284) -> q_gen_6283
<cons, cons, cons>(q_gen_6152, q_gen_6286) -> q_gen_6285
<nil, cons, cons>(q_gen_6222, q_gen_6137) -> q_gen_6286
<cons, cons, cons>(q_gen_6160, q_gen_6288) -> q_gen_6287
<cons, cons, cons>(q_gen_6169, q_gen_6149) -> q_gen_6288
<nil, cons, cons>(q_gen_6143, q_gen_6290) -> q_gen_6289
<cons, cons, cons>(q_gen_6169, q_gen_6293) -> q_gen_6292
<nil, cons, cons>(q_gen_6143, q_gen_6294) -> q_gen_6293
<nil, cons, cons>(q_gen_6143, q_gen_6231) -> q_gen_6295
<cons, cons, cons>(q_gen_6171, q_gen_6297) -> q_gen_6296
<nil, cons, cons>(q_gen_6208, q_gen_6249) -> q_gen_6297
<nil, cons, cons>(q_gen_6138, q_gen_6299) -> q_gen_6298
<cons, cons, cons>(q_gen_6160, q_gen_6303) -> q_gen_6302
<nil, cons, cons>(q_gen_6138, q_gen_6304) -> q_gen_6303
<cons, cons, cons>(q_gen_6160, q_gen_6257) -> q_gen_6306
<cons, cons, cons>(q_gen_6152, q_gen_6259) -> q_gen_6307
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6134, q_gen_6135, q_gen_6139, q_gen_6140, q_gen_6144, q_gen_6145, q_gen_6146, q_gen_6153, q_gen_6154, q_gen_6172, q_gen_6179, q_gen_6184, q_gen_6189, q_gen_6190, q_gen_6191, q_gen_6211, q_gen_6212, q_gen_6213, q_gen_6214, q_gen_6242},
Q_f={},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<a>() -> q_gen_6140
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6134
<b, b>() -> q_gen_6135
<cons, nil>(q_gen_6140, q_gen_6131) -> q_gen_6139
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6146, q_gen_6144) -> q_gen_6145
<a, a>() -> q_gen_6146
<cons, cons>(q_gen_6135, q_gen_6139) -> q_gen_6153
<cons, cons>(q_gen_6135, q_gen_6153) -> q_gen_6154
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6172
<cons, cons>(q_gen_6135, q_gen_6134) -> q_gen_6179
<cons, cons>(q_gen_6135, q_gen_6179) -> q_gen_6184
<cons, cons>(q_gen_6135, q_gen_6190) -> q_gen_6189
<cons, cons>(q_gen_6146, q_gen_6139) -> q_gen_6190
<cons, cons>(q_gen_6135, q_gen_6189) -> q_gen_6191
<cons, cons>(q_gen_6135, q_gen_6212) -> q_gen_6211
<cons, cons>(q_gen_6146, q_gen_6130) -> q_gen_6212
<cons, cons>(q_gen_6146, q_gen_6153) -> q_gen_6213
<cons, cons>(q_gen_6135, q_gen_6213) -> q_gen_6214
<cons, cons>(q_gen_6135, q_gen_6184) -> q_gen_6242
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005224 s (model generation: 0.004505,  model checking: 0.000719):

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

}

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

}

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

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

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

})

-------------------------------------------
Step 1, which took 0.005073 s (model generation: 0.004818,  model checking: 0.000255):

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.004824 s (model generation: 0.004441,  model checking: 0.000383):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
}

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

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

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

-------------------------------------------
Step 3, which took 0.004859 s (model generation: 0.004293,  model checking: 0.000566):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
}

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

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

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

-------------------------------------------
Step 4, which took 0.004591 s (model generation: 0.004375,  model checking: 0.000216):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 5, which took 0.005223 s (model generation: 0.004900,  model checking: 0.000323):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138},
Q_f={q_gen_6133},
Delta=
{
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 6, which took 0.008339 s (model generation: 0.007570,  model checking: 0.000769):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138},
Q_f={q_gen_6133},
Delta=
{
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 7, which took 0.011522 s (model generation: 0.011063,  model checking: 0.000459):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138},
Q_f={q_gen_6133},
Delta=
{
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 8, which took 0.013336 s (model generation: 0.012844,  model checking: 0.000492):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138},
Q_f={q_gen_6133},
Delta=
{
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 9, which took 0.015197 s (model generation: 0.013336,  model checking: 0.001861):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138},
Q_f={q_gen_6133},
Delta=
{
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 10, which took 0.013205 s (model generation: 0.012606,  model checking: 0.000599):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6147, q_gen_6150, q_gen_6151, q_gen_6152},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6142
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6147) -> q_gen_6147
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6147
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6147
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6131, q_gen_6132, q_gen_6135},
Q_f={q_gen_6129},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
}

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

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

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

-------------------------------------------
Step 11, which took 0.006697 s (model generation: 0.005553,  model checking: 0.001144):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6150, q_gen_6151, q_gen_6152},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 12, which took 0.016137 s (model generation: 0.015430,  model checking: 0.000707):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6150, q_gen_6151, q_gen_6152},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 13, which took 0.018265 s (model generation: 0.015911,  model checking: 0.002354):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 14, which took 0.024701 s (model generation: 0.017365,  model checking: 0.007336):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 15, which took 0.015443 s (model generation: 0.014013,  model checking: 0.001430):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, b, a>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 16, which took 0.023647 s (model generation: 0.010497,  model checking: 0.013150):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, b, a>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 17, which took 0.034455 s (model generation: 0.021808,  model checking: 0.012647):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, b, a>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 18, which took 0.033477 s (model generation: 0.025825,  model checking: 0.007652):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 19, which took 0.027577 s (model generation: 0.020917,  model checking: 0.006660):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 20, which took 0.056106 s (model generation: 0.028481,  model checking: 0.027625):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 21, which took 0.040887 s (model generation: 0.036571,  model checking: 0.004316):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6150
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6141
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 22, which took 0.057277 s (model generation: 0.040695,  model checking: 0.016582):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 23, which took 0.048658 s (model generation: 0.044504,  model checking: 0.004154):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 24, which took 0.049519 s (model generation: 0.047336,  model checking: 0.002183):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158},
Q_f={q_gen_6133, q_gen_6148},
Delta=
{
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6150
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6148) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6148
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6140, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<a>() -> q_gen_6140
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6129
<cons, nil>(q_gen_6140, q_gen_6131) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 25, which took 0.051828 s (model generation: 0.046687,  model checking: 0.005141):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 26, which took 0.064288 s (model generation: 0.052823,  model checking: 0.011465):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 27, which took 0.070790 s (model generation: 0.068165,  model checking: 0.002625):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133, q_gen_6148},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6158
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6148) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6148
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6134, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130, q_gen_6134},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6134) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6134
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 28, which took 0.086523 s (model generation: 0.084224,  model checking: 0.002299):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6150
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6139, q_gen_6140, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130, q_gen_6139},
Delta=
{
<nil>() -> q_gen_6131
<b>() -> q_gen_6132
<a>() -> q_gen_6140
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6139) -> q_gen_6139
<cons, nil>(q_gen_6140, q_gen_6131) -> q_gen_6139
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 29, which took 0.079260 s (model generation: 0.078453,  model checking: 0.000807):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6142
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6142
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6142) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 30, which took 0.077555 s (model generation: 0.067909,  model checking: 0.009646):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6148},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6148) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6148
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 31, which took 0.112507 s (model generation: 0.086945,  model checking: 0.025562):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6182},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6182) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 32, which took 0.133420 s (model generation: 0.077271,  model checking: 0.056149):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6148, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6148},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6148) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6148
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> butlast([cons(y, nil), nil]) -> 26
() -> butlast([nil, nil]) -> 26
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 40
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 33
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 34
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, cons(a, cons(b, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 33, which took 0.098373 s (model generation: 0.097236,  model checking: 0.001137):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6182},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6182) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> butlast([cons(y, nil), nil]) -> 27
() -> butlast([nil, nil]) -> 27
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 40
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 36
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 34
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(a, cons(b, nil)))  ;  _wfa -> cons(b, cons(a, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 34, which took 0.083044 s (model generation: 0.081747,  model checking: 0.001297):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6158
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6136
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6136
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6136
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6134, q_gen_6135, q_gen_6144, q_gen_6146},
Q_f={q_gen_6129, q_gen_6130, q_gen_6134},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6135, q_gen_6134) -> q_gen_6129
<cons, cons>(q_gen_6146, q_gen_6130) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6134
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
<cons, cons>(q_gen_6146, q_gen_6144) -> q_gen_6144
<a, a>() -> q_gen_6146
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> butlast([cons(y, nil), nil]) -> 28
() -> butlast([nil, nil]) -> 28
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 40
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 36
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 37
}
Sat witness: Found: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(b, nil)  ;  x2 -> b  ;  x3 -> cons(a, nil)  ;  y -> a
})

-------------------------------------------
Step 35, which took 0.066162 s (model generation: 0.064270,  model checking: 0.001892):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6161, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6161) -> q_gen_6161
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6161
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144, q_gen_6146},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<cons, cons>(q_gen_6146, q_gen_6130) -> q_gen_6129
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
<cons, cons>(q_gen_6146, q_gen_6144) -> q_gen_6144
<a, a>() -> q_gen_6146
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
() -> butlast([cons(y, nil), nil]) -> 29
() -> butlast([nil, nil]) -> 29
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 40
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 37
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 40
}
Sat witness: Found: ((butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]), {
_mfa -> cons(a, cons(b, nil))  ;  x2 -> a  ;  x3 -> cons(b, cons(a, nil))  ;  y -> b
})

-------------------------------------------
Step 36, which took 0.147559 s (model generation: 0.147017,  model checking: 0.000542):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6142
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6142
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6142
<a, a>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6142) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, nil, cons>(q_gen_6138, q_gen_6142) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> butlast([cons(y, nil), nil]) -> 30
() -> butlast([nil, nil]) -> 30
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 40
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 37
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 40
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 0.122463 s (model generation: 0.099243,  model checking: 0.023220):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6182, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6182) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

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

-------------------------------------------
Step 38, which took 0.141511 s (model generation: 0.128643,  model checking: 0.012868):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<b, a>() -> q_gen_6208
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6141
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> butlast([cons(y, nil), nil]) -> 32
() -> butlast([nil, nil]) -> 32
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 46
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 39
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 42
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.122741 s (model generation: 0.122195,  model checking: 0.000546):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6142
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6142
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6142
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6136
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6155
<cons, nil, cons>(q_gen_6138, q_gen_6142) -> q_gen_6155
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> butlast([cons(y, nil), nil]) -> 33
() -> butlast([nil, nil]) -> 33
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 46
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 39
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 42
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 40, which took 0.151164 s (model generation: 0.150206,  model checking: 0.000958):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6136, q_gen_6137, q_gen_6138, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6136},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6136) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6136
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6136
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6136
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> butlast([cons(y, nil), nil]) -> 34
() -> butlast([nil, nil]) -> 34
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 46
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 42
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 42
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, nil))  ;  _wfa -> cons(b, nil)  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 41, which took 0.182037 s (model generation: 0.180688,  model checking: 0.001349):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
() -> butlast([cons(y, nil), nil]) -> 35
() -> butlast([nil, nil]) -> 35
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 46
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 45
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 43
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(b, nil)))  ;  _wfa -> cons(b, cons(b, nil))  ;  x -> a  ;  ys -> nil
})

-------------------------------------------
Step 42, which took 0.194137 s (model generation: 0.192962,  model checking: 0.001175):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6155
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
() -> butlast([cons(y, nil), nil]) -> 36
() -> butlast([nil, nil]) -> 36
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 46
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 48
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 44
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, nil))  ;  _wfa -> cons(b, nil)  ;  x -> a  ;  ys -> nil
})

-------------------------------------------
Step 43, which took 0.186906 s (model generation: 0.180986,  model checking: 0.005920):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
() -> butlast([cons(y, nil), nil]) -> 37
() -> butlast([nil, nil]) -> 37
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 49
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 48
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 45
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(b, cons(b, cons(b, cons(b, nil))))
})

-------------------------------------------
Step 44, which took 0.345255 s (model generation: 0.344469,  model checking: 0.000786):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6143, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6142
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6142
<cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6142
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6142) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6142) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 47
() -> butlast([cons(y, nil), nil]) -> 38
() -> butlast([nil, nil]) -> 38
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 49
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 48
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 45
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 45, which took 0.243904 s (model generation: 0.241379,  model checking: 0.002525):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 48
() -> butlast([cons(y, nil), nil]) -> 39
() -> butlast([nil, nil]) -> 39
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 49
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 51
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 46
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _wfa -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 46, which took 0.260340 s (model generation: 0.251012,  model checking: 0.009328):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 49
() -> butlast([cons(y, nil), nil]) -> 40
() -> butlast([nil, nil]) -> 40
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 52
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 51
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 47
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 47, which took 0.286092 s (model generation: 0.284212,  model checking: 0.001880):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 50
() -> butlast([cons(y, nil), nil]) -> 41
() -> butlast([nil, nil]) -> 41
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 52
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 54
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 48
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  _wfa -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 48, which took 0.408035 s (model generation: 0.400551,  model checking: 0.007484):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 51
() -> butlast([cons(y, nil), nil]) -> 42
() -> butlast([nil, nil]) -> 42
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 55
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 54
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 49
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, cons(b, cons(a, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, cons(a, cons(b, nil))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 49, which took 0.384939 s (model generation: 0.377049,  model checking: 0.007890):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 52
() -> butlast([cons(y, nil), nil]) -> 43
() -> butlast([nil, nil]) -> 43
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 58
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 55
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 50
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 50, which took 1.870116 s (model generation: 0.873484,  model checking: 0.996632):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
() -> butlast([cons(y, nil), nil]) -> 44
() -> butlast([nil, nil]) -> 44
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 61
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 56
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 51
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 51, which took 0.633953 s (model generation: 0.632420,  model checking: 0.001533):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6141, q_gen_6143, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6155, q_gen_6158, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133, q_gen_6141},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6141) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6155) -> q_gen_6141
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6141
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6141
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6141
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6155
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<cons, nil, cons>(q_gen_6143, q_gen_6137) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6155
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6155
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 54
() -> butlast([cons(y, nil), nil]) -> 45
() -> butlast([nil, nil]) -> 45
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 61
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 59
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 52
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(a, nil))  ;  _wfa -> cons(b, nil)  ;  x -> b  ;  ys -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 52, which took 0.795472 s (model generation: 0.794130,  model checking: 0.001342):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6143, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6160, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6133) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<b, b, b>() -> q_gen_6152
<a, a, a>() -> q_gen_6160
<a, b, a>() -> q_gen_6160
<b, a, b>() -> q_gen_6160
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 55
() -> butlast([cons(y, nil), nil]) -> 46
() -> butlast([nil, nil]) -> 46
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 61
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 62
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 53
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, nil)  ;  _wfa -> nil  ;  x -> a  ;  ys -> cons(b, nil)
})

-------------------------------------------
Step 53, which took 1.132980 s (model generation: 1.129616,  model checking: 0.003364):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6143, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6160, q_gen_6177, q_gen_6181},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<b, b>() -> q_gen_6138
<a, a>() -> q_gen_6143
<a, b>() -> q_gen_6143
<b, a>() -> q_gen_6143
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6133) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6143, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6143, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6143, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<a, b, a>() -> q_gen_6160
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 56
() -> butlast([cons(y, nil), nil]) -> 47
() -> butlast([nil, nil]) -> 47
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 64
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 62
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 54
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 54, which took 2.401932 s (model generation: 2.391573,  model checking: 0.010359):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6182, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6182) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6182
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6182
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6182
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6182
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 57
() -> butlast([cons(y, nil), nil]) -> 48
() -> butlast([nil, nil]) -> 48
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 67
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 63
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 55
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 55, which took 3.244675 s (model generation: 3.242793,  model checking: 0.001882):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6160, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6133) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<a, b, a>() -> q_gen_6160
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 58
() -> butlast([cons(y, nil), nil]) -> 49
() -> butlast([nil, nil]) -> 49
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 67
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 66
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 56
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(a, nil)  ;  _wfa -> nil  ;  x -> b  ;  ys -> cons(a, nil)
})

-------------------------------------------
Step 56, which took 2.209219 s (model generation: 2.206848,  model checking: 0.002371):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6142, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6142) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6142
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6142
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6142) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6142) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 59
() -> butlast([cons(y, nil), nil]) -> 50
() -> butlast([nil, nil]) -> 50
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 67
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 69
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 57
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(b, nil)))  ;  _wfa -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 57, which took 1.575712 s (model generation: 1.566748,  model checking: 0.008964):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6176
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 60
() -> butlast([cons(y, nil), nil]) -> 51
() -> butlast([nil, nil]) -> 51
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 70
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 69
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 58
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(a, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 58, which took 1.715844 s (model generation: 1.713863,  model checking: 0.001981):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 61
() -> butlast([cons(y, nil), nil]) -> 52
() -> butlast([nil, nil]) -> 52
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 70
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 72
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 59
}
Sat witness: Found: ((append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]), {
_vfa -> cons(b, cons(b, cons(a, nil)))  ;  _wfa -> cons(b, cons(b, nil))  ;  x -> b  ;  ys -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 59, which took 4.323941 s (model generation: 4.322064,  model checking: 0.001877):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6176
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 62
() -> butlast([cons(y, nil), nil]) -> 53
() -> butlast([nil, nil]) -> 53
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 73
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 72
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 60
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 60, which took 7.138204 s (model generation: 7.128557,  model checking: 0.009647):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6164, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6164
<cons, cons>(q_gen_6138, q_gen_6164) -> q_gen_6164
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6164) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6164) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 63
() -> butlast([cons(y, nil), nil]) -> 54
() -> butlast([nil, nil]) -> 54
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 76
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 73
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 61
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 61, which took 3.866190 s (model generation: 3.855827,  model checking: 0.010363):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6176
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 64
() -> butlast([cons(y, nil), nil]) -> 55
() -> butlast([nil, nil]) -> 55
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 79
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 74
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 62
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, cons(b, cons(a, nil))))  ;  t1 -> nil
})

-------------------------------------------
Step 62, which took 9.879712 s (model generation: 9.874020,  model checking: 0.005692):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6137
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6176
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6176
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 65
() -> butlast([cons(y, nil), nil]) -> 56
() -> butlast([nil, nil]) -> 56
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 82
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 75
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 63
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, cons(b, cons(a, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 63, which took 2.302354 s (model generation: 2.294554,  model checking: 0.007800):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6176, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, cons, cons>(q_gen_6152, q_gen_6176) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<a, b, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6176
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6176
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6176
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 66
() -> butlast([cons(y, nil), nil]) -> 57
() -> butlast([nil, nil]) -> 57
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 85
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 76
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 64
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(b, cons(b, cons(a, cons(a, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(a, cons(a, cons(b, nil)))))  ;  t1 -> nil
})

-------------------------------------------
Step 64, which took 12.024836 s (model generation: 12.018376,  model checking: 0.006460):

Model:
|_
{
append -> 
{{{
Q={q_gen_6133, q_gen_6137, q_gen_6138, q_gen_6149, q_gen_6150, q_gen_6151, q_gen_6152, q_gen_6158, q_gen_6160, q_gen_6175, q_gen_6177, q_gen_6181, q_gen_6208},
Q_f={q_gen_6133},
Delta=
{
<nil>() -> q_gen_6150
<a>() -> q_gen_6151
<b>() -> q_gen_6151
<cons>(q_gen_6151, q_gen_6150) -> q_gen_6177
<cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6137
<nil, nil>() -> q_gen_6137
<a, a>() -> q_gen_6138
<b, b>() -> q_gen_6138
<cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6158
<nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6158
<cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6181
<cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6181
<nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6181
<a, b>() -> q_gen_6208
<b, a>() -> q_gen_6208
<cons, cons, cons>(q_gen_6152, q_gen_6149) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6149) -> q_gen_6133
<cons, cons, cons>(q_gen_6160, q_gen_6175) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6138, q_gen_6181) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<cons, nil, cons>(q_gen_6208, q_gen_6158) -> q_gen_6133
<nil, cons, cons>(q_gen_6138, q_gen_6137) -> q_gen_6133
<nil, cons, cons>(q_gen_6208, q_gen_6137) -> q_gen_6133
<nil, nil, cons>(q_gen_6151, q_gen_6177) -> q_gen_6133
<nil, nil, nil>() -> q_gen_6133
<cons, cons, cons>(q_gen_6152, q_gen_6133) -> q_gen_6149
<cons, nil, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6138, q_gen_6158) -> q_gen_6149
<nil, cons, cons>(q_gen_6208, q_gen_6158) -> q_gen_6149
<nil, nil, cons>(q_gen_6151, q_gen_6150) -> q_gen_6149
<a, a, a>() -> q_gen_6152
<b, a, b>() -> q_gen_6152
<b, b, b>() -> q_gen_6152
<a, b, a>() -> q_gen_6160
<cons, cons, cons>(q_gen_6152, q_gen_6175) -> q_gen_6175
<cons, cons, cons>(q_gen_6160, q_gen_6133) -> q_gen_6175
<nil, cons, cons>(q_gen_6138, q_gen_6181) -> q_gen_6175
<nil, cons, cons>(q_gen_6208, q_gen_6181) -> q_gen_6175
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  butlast -> 
{{{
Q={q_gen_6129, q_gen_6130, q_gen_6131, q_gen_6132, q_gen_6135, q_gen_6144},
Q_f={q_gen_6129, q_gen_6130},
Delta=
{
<nil>() -> q_gen_6131
<a>() -> q_gen_6132
<b>() -> q_gen_6132
<nil, nil>() -> q_gen_6129
<cons, cons>(q_gen_6135, q_gen_6130) -> q_gen_6130
<cons, nil>(q_gen_6132, q_gen_6131) -> q_gen_6130
<a, a>() -> q_gen_6135
<b, b>() -> q_gen_6135
<cons, cons>(q_gen_6135, q_gen_6129) -> q_gen_6144
<cons, cons>(q_gen_6135, q_gen_6144) -> q_gen_6144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 67
() -> butlast([cons(y, nil), nil]) -> 58
() -> butlast([nil, nil]) -> 58
(append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]) -> 88
(append([ys, cons(x, nil), _vfa]) /\ butlast([_vfa, _wfa])) -> eq_eltlist([_wfa, ys]) -> 77
(butlast([cons(x2, x3), _mfa])) -> butlast([cons(y, cons(x2, x3)), cons(y, _mfa)]) -> 65
}
Sat witness: Found: ((append([t1, l2, _qfa])) -> append([cons(h1, t1), l2, cons(h1, _qfa)]), {
_qfa -> cons(a, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, cons(a, nil))
})

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