Solving ../../benchmarks/true/isaplanner_prop46.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  list -> {cons, nil}  ;  list2 -> {cons2, nil2}  ;  pair -> {pair2}
}
definition:
{
(zip, F:
{() -> zip([cons2(z, x2), nil2, nil])
() -> zip([nil2, y, nil])
(zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)])}
(zip([_hv, _iv, _jv]) /\ zip([_hv, _iv, _kv])) -> eq_list([_jv, _kv])
)
(zip_concat, F:
{() -> zip_concat([x, y, nil2, nil])
(zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)])}
(zip_concat([_mv, _nv, _ov, _pv]) /\ zip_concat([_mv, _nv, _ov, _qv])) -> eq_list([_pv, _qv])
)
}

properties:
{(zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)])}


over-approximation: {zip, zip_concat}
under-approximation: {zip_concat}

Clause system for inference is:

{
() -> zip([cons2(z, x2), nil2, nil]) -> 0  ;  () -> zip([nil2, y, nil]) -> 0  ;  () -> zip_concat([x, y, nil2, nil]) -> 0  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 0  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 0  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 0
}


Solving took 30.003420 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2333, q_gen_2334, q_gen_2335, q_gen_2342, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2352, q_gen_2353, q_gen_2354, q_gen_2355, q_gen_2357, q_gen_2358, q_gen_2359, q_gen_2365, q_gen_2366, q_gen_2367, q_gen_2368, q_gen_2369, q_gen_2370, q_gen_2371, q_gen_2374, q_gen_2375, q_gen_2379, q_gen_2380, q_gen_2381, q_gen_2382, q_gen_2383, q_gen_2384, q_gen_2386, q_gen_2387, q_gen_2393, q_gen_2394, q_gen_2395, q_gen_2396, q_gen_2397, q_gen_2398, q_gen_2406, q_gen_2407, q_gen_2408, q_gen_2409, q_gen_2410, q_gen_2411, q_gen_2412, q_gen_2417, q_gen_2418, q_gen_2419, q_gen_2420, q_gen_2421, q_gen_2425, q_gen_2426, q_gen_2427, q_gen_2428, q_gen_2429, q_gen_2430, q_gen_2431, q_gen_2436, q_gen_2437, q_gen_2438, q_gen_2439, q_gen_2440, q_gen_2441, q_gen_2442},
Q_f={},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2359
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2387
<nil2, b>() -> q_gen_2408
<b, b>() -> q_gen_2409
<nil2, a>() -> q_gen_2419
<b, a>() -> q_gen_2420
<cons2, a>(q_gen_2335, q_gen_2334) -> q_gen_2428
<cons2, b>(q_gen_2335, q_gen_2334) -> q_gen_2429
<cons2, a>(q_gen_2344, q_gen_2334) -> q_gen_2439
<cons2, b>(q_gen_2344, q_gen_2334) -> q_gen_2440
<nil2, nil2, nil>() -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2333
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2342
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2354, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2352, q_gen_2332) -> q_gen_2351
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2352
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2354
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2357
<cons2, nil2, nil>(q_gen_2335, q_gen_2359) -> q_gen_2358
<cons2, cons2, cons>(q_gen_2371, q_gen_2370, q_gen_2369, q_gen_2368, q_gen_2367, q_gen_2345, q_gen_2366, q_gen_2332) -> q_gen_2365
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2366
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2367
<b, nil2, nil>() -> q_gen_2368
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2369
<b, a, nil>() -> q_gen_2370
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2371
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2374
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2375
<cons2, cons2, cons>(q_gen_2384, q_gen_2383, q_gen_2382, q_gen_2368, q_gen_2381, q_gen_2380, q_gen_2352, q_gen_2332) -> q_gen_2379
<nil2, b, nil>() -> q_gen_2380
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2381
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2382
<b, b, nil>() -> q_gen_2383
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2384
<nil2, cons2, nil>(q_gen_2344, q_gen_2387) -> q_gen_2386
<cons2, cons2, cons>(q_gen_2398, q_gen_2397, q_gen_2396, q_gen_2347, q_gen_2395, q_gen_2380, q_gen_2394, q_gen_2332) -> q_gen_2393
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2394
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2395
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2396
<a, b, nil>() -> q_gen_2397
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2398
<cons2, cons2, cons>(q_gen_2384, q_gen_2383, q_gen_2411, q_gen_2410, q_gen_2381, q_gen_2380, q_gen_2407, q_gen_2357) -> q_gen_2406
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2407
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2410
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2411
<nil2, cons2, nil>(q_gen_2344, q_gen_2359) -> q_gen_2412
<cons2, cons2, cons>(q_gen_2371, q_gen_2370, q_gen_2421, q_gen_2410, q_gen_2367, q_gen_2345, q_gen_2418, q_gen_2357) -> q_gen_2417
<nil2, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2408, q_gen_2419) -> q_gen_2418
<b, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2408, q_gen_2419) -> q_gen_2421
<nil2, cons2, nil>(q_gen_2335, q_gen_2359) -> q_gen_2425
<cons2, cons2, cons>(q_gen_2371, q_gen_2370, q_gen_2431, q_gen_2430, q_gen_2367, q_gen_2345, q_gen_2427, q_gen_2425) -> q_gen_2426
<nil2, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2429, q_gen_2428) -> q_gen_2427
<b, cons2, nil>(q_gen_2335, q_gen_2359) -> q_gen_2430
<b, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2429, q_gen_2428) -> q_gen_2431
<nil2, cons2, nil>(q_gen_2335, q_gen_2387) -> q_gen_2436
<cons2, cons2, cons>(q_gen_2371, q_gen_2370, q_gen_2442, q_gen_2441, q_gen_2367, q_gen_2345, q_gen_2438, q_gen_2436) -> q_gen_2437
<nil2, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2440, q_gen_2439) -> q_gen_2438
<b, cons2, nil>(q_gen_2335, q_gen_2387) -> q_gen_2441
<b, cons2, pair2>(q_gen_2409, q_gen_2420, q_gen_2440, q_gen_2439) -> q_gen_2442
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2336, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2356, q_gen_2360, q_gen_2361, q_gen_2362, q_gen_2363, q_gen_2364, q_gen_2372, q_gen_2373, q_gen_2376, q_gen_2377, q_gen_2378, q_gen_2385, q_gen_2388, q_gen_2389, q_gen_2390, q_gen_2391, q_gen_2392, q_gen_2399, q_gen_2400, q_gen_2401, q_gen_2402, q_gen_2403, q_gen_2404, q_gen_2405, q_gen_2413, q_gen_2414, q_gen_2415, q_gen_2416, q_gen_2422, q_gen_2423, q_gen_2424, q_gen_2432, q_gen_2433, q_gen_2434, q_gen_2435, q_gen_2443, q_gen_2444, q_gen_2445},
Q_f={},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2362
<nil2>() -> q_gen_2373
<cons2>(q_gen_2362, q_gen_2373) -> q_gen_2400
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, pair2>(q_gen_2339, q_gen_2362) -> q_gen_2361
<b, nil>() -> q_gen_2363
<b, pair2>(q_gen_2339, q_gen_2362) -> q_gen_2364
<nil2, pair2>(q_gen_2362, q_gen_2362) -> q_gen_2377
<b, pair2>(q_gen_2362, q_gen_2362) -> q_gen_2378
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2389
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2390
<nil2, b>() -> q_gen_2391
<a, b>() -> q_gen_2392
<cons2, pair2>(q_gen_2392, q_gen_2404, q_gen_2391, q_gen_2403) -> q_gen_2402
<nil2, a>() -> q_gen_2403
<a, a>() -> q_gen_2404
<a, pair2>(q_gen_2362, q_gen_2339) -> q_gen_2405
<cons2, nil>(q_gen_2339, q_gen_2400) -> q_gen_2414
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2416, q_gen_2416) -> q_gen_2415
<cons2, b>(q_gen_2362, q_gen_2373) -> q_gen_2416
<cons2, pair2>(q_gen_2392, q_gen_2404, q_gen_2416, q_gen_2424) -> q_gen_2423
<cons2, a>(q_gen_2362, q_gen_2373) -> q_gen_2424
<cons2, nil>(q_gen_2362, q_gen_2373) -> q_gen_2433
<cons2, pair2>(q_gen_2435, q_gen_2435, q_gen_2391, q_gen_2391) -> q_gen_2434
<b, b>() -> q_gen_2435
<cons2, pair2>(q_gen_2435, q_gen_2445, q_gen_2391, q_gen_2403) -> q_gen_2444
<b, a>() -> q_gen_2445
<b, nil2, nil2, nil>() -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2336
<a, nil2, nil2, nil>() -> q_gen_2356
<a, nil2, cons2, cons>(q_gen_2364, q_gen_2363, q_gen_2361, q_gen_2337) -> q_gen_2360
<b, cons2, nil2, nil>(q_gen_2362, q_gen_2373) -> q_gen_2372
<b, nil2, cons2, cons>(q_gen_2378, q_gen_2363, q_gen_2377, q_gen_2337) -> q_gen_2376
<a, cons2, nil2, nil>(q_gen_2362, q_gen_2373) -> q_gen_2385
<b, nil2, cons2, cons>(q_gen_2378, q_gen_2363, q_gen_2390, q_gen_2389) -> q_gen_2388
<b, cons2, nil2, nil>(q_gen_2362, q_gen_2400) -> q_gen_2399
<b, nil2, cons2, cons>(q_gen_2405, q_gen_2340, q_gen_2402, q_gen_2389) -> q_gen_2401
<b, nil2, cons2, cons>(q_gen_2378, q_gen_2363, q_gen_2415, q_gen_2414) -> q_gen_2413
<b, nil2, cons2, cons>(q_gen_2405, q_gen_2340, q_gen_2423, q_gen_2414) -> q_gen_2422
<b, nil2, cons2, cons>(q_gen_2378, q_gen_2363, q_gen_2434, q_gen_2433) -> q_gen_2432
<b, nil2, cons2, cons>(q_gen_2405, q_gen_2340, q_gen_2444, q_gen_2433) -> q_gen_2443
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006008 s (model generation: 0.004020,  model checking: 0.001988):

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

}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 0  ;  () -> zip([nil2, y, nil]) -> 0  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 1  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 1  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 1
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> nil2
})

-------------------------------------------
Step 1, which took 0.004229 s (model generation: 0.003565,  model checking: 0.000664):

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

}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331},
Q_f={q_gen_2331},
Delta=
{
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 0  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 1  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 1  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 1
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> nil2
})

-------------------------------------------
Step 2, which took 0.004230 s (model generation: 0.003500,  model checking: 0.000730):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332},
Q_f={q_gen_2332},
Delta=
{
<nil2, nil2, nil>() -> q_gen_2332
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331},
Q_f={q_gen_2331},
Delta=
{
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 1  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 1  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 1
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> nil2  ;  z -> b
})

-------------------------------------------
Step 3, which took 0.004329 s (model generation: 0.003444,  model checking: 0.000885):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331},
Q_f={q_gen_2331},
Delta=
{
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 1  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 1  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> a  ;  y -> nil2  ;  y2 -> a  ;  ys -> nil2
})

-------------------------------------------
Step 4, which took 0.009260 s (model generation: 0.003582,  model checking: 0.005678):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 2  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> a
})

-------------------------------------------
Step 5, which took 0.004776 s (model generation: 0.004251,  model checking: 0.000525):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<a>() -> q_gen_2335
<b>() -> q_gen_2335
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 3  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: ((zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]), {
_rv -> cons(pair2(b, b), nil)  ;  _sv -> nil  ;  x -> a  ;  xs -> nil2  ;  y -> a  ;  ys -> nil2
})

-------------------------------------------
Step 6, which took 0.005949 s (model generation: 0.004409,  model checking: 0.001540):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2352},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2352, q_gen_2332) -> q_gen_2351
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2352
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 3  ;  () -> zip_concat([x, y, nil2, nil]) -> 6  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> nil2
})

-------------------------------------------
Step 7, which took 0.012899 s (model generation: 0.005572,  model checking: 0.007327):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2352},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2352, q_gen_2332) -> q_gen_2351
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2352
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 3  ;  () -> zip([nil2, y, nil]) -> 6  ;  () -> zip_concat([x, y, nil2, nil]) -> 6  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(b, nil2)
})

-------------------------------------------
Step 8, which took 0.010041 s (model generation: 0.004624,  model checking: 0.005417):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 6  ;  () -> zip([nil2, y, nil]) -> 6  ;  () -> zip_concat([x, y, nil2, nil]) -> 6  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 4
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 9, which took 0.007384 s (model generation: 0.004554,  model checking: 0.002830):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 6  ;  () -> zip([nil2, y, nil]) -> 6  ;  () -> zip_concat([x, y, nil2, nil]) -> 6  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 4  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 7
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> a  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 10, which took 0.331223 s (model generation: 0.005001,  model checking: 0.326222):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 6  ;  () -> zip([nil2, y, nil]) -> 6  ;  () -> zip_concat([x, y, nil2, nil]) -> 6  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 7  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 5  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 7
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 11, which took 0.011045 s (model generation: 0.006588,  model checking: 0.004457):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 6  ;  () -> zip([nil2, y, nil]) -> 6  ;  () -> zip_concat([x, y, nil2, nil]) -> 9  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 7  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 6  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 7
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 12, which took 0.035799 s (model generation: 0.005996,  model checking: 0.029803):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 6  ;  () -> zip([nil2, y, nil]) -> 9  ;  () -> zip_concat([x, y, nil2, nil]) -> 9  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 7  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 7  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 7
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(a, nil2)
})

-------------------------------------------
Step 13, which took 0.011698 s (model generation: 0.006588,  model checking: 0.005110):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2352},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2352, q_gen_2332) -> q_gen_2351
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2352
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 9  ;  () -> zip([nil2, y, nil]) -> 9  ;  () -> zip_concat([x, y, nil2, nil]) -> 9  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 7  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 7  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 7
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> nil2  ;  z -> a
})

-------------------------------------------
Step 14, which took 0.008799 s (model generation: 0.006509,  model checking: 0.002290):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2354},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2354, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2354
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 9  ;  () -> zip([nil2, y, nil]) -> 9  ;  () -> zip_concat([x, y, nil2, nil]) -> 9  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 7  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 7  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 10
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 15, which took 0.961269 s (model generation: 0.006262,  model checking: 0.955007):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2352},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2352, q_gen_2332) -> q_gen_2351
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2352
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 9  ;  () -> zip([nil2, y, nil]) -> 9  ;  () -> zip_concat([x, y, nil2, nil]) -> 9  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 10  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 8  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 10
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 16, which took 0.013574 s (model generation: 0.007986,  model checking: 0.005588):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 9  ;  () -> zip([nil2, y, nil]) -> 9  ;  () -> zip_concat([x, y, nil2, nil]) -> 12  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 10  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 9  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 10
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 17, which took 0.016504 s (model generation: 0.007217,  model checking: 0.009287):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 9  ;  () -> zip([nil2, y, nil]) -> 12  ;  () -> zip_concat([x, y, nil2, nil]) -> 12  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 10  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 10  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 10
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(a, cons2(a, nil2))
})

-------------------------------------------
Step 18, which took 0.015986 s (model generation: 0.007603,  model checking: 0.008383):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<nil2, nil>() -> q_gen_2337
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 10  ;  () -> zip([nil2, y, nil]) -> 12  ;  () -> zip_concat([x, y, nil2, nil]) -> 12  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 10  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 10  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 13
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(a, nil2)
})

-------------------------------------------
Step 19, which took 0.982459 s (model generation: 0.007462,  model checking: 0.974997):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, b>() -> q_gen_2391
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 10  ;  () -> zip([nil2, y, nil]) -> 12  ;  () -> zip_concat([x, y, nil2, nil]) -> 12  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 13  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 11  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 13
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> a
})

-------------------------------------------
Step 20, which took 0.024099 s (model generation: 0.009363,  model checking: 0.014736):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, b>() -> q_gen_2391
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 11  ;  () -> zip([nil2, y, nil]) -> 12  ;  () -> zip_concat([x, y, nil2, nil]) -> 15  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 13  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 12  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 13
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> cons2(b, cons2(b, nil2))
})

-------------------------------------------
Step 21, which took 0.029708 s (model generation: 0.008974,  model checking: 0.020734):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, b>() -> q_gen_2391
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 12  ;  () -> zip([nil2, y, nil]) -> 13  ;  () -> zip_concat([x, y, nil2, nil]) -> 15  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 13  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 13  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 16
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(a, nil2)
})

-------------------------------------------
Step 22, which took 5.862122 s (model generation: 0.009615,  model checking: 5.852507):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 13  ;  () -> zip([nil2, y, nil]) -> 13  ;  () -> zip_concat([x, y, nil2, nil]) -> 15  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 16  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 14  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 16
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 23, which took 0.047134 s (model generation: 0.010997,  model checking: 0.036137):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2354, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<nil2, b>() -> q_gen_2408
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2354, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2354
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 14  ;  () -> zip([nil2, y, nil]) -> 14  ;  () -> zip_concat([x, y, nil2, nil]) -> 16  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 16  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 15  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 19
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(a, cons2(b, nil2))
})

-------------------------------------------
Step 24, which took 4.567602 s (model generation: 0.011870,  model checking: 4.555732):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<nil2, b>() -> q_gen_2408
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 15  ;  () -> zip([nil2, y, nil]) -> 15  ;  () -> zip_concat([x, y, nil2, nil]) -> 16  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 19  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 16  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 19
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 25, which took 0.050806 s (model generation: 0.013741,  model checking: 0.037065):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<nil2, a>() -> q_gen_2408
<nil2, b>() -> q_gen_2408
<b, a>() -> q_gen_2409
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 16  ;  () -> zip([nil2, y, nil]) -> 16  ;  () -> zip_concat([x, y, nil2, nil]) -> 17  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 19  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 17  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 22
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(a, cons2(b, nil2))
})

-------------------------------------------
Step 26, which took 4.598721 s (model generation: 0.014140,  model checking: 4.584581):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<nil2, a>() -> q_gen_2408
<nil2, b>() -> q_gen_2408
<b, a>() -> q_gen_2409
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, a>(q_gen_2339, q_gen_2373) -> q_gen_2391
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 17  ;  () -> zip([nil2, y, nil]) -> 17  ;  () -> zip_concat([x, y, nil2, nil]) -> 18  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 22  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 18  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 22
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, cons2(b, nil2))  ;  z -> b
})

-------------------------------------------
Step 27, which took 0.051510 s (model generation: 0.016253,  model checking: 0.035257):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, a>(q_gen_2335, q_gen_2334) -> q_gen_2408
<cons2, b>(q_gen_2335, q_gen_2334) -> q_gen_2408
<nil2, a>() -> q_gen_2408
<nil2, b>() -> q_gen_2408
<b, a>() -> q_gen_2409
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, a>(q_gen_2339, q_gen_2373) -> q_gen_2391
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 18  ;  () -> zip([nil2, y, nil]) -> 18  ;  () -> zip_concat([x, y, nil2, nil]) -> 19  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 22  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 19  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 25
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(b, nil2)
})

-------------------------------------------
Step 28, which took 4.616613 s (model generation: 0.017517,  model checking: 4.599096):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2353, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, a>(q_gen_2335, q_gen_2334) -> q_gen_2408
<cons2, b>(q_gen_2335, q_gen_2334) -> q_gen_2408
<nil2, a>() -> q_gen_2408
<nil2, b>() -> q_gen_2408
<b, a>() -> q_gen_2409
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2353, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2353
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, a>(q_gen_2339, q_gen_2373) -> q_gen_2391
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<b, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 19  ;  () -> zip([nil2, y, nil]) -> 19  ;  () -> zip_concat([x, y, nil2, nil]) -> 20  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 25  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 20  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 25
}
Sat witness: Yes: ((zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]), {
_gv -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, cons2(a, nil2))  ;  z -> b
})

-------------------------------------------
Step 29, which took 0.052933 s (model generation: 0.019791,  model checking: 0.033142):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2332, q_gen_2334, q_gen_2335, q_gen_2343, q_gen_2344, q_gen_2345, q_gen_2346, q_gen_2347, q_gen_2348, q_gen_2349, q_gen_2350, q_gen_2351, q_gen_2355, q_gen_2408, q_gen_2409},
Q_f={q_gen_2332},
Delta=
{
<cons2>(q_gen_2335, q_gen_2334) -> q_gen_2334
<cons2>(q_gen_2344, q_gen_2334) -> q_gen_2334
<nil2>() -> q_gen_2334
<b>() -> q_gen_2335
<a>() -> q_gen_2344
<cons2, a>(q_gen_2335, q_gen_2334) -> q_gen_2408
<cons2, a>(q_gen_2344, q_gen_2334) -> q_gen_2408
<cons2, b>(q_gen_2335, q_gen_2334) -> q_gen_2408
<cons2, b>(q_gen_2344, q_gen_2334) -> q_gen_2408
<nil2, a>() -> q_gen_2408
<nil2, b>() -> q_gen_2408
<b, a>() -> q_gen_2409
<b, b>() -> q_gen_2409
<cons2, cons2, cons>(q_gen_2350, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<cons2, nil2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2332
<nil2, cons2, nil>(q_gen_2344, q_gen_2334) -> q_gen_2332
<nil2, nil2, nil>() -> q_gen_2332
<nil2, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2343
<nil2, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2343
<nil2, a, nil>() -> q_gen_2345
<nil2, b, nil>() -> q_gen_2345
<nil2, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2346
<nil2, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2346
<nil2, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2346
<nil2, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2346
<a, nil2, nil>() -> q_gen_2347
<b, cons2, nil>(q_gen_2335, q_gen_2334) -> q_gen_2347
<b, nil2, nil>() -> q_gen_2347
<a, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2348
<a, nil2, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2348
<b, cons2, pair2>(q_gen_2409, q_gen_2409, q_gen_2408, q_gen_2408) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2348
<b, nil2, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2348
<a, a, nil>() -> q_gen_2349
<a, b, nil>() -> q_gen_2349
<b, a, nil>() -> q_gen_2349
<b, b, nil>() -> q_gen_2349
<a, a, pair2>(q_gen_2344, q_gen_2344) -> q_gen_2350
<a, b, pair2>(q_gen_2344, q_gen_2335) -> q_gen_2350
<b, a, pair2>(q_gen_2335, q_gen_2344) -> q_gen_2350
<b, b, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2350
<cons2, cons2, cons>(q_gen_2355, q_gen_2349, q_gen_2348, q_gen_2347, q_gen_2346, q_gen_2345, q_gen_2343, q_gen_2332) -> q_gen_2351
<a, a, pair2>(q_gen_2335, q_gen_2335) -> q_gen_2355
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2331, q_gen_2337, q_gen_2338, q_gen_2339, q_gen_2340, q_gen_2341, q_gen_2373, q_gen_2391, q_gen_2392},
Q_f={q_gen_2331},
Delta=
{
<a>() -> q_gen_2339
<b>() -> q_gen_2339
<cons2>(q_gen_2339, q_gen_2373) -> q_gen_2373
<nil2>() -> q_gen_2373
<cons2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2337
<nil2, nil>() -> q_gen_2337
<cons2, pair2>(q_gen_2392, q_gen_2392, q_gen_2391, q_gen_2391) -> q_gen_2338
<nil2, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2338
<a, nil>() -> q_gen_2340
<b, nil>() -> q_gen_2340
<a, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<b, pair2>(q_gen_2339, q_gen_2339) -> q_gen_2341
<cons2, a>(q_gen_2339, q_gen_2373) -> q_gen_2391
<cons2, b>(q_gen_2339, q_gen_2373) -> q_gen_2391
<nil2, a>() -> q_gen_2391
<nil2, b>() -> q_gen_2391
<a, a>() -> q_gen_2392
<a, b>() -> q_gen_2392
<b, b>() -> q_gen_2392
<a, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<a, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<a, nil2, nil2, nil>() -> q_gen_2331
<b, cons2, nil2, nil>(q_gen_2339, q_gen_2373) -> q_gen_2331
<b, nil2, cons2, cons>(q_gen_2341, q_gen_2340, q_gen_2338, q_gen_2337) -> q_gen_2331
<b, nil2, nil2, nil>() -> q_gen_2331
}

Datatype: <elt, list2, list2, list>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_list, eq_list2, eq_pair}
_|

Teacher's answer:
New clause system:
{
() -> zip([cons2(z, x2), nil2, nil]) -> 20  ;  () -> zip([nil2, y, nil]) -> 20  ;  () -> zip_concat([x, y, nil2, nil]) -> 21  ;  (zip([x2, x4, _gv])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _gv)]) -> 25  ;  (zip([xs, ys, _sv]) /\ zip([cons2(x, xs), cons2(y, ys), _rv])) -> eq_list([_rv, cons(pair2(x, y), _sv)]) -> 21  ;  (zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]) -> 28
}
Sat witness: Yes: ((zip([y, ys, _lv])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _lv)]), {
_lv -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(b, nil2)
})

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