Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} ; nat -> {s, z} } definition: { (append, F: {() -> append([nil, l2, l2]) (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)])} (append([_jx, _kx, _lx]) /\ append([_jx, _kx, _mx])) -> eq_eltlist([_lx, _mx]) ) (length, F: {() -> length([nil, z]) (length([ll, _nx])) -> length([cons(x, ll), s(_nx)])} (length([_ox, _px]) /\ length([_ox, _qx])) -> eq_nat([_px, _qx]) ) } properties: {(append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux])} over-approximation: {append, length} under-approximation: {} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 0 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 0 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 0 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 0 } Solving took 73.946814 seconds. DontKnow. Stopped because: timeout Working model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6186, q_gen_6187, q_gen_6190, q_gen_6191, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6201, q_gen_6202, q_gen_6203, q_gen_6204, q_gen_6209, q_gen_6210, q_gen_6211, q_gen_6212, q_gen_6213, q_gen_6214, q_gen_6219, q_gen_6220, q_gen_6221, q_gen_6222, q_gen_6223, q_gen_6224, q_gen_6229, q_gen_6230, q_gen_6231, q_gen_6232, q_gen_6233, q_gen_6240, q_gen_6241, q_gen_6242, q_gen_6243, q_gen_6244, q_gen_6245, q_gen_6246, q_gen_6249, q_gen_6250, q_gen_6251, 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_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_6281, q_gen_6282, q_gen_6283, q_gen_6284, q_gen_6285, q_gen_6286, q_gen_6287, q_gen_6289, q_gen_6290, q_gen_6293, q_gen_6294, q_gen_6295, q_gen_6296, 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_gen_6319, q_gen_6320, q_gen_6321, q_gen_6322, q_gen_6323, q_gen_6324, q_gen_6325, q_gen_6330, q_gen_6331, q_gen_6332, q_gen_6333, q_gen_6334, q_gen_6335, q_gen_6336, q_gen_6337, q_gen_6339, q_gen_6340, q_gen_6341, q_gen_6342, q_gen_6343, q_gen_6344, q_gen_6345, q_gen_6346, q_gen_6347, q_gen_6348, q_gen_6349, q_gen_6351, q_gen_6352, q_gen_6353, q_gen_6354, q_gen_6355, q_gen_6356, q_gen_6357}, Q_f={}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6212 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6194, q_gen_6232) -> q_gen_6323 () -> q_gen_6183 () -> q_gen_6184 (q_gen_6187, q_gen_6183) -> q_gen_6186 () -> q_gen_6187 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6212, q_gen_6193) -> q_gen_6221 (q_gen_6184, q_gen_6261) -> q_gen_6260 (q_gen_6184, q_gen_6183) -> q_gen_6261 (q_gen_6184, q_gen_6203) -> q_gen_6271 () -> q_gen_6275 () -> q_gen_6284 (q_gen_6194, q_gen_6232) -> q_gen_6286 (q_gen_6275, q_gen_6286) -> q_gen_6331 (q_gen_6194, q_gen_6323) -> q_gen_6334 (q_gen_6184, q_gen_6286) -> q_gen_6336 (q_gen_6184, q_gen_6186) -> q_gen_6357 () -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6187, q_gen_6186) -> q_gen_6185 (q_gen_6184, q_gen_6183) -> q_gen_6190 (q_gen_6195, q_gen_6192) -> q_gen_6191 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 (q_gen_6204, q_gen_6202) -> q_gen_6201 (q_gen_6184, q_gen_6203) -> q_gen_6202 () -> q_gen_6204 (q_gen_6187, q_gen_6183) -> q_gen_6209 (q_gen_6213, q_gen_6211) -> q_gen_6210 (q_gen_6212, q_gen_6193) -> q_gen_6211 () -> q_gen_6213 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6222, q_gen_6220) -> q_gen_6219 (q_gen_6184, q_gen_6221) -> q_gen_6220 () -> q_gen_6222 (q_gen_6204, q_gen_6192) -> q_gen_6223 (q_gen_6213, q_gen_6192) -> q_gen_6224 (q_gen_6184, q_gen_6203) -> q_gen_6229 (q_gen_6204, q_gen_6231) -> q_gen_6230 (q_gen_6194, q_gen_6232) -> q_gen_6231 (q_gen_6195, q_gen_6231) -> q_gen_6233 (q_gen_6204, q_gen_6241) -> q_gen_6240 (q_gen_6204, q_gen_6178) -> q_gen_6241 (q_gen_6204, q_gen_6243) -> q_gen_6242 (q_gen_6204, q_gen_6244) -> q_gen_6243 (q_gen_6187, q_gen_6183) -> q_gen_6244 (q_gen_6204, q_gen_6191) -> q_gen_6245 (q_gen_6213, q_gen_6233) -> q_gen_6246 (q_gen_6204, q_gen_6229) -> q_gen_6249 (q_gen_6204, q_gen_6230) -> q_gen_6250 (q_gen_6212, q_gen_6232) -> q_gen_6251 (q_gen_6222, q_gen_6257) -> q_gen_6256 (q_gen_6187, q_gen_6221) -> q_gen_6257 (q_gen_6195, q_gen_6244) -> q_gen_6258 (q_gen_6184, q_gen_6260) -> q_gen_6259 (q_gen_6222, q_gen_6233) -> q_gen_6262 (q_gen_6222, q_gen_6191) -> q_gen_6263 (q_gen_6195, q_gen_6266) -> q_gen_6265 (q_gen_6187, q_gen_6186) -> q_gen_6266 (q_gen_6213, q_gen_6231) -> q_gen_6267 (q_gen_6213, q_gen_6202) -> q_gen_6268 (q_gen_6222, q_gen_6270) -> q_gen_6269 (q_gen_6184, q_gen_6271) -> q_gen_6270 (q_gen_6184, q_gen_6186) -> q_gen_6272 (q_gen_6204, q_gen_6274) -> q_gen_6273 (q_gen_6275, q_gen_6221) -> q_gen_6274 (q_gen_6222, q_gen_6192) -> q_gen_6276 (q_gen_6204, q_gen_6209) -> q_gen_6277 (q_gen_6195, q_gen_6279) -> q_gen_6278 (q_gen_6222, q_gen_6211) -> q_gen_6279 (q_gen_6187, q_gen_6261) -> q_gen_6281 (q_gen_6222, q_gen_6283) -> q_gen_6282 (q_gen_6284, q_gen_6203) -> q_gen_6283 (q_gen_6187, q_gen_6286) -> q_gen_6285 (q_gen_6187, q_gen_6203) -> q_gen_6287 (q_gen_6204, q_gen_6182) -> q_gen_6289 (q_gen_6213, q_gen_6190) -> q_gen_6290 (q_gen_6184, q_gen_6261) -> q_gen_6293 (q_gen_6284, q_gen_6271) -> q_gen_6294 (q_gen_6184, q_gen_6186) -> q_gen_6295 (q_gen_6222, q_gen_6231) -> q_gen_6296 (q_gen_6204, q_gen_6300) -> q_gen_6299 (q_gen_6195, q_gen_6190) -> q_gen_6300 (q_gen_6213, q_gen_6302) -> q_gen_6301 (q_gen_6195, q_gen_6202) -> q_gen_6302 (q_gen_6222, q_gen_6304) -> q_gen_6303 (q_gen_6187, q_gen_6221) -> q_gen_6304 (q_gen_6213, q_gen_6283) -> q_gen_6305 (q_gen_6213, q_gen_6307) -> q_gen_6306 (q_gen_6195, q_gen_6251) -> q_gen_6307 (q_gen_6222, q_gen_6320) -> q_gen_6319 (q_gen_6195, q_gen_6321) -> q_gen_6320 (q_gen_6195, q_gen_6322) -> q_gen_6321 (q_gen_6194, q_gen_6323) -> q_gen_6322 (q_gen_6222, q_gen_6325) -> q_gen_6324 (q_gen_6195, q_gen_6233) -> q_gen_6325 (q_gen_6284, q_gen_6331) -> q_gen_6330 (q_gen_6195, q_gen_6333) -> q_gen_6332 (q_gen_6187, q_gen_6334) -> q_gen_6333 (q_gen_6184, q_gen_6336) -> q_gen_6335 (q_gen_6284, q_gen_6261) -> q_gen_6337 (q_gen_6222, q_gen_6340) -> q_gen_6339 (q_gen_6195, q_gen_6341) -> q_gen_6340 (q_gen_6184, q_gen_6286) -> q_gen_6341 (q_gen_6275, q_gen_6183) -> q_gen_6342 (q_gen_6187, q_gen_6286) -> q_gen_6343 (q_gen_6213, q_gen_6345) -> q_gen_6344 (q_gen_6204, q_gen_6346) -> q_gen_6345 (q_gen_6284, q_gen_6183) -> q_gen_6346 (q_gen_6222, q_gen_6348) -> q_gen_6347 (q_gen_6195, q_gen_6349) -> q_gen_6348 (q_gen_6204, q_gen_6211) -> q_gen_6349 (q_gen_6213, q_gen_6352) -> q_gen_6351 (q_gen_6222, q_gen_6349) -> q_gen_6352 (q_gen_6222, q_gen_6354) -> q_gen_6353 (q_gen_6213, q_gen_6355) -> q_gen_6354 (q_gen_6204, q_gen_6304) -> q_gen_6355 (q_gen_6187, q_gen_6357) -> q_gen_6356 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6179, q_gen_6180, q_gen_6181, q_gen_6188, q_gen_6189, q_gen_6196, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6206, q_gen_6207, q_gen_6208, q_gen_6215, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6225, q_gen_6226, q_gen_6227, q_gen_6228, q_gen_6234, q_gen_6235, q_gen_6236, q_gen_6237, q_gen_6238, q_gen_6239, q_gen_6247, q_gen_6248, q_gen_6252, q_gen_6253, q_gen_6254, q_gen_6255, q_gen_6264, q_gen_6280, q_gen_6288, q_gen_6291, q_gen_6292, q_gen_6297, q_gen_6298, q_gen_6308, q_gen_6309, q_gen_6310, q_gen_6311, q_gen_6312, q_gen_6313, q_gen_6314, q_gen_6315, q_gen_6316, q_gen_6317, q_gen_6318, q_gen_6326, q_gen_6327, q_gen_6328, q_gen_6329, q_gen_6338, q_gen_6350}, Q_f={}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6208, q_gen_6180) -> q_gen_6207 () -> q_gen_6208 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6198, q_gen_6216) -> q_gen_6237 (q_gen_6218) -> q_gen_6239 (q_gen_6239) -> q_gen_6310 (q_gen_6208, q_gen_6197) -> q_gen_6313 (q_gen_6208, q_gen_6313) -> q_gen_6318 (q_gen_6198, q_gen_6328) -> q_gen_6327 (q_gen_6198, q_gen_6237) -> q_gen_6328 () -> q_gen_6177 (q_gen_6181, q_gen_6180) -> q_gen_6179 () -> q_gen_6181 (q_gen_6189, q_gen_6180) -> q_gen_6188 () -> q_gen_6189 (q_gen_6199, q_gen_6197) -> q_gen_6196 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6207) -> q_gen_6206 (q_gen_6217, q_gen_6216) -> q_gen_6215 (q_gen_6218) -> q_gen_6217 (q_gen_6189, q_gen_6197) -> q_gen_6225 (q_gen_6199, q_gen_6180) -> q_gen_6226 (q_gen_6228, q_gen_6197) -> q_gen_6227 (q_gen_6218) -> q_gen_6228 (q_gen_6199, q_gen_6216) -> q_gen_6234 (q_gen_6217, q_gen_6197) -> q_gen_6235 (q_gen_6238, q_gen_6237) -> q_gen_6236 (q_gen_6239) -> q_gen_6238 (q_gen_6189, q_gen_6216) -> q_gen_6247 (q_gen_6199, q_gen_6237) -> q_gen_6248 (q_gen_6253, q_gen_6197) -> q_gen_6252 (q_gen_6200) -> q_gen_6253 (q_gen_6253, q_gen_6180) -> q_gen_6254 (q_gen_6217, q_gen_6207) -> q_gen_6255 (q_gen_6253, q_gen_6237) -> q_gen_6264 (q_gen_6228, q_gen_6180) -> q_gen_6280 (q_gen_6228, q_gen_6216) -> q_gen_6288 (q_gen_6238, q_gen_6197) -> q_gen_6291 (q_gen_6217, q_gen_6180) -> q_gen_6292 (q_gen_6298, q_gen_6216) -> q_gen_6297 (q_gen_6239) -> q_gen_6298 (q_gen_6309, q_gen_6216) -> q_gen_6308 (q_gen_6310) -> q_gen_6309 (q_gen_6298, q_gen_6197) -> q_gen_6311 (q_gen_6314, q_gen_6313) -> q_gen_6312 (q_gen_6310) -> q_gen_6314 (q_gen_6228, q_gen_6237) -> q_gen_6315 (q_gen_6228, q_gen_6313) -> q_gen_6316 (q_gen_6298, q_gen_6318) -> q_gen_6317 (q_gen_6228, q_gen_6327) -> q_gen_6326 (q_gen_6253, q_gen_6328) -> q_gen_6329 (q_gen_6217, q_gen_6237) -> q_gen_6338 (q_gen_6181, q_gen_6237) -> q_gen_6350 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.021219 s (model generation: 0.021003, model checking: 0.000216): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 3 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 1 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 1 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 1 } Sat witness: Found: (() -> length([nil, z]), { }) ------------------------------------------- Step 1, which took 0.010689 s (model generation: 0.009873, model checking: 0.000816): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6177 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 1 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 1 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 1 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 2, which took 0.008640 s (model generation: 0.008541, model checking: 0.000099): Model: |_ { append -> {{{ Q={q_gen_6178}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6178 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6177 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 1 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 1 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 4 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> z ; ll -> nil ; x -> b }) ------------------------------------------- Step 3, which took 0.009634 s (model generation: 0.009466, model checking: 0.000168): Model: |_ { append -> {{{ Q={q_gen_6178}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6178 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 1 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 4 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 4 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 4, which took 0.009643 s (model generation: 0.009238, model checking: 0.000405): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6183 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 2 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 4 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 4 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 5, which took 0.017556 s (model generation: 0.017223, model checking: 0.000333): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184}, Q_f={q_gen_6178}, Delta= { (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 3 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 4 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 7 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> z ; ll -> nil ; x -> a }) ------------------------------------------- Step 6, which took 0.015716 s (model generation: 0.013717, model checking: 0.001999): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184}, Q_f={q_gen_6178}, Delta= { (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 4 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 7 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 7 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 7, which took 0.013971 s (model generation: 0.013406, model checking: 0.000565): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6178) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6178 () -> q_gen_6178 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 7 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 7 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 7 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> nil ; _sx -> z ; _tx -> cons(b, nil) ; _ux -> s(z) ; l1 -> nil ; l2 -> nil }) ------------------------------------------- Step 8, which took 0.012672 s (model generation: 0.011731, model checking: 0.000941): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> length([nil, z]) -> 5 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 7 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 7 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 10 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(z) ; ll -> cons(b, nil) ; x -> b }) ------------------------------------------- Step 9, which took 0.012709 s (model generation: 0.011247, model checking: 0.001462): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6198, q_gen_6200}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6180) -> q_gen_6180 () -> q_gen_6180 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6200) -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> length([nil, z]) -> 6 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 7 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 10 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 10 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(b, nil)) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> cons(b, nil) }) ------------------------------------------- Step 10, which took 0.014308 s (model generation: 0.013158, model checking: 0.001150): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6178) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6198, q_gen_6200}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6180) -> q_gen_6180 () -> q_gen_6180 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6200) -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> length([nil, z]) -> 7 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 10 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 10 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 10 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, cons(b, nil)) ; _sx -> s(z) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 11, which took 0.015364 s (model generation: 0.014947, model checking: 0.000417): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6187, q_gen_6190, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6187, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6187 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6190 (q_gen_6195, q_gen_6190) -> q_gen_6190 (q_gen_6184, q_gen_6183) -> q_gen_6190 (q_gen_6194, q_gen_6193) -> q_gen_6190 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6198, q_gen_6200}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6180) -> q_gen_6180 () -> q_gen_6180 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6200) -> q_gen_6181 () -> q_gen_6181 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 8 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 10 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 10 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 10 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, nil) }) ------------------------------------------- Step 12, which took 0.014742 s (model generation: 0.013932, model checking: 0.000810): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6178) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 9 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 10 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 10 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 13 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(z) ; ll -> cons(a, nil) ; x -> b }) ------------------------------------------- Step 13, which took 0.017180 s (model generation: 0.015188, model checking: 0.001992): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6178) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 10 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 10 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 13 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 13 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, nil) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> nil }) ------------------------------------------- Step 14, which took 0.018728 s (model generation: 0.016353, model checking: 0.002375): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6178) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 10 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 13 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 13 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 13 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, cons(b, nil)) ; _sx -> s(s(z)) ; _tx -> cons(b, nil) ; _ux -> s(z) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 15, which took 0.019631 s (model generation: 0.018108, model checking: 0.001523): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> length([nil, z]) -> 11 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 13 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 13 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 16 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(b, cons(b, nil)) ; x -> b }) ------------------------------------------- Step 16, which took 0.021248 s (model generation: 0.019219, model checking: 0.002029): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6189, q_gen_6197, q_gen_6198, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6189, q_gen_6180) -> q_gen_6177 (q_gen_6189, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6189 (q_gen_6200) -> q_gen_6189 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 12 () -> length([nil, z]) -> 12 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 13 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 16 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 16 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(a, nil)) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> cons(b, nil) }) ------------------------------------------- Step 17, which took 0.027274 s (model generation: 0.024920, model checking: 0.002354): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6189, q_gen_6197, q_gen_6198, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6189, q_gen_6180) -> q_gen_6177 (q_gen_6189, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6189 (q_gen_6200) -> q_gen_6189 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 13 () -> length([nil, z]) -> 13 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 16 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 16 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 16 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, nil)) ; _sx -> s(z) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> cons(a, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 18, which took 0.027621 s (model generation: 0.026399, model checking: 0.001222): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 14 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 16 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 16 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 19 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(b, nil) ; x -> a }) ------------------------------------------- Step 19, which took 0.032101 s (model generation: 0.029444, model checking: 0.002657): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 15 () -> length([nil, z]) -> 15 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 16 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 19 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 19 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(b, nil)) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 20, which took 0.035282 s (model generation: 0.032293, model checking: 0.002989): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 16 () -> length([nil, z]) -> 16 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 19 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 19 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 19 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, cons(b, cons(b, nil))) ; _sx -> s(s(z)) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(s(z))) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 21, which took 0.043180 s (model generation: 0.040640, model checking: 0.002540): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> length([nil, z]) -> 17 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 19 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 19 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 22 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(s(z))) ; ll -> cons(b, cons(b, cons(b, nil))) ; x -> b }) ------------------------------------------- Step 22, which took 0.038615 s (model generation: 0.037257, model checking: 0.001358): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 18 () -> length([nil, z]) -> 18 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 19 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 22 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 22 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(a, nil)) ; h1 -> a ; l2 -> cons(b, cons(b, nil)) ; t1 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 23, which took 0.053903 s (model generation: 0.049008, model checking: 0.004895): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 () -> length([nil, z]) -> 19 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 22 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 22 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 22 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(z) ; _tx -> cons(b, cons(b, cons(b, cons(b, nil)))) ; _ux -> s(s(z)) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 24, which took 0.059722 s (model generation: 0.058543, model checking: 0.001179): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 20 () -> length([nil, z]) -> 20 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 22 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 22 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 25 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(b, nil) ; x -> b }) ------------------------------------------- Step 25, which took 0.058124 s (model generation: 0.055354, model checking: 0.002770): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 21 () -> length([nil, z]) -> 21 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 22 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 25 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 25 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(b, cons(b, nil))) ; h1 -> a ; l2 -> cons(b, cons(b, nil)) ; t1 -> cons(a, nil) }) ------------------------------------------- Step 26, which took 0.065545 s (model generation: 0.062914, model checking: 0.002631): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6194, q_gen_6232) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 22 () -> length([nil, z]) -> 22 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 25 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 25 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 25 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> nil ; _sx -> z ; _tx -> cons(a, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> nil ; l2 -> nil }) ------------------------------------------- Step 27, which took 0.071319 s (model generation: 0.069632, model checking: 0.001687): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6203) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6200) -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 23 () -> length([nil, z]) -> 23 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 25 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 25 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 28 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(a, nil) ; x -> b }) ------------------------------------------- Step 28, which took 0.090519 s (model generation: 0.083002, model checking: 0.007517): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 24 () -> length([nil, z]) -> 24 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 25 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 28 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 28 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(a, nil)) ; h1 -> a ; l2 -> cons(a, cons(a, nil)) ; t1 -> nil }) ------------------------------------------- Step 29, which took 0.095826 s (model generation: 0.092097, model checking: 0.003729): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6204, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6204, q_gen_6178) -> q_gen_6178 (q_gen_6204, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6194, q_gen_6232) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6204 () -> q_gen_6204 () -> q_gen_6204 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6200) -> q_gen_6181 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 () -> length([nil, z]) -> 25 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 28 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 28 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 28 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> nil ; _sx -> z ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> nil ; l2 -> nil }) ------------------------------------------- Step 30, which took 0.091879 s (model generation: 0.089314, model checking: 0.002565): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6204}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6204, q_gen_6178) -> q_gen_6178 (q_gen_6204, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6204 () -> q_gen_6204 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 26 () -> length([nil, z]) -> 26 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 28 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 31 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 29 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> cons(a, nil) }) ------------------------------------------- Step 31, which took 0.096709 s (model generation: 0.096205, model checking: 0.000504): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6222}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6186 (q_gen_6194, q_gen_6193) -> q_gen_6186 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6222, q_gen_6178) -> q_gen_6178 (q_gen_6222, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6186) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6222 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 () -> length([nil, z]) -> 27 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 28 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 31 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 29 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(b, cons(b, nil))) }) ------------------------------------------- Step 32, which took 0.117836 s (model generation: 0.110214, model checking: 0.007622): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6222}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6186 (q_gen_6184, q_gen_6186) -> q_gen_6186 (q_gen_6194, q_gen_6193) -> q_gen_6186 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6222, q_gen_6178) -> q_gen_6178 (q_gen_6222, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6186) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6222 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 () -> length([nil, z]) -> 28 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 31 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 31 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 29 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, cons(b, nil)))) ; _sx -> s(s(z)) ; _tx -> cons(a, cons(b, cons(b, nil))) ; _ux -> s(z) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 33, which took 0.118315 s (model generation: 0.117242, model checking: 0.001073): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6200) -> q_gen_6181 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 () -> length([nil, z]) -> 29 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 31 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 31 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 32 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(z) ; ll -> cons(b, nil) ; x -> a }) ------------------------------------------- Step 34, which took 0.121667 s (model generation: 0.119181, model checking: 0.002486): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6204}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6192) -> q_gen_6178 () -> q_gen_6178 (q_gen_6204, q_gen_6182) -> q_gen_6182 (q_gen_6204, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6182) -> q_gen_6192 (q_gen_6204, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6204 () -> q_gen_6204 () -> q_gen_6204 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 30 () -> length([nil, z]) -> 30 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 31 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 34 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 32 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(a, nil)) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> cons(a, cons(a, nil)) }) ------------------------------------------- Step 35, which took 0.159669 s (model generation: 0.150586, model checking: 0.009083): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6181, q_gen_6216) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 () -> length([nil, z]) -> 31 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 34 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 34 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 32 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(z) ; _tx -> cons(b, cons(b, cons(b, nil))) ; _ux -> s(s(s(z))) ; l1 -> cons(a, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 36, which took 0.186155 s (model generation: 0.172189, model checking: 0.013966): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 32 () -> length([nil, z]) -> 32 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 34 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 37 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 33 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(b, cons(b, nil))) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 37, which took 0.216413 s (model generation: 0.212900, model checking: 0.003513): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6231, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6231) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6194, q_gen_6232) -> q_gen_6231 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 33 () -> length([nil, z]) -> 33 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 37 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 37 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 34 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, nil) ; _sx -> s(s(z)) ; _tx -> cons(b, nil) ; _ux -> s(z) ; l1 -> cons(b, nil) ; l2 -> nil }) ------------------------------------------- Step 38, which took 0.204699 s (model generation: 0.187399, model checking: 0.017300): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 34 () -> length([nil, z]) -> 34 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 37 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 40 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 35 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(a, nil)) ; h1 -> a ; l2 -> cons(b, cons(a, nil)) ; t1 -> nil }) ------------------------------------------- Step 39, which took 0.217609 s (model generation: 0.214761, model checking: 0.002848): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 35 () -> length([nil, z]) -> 35 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 40 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 40 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 36 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, nil)) ; _sx -> s(s(z)) ; _tx -> cons(a, cons(b, nil)) ; _ux -> s(s(s(z))) ; l1 -> cons(a, nil) ; l2 -> cons(a, nil) }) ------------------------------------------- Step 40, which took 0.268168 s (model generation: 0.263275, model checking: 0.004893): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6204, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6204, q_gen_6178) -> q_gen_6182 (q_gen_6204, q_gen_6182) -> q_gen_6182 (q_gen_6204, q_gen_6214) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6204 () -> q_gen_6204 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6195, q_gen_6214) -> q_gen_6214 (q_gen_6204, q_gen_6192) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 36 () -> length([nil, z]) -> 36 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 40 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 43 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 37 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(a, nil)) ; h1 -> b ; l2 -> cons(b, cons(a, nil)) ; t1 -> cons(a, nil) }) ------------------------------------------- Step 41, which took 0.447134 s (model generation: 0.442511, model checking: 0.004623): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6204, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178, q_gen_6182}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6195, q_gen_6182) -> q_gen_6178 (q_gen_6204, q_gen_6178) -> q_gen_6178 (q_gen_6204, q_gen_6214) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6204, q_gen_6182) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6204, q_gen_6192) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6204 () -> q_gen_6204 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6197) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6200) -> q_gen_6200 () -> q_gen_6200 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 37 () -> length([nil, z]) -> 37 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 43 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 43 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 38 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, cons(b, nil)) ; _sx -> s(s(z)) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(s(z))) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 42, which took 0.242163 s (model generation: 0.239858, model checking: 0.002305): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6202, q_gen_6203, q_gen_6204}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6195, q_gen_6202) -> q_gen_6178 (q_gen_6204, q_gen_6202) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6204, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6204, q_gen_6192) -> q_gen_6202 (q_gen_6184, q_gen_6203) -> q_gen_6202 (q_gen_6184, q_gen_6203) -> q_gen_6202 () -> q_gen_6204 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 38 () -> length([nil, z]) -> 38 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 43 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 46 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 39 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil }) ------------------------------------------- Step 43, which took 0.240170 s (model generation: 0.236472, model checking: 0.003698): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 39 () -> length([nil, z]) -> 39 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 46 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 46 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 40 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, nil) ; _sx -> s(z) ; _tx -> cons(a, nil) ; _ux -> s(s(s(z))) ; l1 -> cons(a, nil) ; l2 -> nil }) ------------------------------------------- Step 44, which took 0.358811 s (model generation: 0.347464, model checking: 0.011347): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 40 () -> length([nil, z]) -> 40 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 46 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 49 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 41 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(b, nil)) ; h1 -> a ; l2 -> cons(a, cons(b, nil)) ; t1 -> nil }) ------------------------------------------- Step 45, which took 0.286101 s (model generation: 0.274493, model checking: 0.011608): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 41 () -> length([nil, z]) -> 41 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 49 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 49 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 42 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(a, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> cons(a, nil) ; l2 -> nil }) ------------------------------------------- Step 46, which took 0.417833 s (model generation: 0.415830, model checking: 0.002003): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6231, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6187, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6187 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6194, q_gen_6232) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6231) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6187, q_gen_6183) -> q_gen_6231 (q_gen_6194, q_gen_6232) -> q_gen_6231 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 42 () -> length([nil, z]) -> 42 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 49 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 52 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 43 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> nil ; h1 -> a ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 47, which took 0.377554 s (model generation: 0.377005, model checking: 0.000549): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6213}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6186) -> q_gen_6186 (q_gen_6187, q_gen_6183) -> q_gen_6186 (q_gen_6194, q_gen_6193) -> q_gen_6186 () -> q_gen_6187 (q_gen_6195, q_gen_6182) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6186) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6213, q_gen_6178) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6213, q_gen_6182) -> q_gen_6192 (q_gen_6213, q_gen_6192) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6187, q_gen_6186) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6187, q_gen_6183) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6213 () -> q_gen_6213 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 45 () -> length([nil, z]) -> 43 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 49 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 52 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 43 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 48, which took 0.390321 s (model generation: 0.388362, model checking: 0.001959): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6213}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6186) -> q_gen_6186 (q_gen_6187, q_gen_6183) -> q_gen_6186 (q_gen_6194, q_gen_6193) -> q_gen_6186 () -> q_gen_6187 (q_gen_6195, q_gen_6182) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6186) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6213, q_gen_6178) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6186) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6213, q_gen_6182) -> q_gen_6192 (q_gen_6213, q_gen_6192) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6187, q_gen_6186) -> q_gen_6192 (q_gen_6187, q_gen_6183) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6213 () -> q_gen_6213 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6197) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 48 () -> length([nil, z]) -> 44 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 49 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 52 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 44 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, nil) }) ------------------------------------------- Step 49, which took 0.388411 s (model generation: 0.375828, model checking: 0.012583): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 49 () -> length([nil, z]) -> 45 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 52 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 52 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 45 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, nil)) ; _sx -> s(s(z)) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(s(s(z)))) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 50, which took 0.410895 s (model generation: 0.409656, model checking: 0.001239): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6222}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6222, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6222, q_gen_6192) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6222 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6189, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6218}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6216) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6181, q_gen_6216) -> q_gen_6177 (q_gen_6189, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 () -> q_gen_6177 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 () -> q_gen_6189 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6189, q_gen_6197) -> q_gen_6205 (q_gen_6189, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 49 () -> length([nil, z]) -> 45 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 52 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 52 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 48 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(s(z))) ; ll -> cons(b, nil) ; x -> b }) ------------------------------------------- Step 51, which took 0.376532 s (model generation: 0.329851, model checking: 0.046681): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6203) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 50 () -> length([nil, z]) -> 46 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 55 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 53 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 49 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(b, cons(b, nil)) ; _ux -> s(s(z)) ; l1 -> nil ; l2 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 52, which took 0.418617 s (model generation: 0.415605, model checking: 0.003012): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6186 (q_gen_6184, q_gen_6186) -> q_gen_6186 (q_gen_6194, q_gen_6193) -> q_gen_6186 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6186) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6186) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 51 () -> length([nil, z]) -> 47 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 55 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 56 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 50 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, nil) ; h1 -> b ; l2 -> nil ; t1 -> cons(a, nil) }) ------------------------------------------- Step 53, which took 0.548238 s (model generation: 0.544523, model checking: 0.003715): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6222}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6222, q_gen_6182) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6222, q_gen_6192) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6222 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 51 () -> length([nil, z]) -> 48 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 55 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 56 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 53 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(b, cons(b, nil)) ; x -> a }) ------------------------------------------- Step 54, which took 0.432799 s (model generation: 0.419516, model checking: 0.013283): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 52 () -> length([nil, z]) -> 49 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 58 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 56 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 54 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(a, cons(b, cons(b, nil))) ; _ux -> s(s(s(s(z)))) ; l1 -> cons(a, nil) ; l2 -> cons(a, nil) }) ------------------------------------------- Step 55, which took 0.660939 s (model generation: 0.612430, model checking: 0.048509): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 53 () -> length([nil, z]) -> 50 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 61 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 57 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 55 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(b, cons(b, cons(b, cons(b, nil)))) ; _ux -> s(s(z)) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(b, cons(b, cons(b, nil))) }) ------------------------------------------- Step 56, which took 0.571825 s (model generation: 0.571327, model checking: 0.000498): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6187, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6187 () -> q_gen_6187 (q_gen_6184, q_gen_6183) -> q_gen_6203 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6203) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 56 () -> length([nil, z]) -> 51 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 61 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 57 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 55 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, cons(b, nil)) }) ------------------------------------------- Step 57, which took 0.678166 s (model generation: 0.672159, model checking: 0.006007): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6187, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6187 () -> q_gen_6187 () -> q_gen_6187 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6203) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6203) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 57 () -> length([nil, z]) -> 52 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 61 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 60 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 56 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(a, nil)) ; h1 -> a ; l2 -> cons(a, nil) ; t1 -> cons(a, nil) }) ------------------------------------------- Step 58, which took 0.771512 s (model generation: 0.762565, model checking: 0.008947): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6187, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6187 () -> q_gen_6187 () -> q_gen_6187 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6203) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6187, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 58 () -> length([nil, z]) -> 53 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 61 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 63 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 57 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(a, cons(b, nil))) ; h1 -> b ; l2 -> cons(a, cons(b, nil)) ; t1 -> cons(b, nil) }) ------------------------------------------- Step 59, which took 0.804126 s (model generation: 0.799686, model checking: 0.004440): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6191, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6191}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6191) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6191 (q_gen_6184, q_gen_6203) -> q_gen_6191 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 59 () -> length([nil, z]) -> 54 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 64 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 63 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 58 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(a, cons(b, cons(b, nil))) ; _ux -> s(s(s(s(s(z))))) ; l1 -> cons(a, nil) ; l2 -> cons(a, nil) }) ------------------------------------------- Step 60, which took 0.976871 s (model generation: 0.974120, model checking: 0.002751): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6239}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6216) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6239) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6239 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6239) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 59 () -> length([nil, z]) -> 55 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 64 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 63 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 61 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(s(s(z)))) ; ll -> cons(a, cons(b, nil)) ; x -> b }) ------------------------------------------- Step 61, which took 1.140374 s (model generation: 1.136751, model checking: 0.003623): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6232) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6181, q_gen_6216) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6199, q_gen_6216) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 60 () -> length([nil, z]) -> 56 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 64 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 63 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 64 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(z)) ; ll -> cons(b, cons(b, cons(b, nil))) ; x -> a }) ------------------------------------------- Step 62, which took 1.114984 s (model generation: 1.084712, model checking: 0.030272): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6239}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6239) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6239 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 (q_gen_6239) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 61 () -> length([nil, z]) -> 57 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 64 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 64 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 67 } Sat witness: Found: ((length([ll, _nx])) -> length([cons(x, ll), s(_nx)]), { _nx -> s(s(s(z))) ; ll -> cons(a, cons(a, cons(b, nil))) ; x -> a }) ------------------------------------------- Step 63, which took 0.927555 s (model generation: 0.891363, model checking: 0.036192): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6239}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6216) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6239 (q_gen_6239) -> q_gen_6239 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 62 () -> length([nil, z]) -> 58 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 67 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 65 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 67 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, cons(b, cons(b, nil))))) ; _sx -> s(s(z)) ; _tx -> cons(a, cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))) ; _ux -> s(s(s(z))) ; l1 -> cons(a, cons(b, cons(b, nil))) ; l2 -> cons(a, cons(b, cons(b, nil))) }) ------------------------------------------- Step 64, which took 1.889174 s (model generation: 1.883643, model checking: 0.005531): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6231, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6194, q_gen_6232) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6232) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6231) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6194, q_gen_6232) -> q_gen_6231 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6199, q_gen_6216) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 63 () -> length([nil, z]) -> 59 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 67 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 68 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 67 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(a, cons(b, cons(b, cons(b, nil)))) ; h1 -> b ; l2 -> cons(b, cons(a, nil)) ; t1 -> nil }) ------------------------------------------- Step 65, which took 6.420087 s (model generation: 6.411465, model checking: 0.008622): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6214, q_gen_6232}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6232) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6232) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6214) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6195, q_gen_6178) -> q_gen_6214 (q_gen_6194, q_gen_6232) -> q_gen_6214 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6199, q_gen_6216) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 64 () -> length([nil, z]) -> 60 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 70 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 68 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 68 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, nil)) ; _sx -> s(s(z)) ; _tx -> cons(b, cons(b, cons(b, cons(b, nil)))) ; _ux -> s(s(s(z))) ; l1 -> nil ; l2 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 66, which took 4.388456 s (model generation: 4.380547, model checking: 0.007909): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6231, q_gen_6232}, Q_f={q_gen_6178}, Delta= { () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6194, q_gen_6232) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6194, q_gen_6232) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6231) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6194, q_gen_6232) -> q_gen_6231 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6218, q_gen_6228}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6198, q_gen_6216) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6181, q_gen_6216) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6199, q_gen_6216) -> q_gen_6177 (q_gen_6228, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6228, q_gen_6180) -> q_gen_6205 (q_gen_6228, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6228 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 65 () -> length([nil, z]) -> 61 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 70 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 71 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 69 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(b, cons(b, cons(b, nil)))) ; h1 -> a ; l2 -> cons(a, cons(b, nil)) ; t1 -> cons(b, cons(b, nil)) }) ------------------------------------------- Step 67, which took 5.702187 s (model generation: 5.690309, model checking: 0.011878): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203, q_gen_6231, q_gen_6232}, Q_f={q_gen_6178}, Delta= { (q_gen_6194, q_gen_6232) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6183) -> q_gen_6183 (q_gen_6194, q_gen_6232) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6195, q_gen_6231) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6194, q_gen_6232) -> q_gen_6231 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 66 () -> length([nil, z]) -> 62 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 73 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 71 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 70 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(a, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(b, nil) ; _ux -> s(z) ; l1 -> nil ; l2 -> cons(a, nil) }) ------------------------------------------- Step 68, which took 3.776531 s (model generation: 3.769751, model checking: 0.006780): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6191, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6191}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6191) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6191 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6239}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6216) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6239) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6239 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 67 () -> length([nil, z]) -> 63 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 73 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 74 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 71 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(a, cons(a, nil))) ; h1 -> a ; l2 -> cons(a, cons(b, cons(b, nil))) ; t1 -> cons(b, cons(a, nil)) }) ------------------------------------------- Step 69, which took 9.414646 s (model generation: 9.407963, model checking: 0.006683): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6183, q_gen_6184, q_gen_6185, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6203}, Q_f={q_gen_6178, q_gen_6185}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6185) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6185 (q_gen_6184, q_gen_6183) -> q_gen_6185 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6184, q_gen_6203) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218, q_gen_6239}, Q_f={q_gen_6177}, Delta= { (q_gen_6198, q_gen_6216) -> q_gen_6180 () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6239) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6218) -> q_gen_6239 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6239) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 68 () -> length([nil, z]) -> 64 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 76 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 74 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 72 } Sat witness: Found: ((append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]), { _rx -> cons(b, cons(b, cons(b, nil))) ; _sx -> s(s(s(z))) ; _tx -> cons(b, cons(b, cons(b, cons(b, nil)))) ; _ux -> s(z) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) }) ------------------------------------------- Step 70, which took 7.075748 s (model generation: 7.058732, model checking: 0.017016): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6202, q_gen_6203, q_gen_6222}, Q_f={q_gen_6178, q_gen_6182}, Delta= { (q_gen_6194, q_gen_6193) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6194 (q_gen_6184, q_gen_6183) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 () -> q_gen_6184 (q_gen_6184, q_gen_6203) -> q_gen_6203 (q_gen_6194, q_gen_6193) -> q_gen_6203 (q_gen_6195, q_gen_6202) -> q_gen_6178 (q_gen_6222, q_gen_6178) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6182) -> q_gen_6182 (q_gen_6195, q_gen_6192) -> q_gen_6182 (q_gen_6222, q_gen_6182) -> q_gen_6182 (q_gen_6222, q_gen_6202) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6222, q_gen_6192) -> q_gen_6202 (q_gen_6184, q_gen_6203) -> q_gen_6202 (q_gen_6184, q_gen_6203) -> q_gen_6202 () -> q_gen_6222 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6217, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6217, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6181, q_gen_6216) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 (q_gen_6199, q_gen_6216) -> q_gen_6205 (q_gen_6217, q_gen_6180) -> q_gen_6205 (q_gen_6217, q_gen_6197) -> q_gen_6205 (q_gen_6218) -> q_gen_6217 (q_gen_6218) -> q_gen_6217 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 69 () -> length([nil, z]) -> 65 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 76 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 77 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 73 } Sat witness: Found: ((append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]), { _ix -> cons(b, cons(a, cons(a, cons(a, nil)))) ; h1 -> a ; l2 -> cons(a, cons(a, cons(b, nil))) ; t1 -> cons(b, cons(a, cons(a, nil))) }) ------------------------------------------- Step 71, which took 5.045407 s (model generation: 5.042494, model checking: 0.002913): Model: |_ { append -> {{{ Q={q_gen_6178, q_gen_6182, q_gen_6183, q_gen_6184, q_gen_6186, q_gen_6187, q_gen_6192, q_gen_6193, q_gen_6194, q_gen_6195, q_gen_6210, q_gen_6212, q_gen_6213, q_gen_6221, q_gen_6231, q_gen_6232, q_gen_6243, q_gen_6244, q_gen_6268, q_gen_6269, q_gen_6275, q_gen_6278, q_gen_6283}, Q_f={q_gen_6178, q_gen_6182, q_gen_6210, q_gen_6244, q_gen_6268, q_gen_6269, q_gen_6278}, Delta= { (q_gen_6194, q_gen_6232) -> q_gen_6193 () -> q_gen_6193 () -> q_gen_6194 () -> q_gen_6212 (q_gen_6194, q_gen_6193) -> q_gen_6232 (q_gen_6184, q_gen_6221) -> q_gen_6183 (q_gen_6275, q_gen_6221) -> q_gen_6183 (q_gen_6194, q_gen_6193) -> q_gen_6183 () -> q_gen_6183 () -> q_gen_6184 (q_gen_6184, q_gen_6183) -> q_gen_6186 (q_gen_6187, q_gen_6183) -> q_gen_6186 () -> q_gen_6187 (q_gen_6184, q_gen_6186) -> q_gen_6221 (q_gen_6194, q_gen_6232) -> q_gen_6221 (q_gen_6212, q_gen_6193) -> q_gen_6221 () -> q_gen_6275 () -> q_gen_6275 (q_gen_6195, q_gen_6182) -> q_gen_6178 (q_gen_6195, q_gen_6192) -> q_gen_6178 (q_gen_6195, q_gen_6231) -> q_gen_6178 (q_gen_6213, q_gen_6269) -> q_gen_6178 (q_gen_6184, q_gen_6183) -> q_gen_6178 (q_gen_6184, q_gen_6186) -> q_gen_6178 (q_gen_6187, q_gen_6183) -> q_gen_6178 () -> q_gen_6178 (q_gen_6195, q_gen_6243) -> q_gen_6182 (q_gen_6195, q_gen_6278) -> q_gen_6182 (q_gen_6184, q_gen_6183) -> q_gen_6182 (q_gen_6187, q_gen_6186) -> q_gen_6182 (q_gen_6184, q_gen_6221) -> q_gen_6182 (q_gen_6187, q_gen_6186) -> q_gen_6182 (q_gen_6195, q_gen_6178) -> q_gen_6192 (q_gen_6213, q_gen_6192) -> q_gen_6192 (q_gen_6194, q_gen_6193) -> q_gen_6192 () -> q_gen_6195 () -> q_gen_6195 (q_gen_6213, q_gen_6210) -> q_gen_6210 (q_gen_6213, q_gen_6243) -> q_gen_6210 (q_gen_6184, q_gen_6221) -> q_gen_6210 (q_gen_6212, q_gen_6193) -> q_gen_6210 () -> q_gen_6213 () -> q_gen_6213 (q_gen_6213, q_gen_6231) -> q_gen_6231 (q_gen_6275, q_gen_6221) -> q_gen_6231 (q_gen_6194, q_gen_6232) -> q_gen_6231 (q_gen_6195, q_gen_6244) -> q_gen_6243 (q_gen_6195, q_gen_6283) -> q_gen_6243 (q_gen_6213, q_gen_6178) -> q_gen_6243 (q_gen_6187, q_gen_6221) -> q_gen_6243 (q_gen_6212, q_gen_6232) -> q_gen_6243 (q_gen_6184, q_gen_6186) -> q_gen_6244 (q_gen_6187, q_gen_6183) -> q_gen_6244 (q_gen_6213, q_gen_6182) -> q_gen_6268 (q_gen_6213, q_gen_6244) -> q_gen_6269 (q_gen_6213, q_gen_6278) -> q_gen_6269 (q_gen_6195, q_gen_6210) -> q_gen_6278 (q_gen_6213, q_gen_6283) -> q_gen_6278 (q_gen_6187, q_gen_6221) -> q_gen_6283 (q_gen_6275, q_gen_6183) -> q_gen_6283 (q_gen_6275, q_gen_6183) -> q_gen_6283 (q_gen_6275, q_gen_6186) -> q_gen_6283 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_6177, q_gen_6180, q_gen_6181, q_gen_6197, q_gen_6198, q_gen_6199, q_gen_6200, q_gen_6205, q_gen_6216, q_gen_6218}, Q_f={q_gen_6177}, Delta= { () -> q_gen_6180 (q_gen_6198, q_gen_6180) -> q_gen_6197 (q_gen_6198, q_gen_6216) -> q_gen_6197 () -> q_gen_6198 () -> q_gen_6198 (q_gen_6218) -> q_gen_6200 () -> q_gen_6200 (q_gen_6198, q_gen_6197) -> q_gen_6216 (q_gen_6200) -> q_gen_6218 (q_gen_6181, q_gen_6180) -> q_gen_6177 (q_gen_6181, q_gen_6216) -> q_gen_6177 (q_gen_6199, q_gen_6197) -> q_gen_6177 (q_gen_6199, q_gen_6216) -> q_gen_6177 () -> q_gen_6177 () -> q_gen_6181 (q_gen_6218) -> q_gen_6181 () -> q_gen_6181 (q_gen_6200) -> q_gen_6199 (q_gen_6218) -> q_gen_6199 (q_gen_6200) -> q_gen_6199 (q_gen_6181, q_gen_6197) -> q_gen_6205 (q_gen_6199, q_gen_6180) -> q_gen_6205 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_elt, eq_eltlist, eq_nat} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 72 () -> length([nil, z]) -> 66 (append([l1, l2, _rx]) /\ append([l2, l1, _tx]) /\ length([_rx, _sx]) /\ length([_tx, _ux])) -> eq_nat([_sx, _ux]) -> 76 (append([t1, l2, _ix])) -> append([cons(h1, t1), l2, cons(h1, _ix)]) -> 77 (length([ll, _nx])) -> length([cons(x, ll), s(_nx)]) -> 73 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(a, cons(b, cons(a, nil))) }) Total time: 73.946814 Reason for stopping: DontKnow. Stopped because: timeout