Solving ../../benchmarks/true/isaplanner_prop45.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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)])}
(zip([_qca, _rca, _sca]) /\ zip([_qca, _rca, _tca])) -> eq_list([_sca, _tca])
)
(zip_concat, F:
{() -> zip_concat([x, y, nil2, nil])
(zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)])}
(zip_concat([_vca, _wca, _xca, _yca]) /\ zip_concat([_vca, _wca, _xca, _zca])) -> eq_list([_yca, _zca])
)
}

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


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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 0  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 0  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 0
}


Solving took 30.005770 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2218, q_gen_2219, q_gen_2220, q_gen_2227, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237, q_gen_2238, q_gen_2239, q_gen_2240, q_gen_2242, q_gen_2243, q_gen_2244, q_gen_2250, q_gen_2251, q_gen_2252, q_gen_2253, q_gen_2254, q_gen_2255, q_gen_2256, q_gen_2259, q_gen_2260, q_gen_2264, q_gen_2265, q_gen_2266, q_gen_2267, q_gen_2268, q_gen_2269, q_gen_2271, q_gen_2272, q_gen_2278, q_gen_2279, q_gen_2280, q_gen_2281, q_gen_2282, q_gen_2283, q_gen_2291, q_gen_2292, q_gen_2293, q_gen_2294, q_gen_2295, q_gen_2296, q_gen_2297, q_gen_2302, q_gen_2303, q_gen_2304, q_gen_2305, q_gen_2306, q_gen_2310, q_gen_2311, q_gen_2312, q_gen_2313, q_gen_2314, q_gen_2315, q_gen_2316, q_gen_2321, q_gen_2322, q_gen_2323, q_gen_2324, q_gen_2325, q_gen_2326, q_gen_2327},
Q_f={},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2244
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2272
<nil2, b>() -> q_gen_2293
<b, b>() -> q_gen_2294
<nil2, a>() -> q_gen_2304
<b, a>() -> q_gen_2305
<cons2, a>(q_gen_2220, q_gen_2219) -> q_gen_2313
<cons2, b>(q_gen_2220, q_gen_2219) -> q_gen_2314
<cons2, a>(q_gen_2229, q_gen_2219) -> q_gen_2324
<cons2, b>(q_gen_2229, q_gen_2219) -> q_gen_2325
<nil2, nil2, nil>() -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2218
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2227
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2239, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2237, q_gen_2217) -> q_gen_2236
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2237
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2239
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2242
<cons2, nil2, nil>(q_gen_2220, q_gen_2244) -> q_gen_2243
<cons2, cons2, cons>(q_gen_2256, q_gen_2255, q_gen_2254, q_gen_2253, q_gen_2252, q_gen_2230, q_gen_2251, q_gen_2217) -> q_gen_2250
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2251
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2252
<b, nil2, nil>() -> q_gen_2253
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2254
<b, a, nil>() -> q_gen_2255
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2256
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2259
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2260
<cons2, cons2, cons>(q_gen_2269, q_gen_2268, q_gen_2267, q_gen_2253, q_gen_2266, q_gen_2265, q_gen_2237, q_gen_2217) -> q_gen_2264
<nil2, b, nil>() -> q_gen_2265
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2266
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2267
<b, b, nil>() -> q_gen_2268
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2269
<nil2, cons2, nil>(q_gen_2229, q_gen_2272) -> q_gen_2271
<cons2, cons2, cons>(q_gen_2283, q_gen_2282, q_gen_2281, q_gen_2232, q_gen_2280, q_gen_2265, q_gen_2279, q_gen_2217) -> q_gen_2278
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2279
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2280
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2281
<a, b, nil>() -> q_gen_2282
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2283
<cons2, cons2, cons>(q_gen_2269, q_gen_2268, q_gen_2296, q_gen_2295, q_gen_2266, q_gen_2265, q_gen_2292, q_gen_2242) -> q_gen_2291
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2292
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2295
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2296
<nil2, cons2, nil>(q_gen_2229, q_gen_2244) -> q_gen_2297
<cons2, cons2, cons>(q_gen_2256, q_gen_2255, q_gen_2306, q_gen_2295, q_gen_2252, q_gen_2230, q_gen_2303, q_gen_2242) -> q_gen_2302
<nil2, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2293, q_gen_2304) -> q_gen_2303
<b, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2293, q_gen_2304) -> q_gen_2306
<nil2, cons2, nil>(q_gen_2220, q_gen_2244) -> q_gen_2310
<cons2, cons2, cons>(q_gen_2256, q_gen_2255, q_gen_2316, q_gen_2315, q_gen_2252, q_gen_2230, q_gen_2312, q_gen_2310) -> q_gen_2311
<nil2, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2314, q_gen_2313) -> q_gen_2312
<b, cons2, nil>(q_gen_2220, q_gen_2244) -> q_gen_2315
<b, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2314, q_gen_2313) -> q_gen_2316
<nil2, cons2, nil>(q_gen_2220, q_gen_2272) -> q_gen_2321
<cons2, cons2, cons>(q_gen_2256, q_gen_2255, q_gen_2327, q_gen_2326, q_gen_2252, q_gen_2230, q_gen_2323, q_gen_2321) -> q_gen_2322
<nil2, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2325, q_gen_2324) -> q_gen_2323
<b, cons2, nil>(q_gen_2220, q_gen_2272) -> q_gen_2326
<b, cons2, pair2>(q_gen_2294, q_gen_2305, q_gen_2325, q_gen_2324) -> q_gen_2327
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2221, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2241, q_gen_2245, q_gen_2246, q_gen_2247, q_gen_2248, q_gen_2249, q_gen_2257, q_gen_2258, q_gen_2261, q_gen_2262, q_gen_2263, q_gen_2270, q_gen_2273, q_gen_2274, q_gen_2275, q_gen_2276, q_gen_2277, q_gen_2284, q_gen_2285, q_gen_2286, q_gen_2287, q_gen_2288, q_gen_2289, q_gen_2290, q_gen_2298, q_gen_2299, q_gen_2300, q_gen_2301, q_gen_2307, q_gen_2308, q_gen_2309, q_gen_2317, q_gen_2318, q_gen_2319, q_gen_2320, q_gen_2328, q_gen_2329, q_gen_2330},
Q_f={},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2247
<nil2>() -> q_gen_2258
<cons2>(q_gen_2247, q_gen_2258) -> q_gen_2285
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, pair2>(q_gen_2224, q_gen_2247) -> q_gen_2246
<b, nil>() -> q_gen_2248
<b, pair2>(q_gen_2224, q_gen_2247) -> q_gen_2249
<nil2, pair2>(q_gen_2247, q_gen_2247) -> q_gen_2262
<b, pair2>(q_gen_2247, q_gen_2247) -> q_gen_2263
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2274
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2275
<nil2, b>() -> q_gen_2276
<a, b>() -> q_gen_2277
<cons2, pair2>(q_gen_2277, q_gen_2289, q_gen_2276, q_gen_2288) -> q_gen_2287
<nil2, a>() -> q_gen_2288
<a, a>() -> q_gen_2289
<a, pair2>(q_gen_2247, q_gen_2224) -> q_gen_2290
<cons2, nil>(q_gen_2224, q_gen_2285) -> q_gen_2299
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2301, q_gen_2301) -> q_gen_2300
<cons2, b>(q_gen_2247, q_gen_2258) -> q_gen_2301
<cons2, pair2>(q_gen_2277, q_gen_2289, q_gen_2301, q_gen_2309) -> q_gen_2308
<cons2, a>(q_gen_2247, q_gen_2258) -> q_gen_2309
<cons2, nil>(q_gen_2247, q_gen_2258) -> q_gen_2318
<cons2, pair2>(q_gen_2320, q_gen_2320, q_gen_2276, q_gen_2276) -> q_gen_2319
<b, b>() -> q_gen_2320
<cons2, pair2>(q_gen_2320, q_gen_2330, q_gen_2276, q_gen_2288) -> q_gen_2329
<b, a>() -> q_gen_2330
<b, nil2, nil2, nil>() -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2221
<a, nil2, nil2, nil>() -> q_gen_2241
<a, nil2, cons2, cons>(q_gen_2249, q_gen_2248, q_gen_2246, q_gen_2222) -> q_gen_2245
<b, cons2, nil2, nil>(q_gen_2247, q_gen_2258) -> q_gen_2257
<b, nil2, cons2, cons>(q_gen_2263, q_gen_2248, q_gen_2262, q_gen_2222) -> q_gen_2261
<a, cons2, nil2, nil>(q_gen_2247, q_gen_2258) -> q_gen_2270
<b, nil2, cons2, cons>(q_gen_2263, q_gen_2248, q_gen_2275, q_gen_2274) -> q_gen_2273
<b, cons2, nil2, nil>(q_gen_2247, q_gen_2285) -> q_gen_2284
<b, nil2, cons2, cons>(q_gen_2290, q_gen_2225, q_gen_2287, q_gen_2274) -> q_gen_2286
<b, nil2, cons2, cons>(q_gen_2263, q_gen_2248, q_gen_2300, q_gen_2299) -> q_gen_2298
<b, nil2, cons2, cons>(q_gen_2290, q_gen_2225, q_gen_2308, q_gen_2299) -> q_gen_2307
<b, nil2, cons2, cons>(q_gen_2263, q_gen_2248, q_gen_2319, q_gen_2318) -> q_gen_2317
<b, nil2, cons2, cons>(q_gen_2290, q_gen_2225, q_gen_2329, q_gen_2318) -> q_gen_2328
}

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.005625 s (model generation: 0.003943,  model checking: 0.001682):

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 1  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 1  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 1
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> nil2
})

-------------------------------------------
Step 1, which took 0.004050 s (model generation: 0.003531,  model checking: 0.000519):

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

}

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

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 1  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 1  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 1
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> nil2
})

-------------------------------------------
Step 2, which took 0.003935 s (model generation: 0.003398,  model checking: 0.000537):

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

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

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 1  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 1  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 1
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> nil2  ;  z -> b
})

-------------------------------------------
Step 3, which took 0.004284 s (model generation: 0.003540,  model checking: 0.000744):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
}

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

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 1  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 1  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> a  ;  y -> nil2  ;  y2 -> a  ;  ys -> nil2
})

-------------------------------------------
Step 4, which took 0.009375 s (model generation: 0.003630,  model checking: 0.005745):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 2  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> a
})

-------------------------------------------
Step 5, which took 0.004798 s (model generation: 0.004309,  model checking: 0.000489):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<a>() -> q_gen_2220
<b>() -> q_gen_2220
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: ((zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]), {
_ada -> cons(pair2(b, b), nil)  ;  _bda -> nil  ;  x -> a  ;  xs -> nil2  ;  y -> a  ;  ys -> nil2
})

-------------------------------------------
Step 6, which took 0.006060 s (model generation: 0.004428,  model checking: 0.001632):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2237, q_gen_2217) -> q_gen_2236
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2237
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> nil2
})

-------------------------------------------
Step 7, which took 0.013438 s (model generation: 0.005897,  model checking: 0.007541):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2237, q_gen_2217) -> q_gen_2236
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2237
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(b, nil2)
})

-------------------------------------------
Step 8, which took 0.010481 s (model generation: 0.004841,  model checking: 0.005640):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 4
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 9, which took 0.007158 s (model generation: 0.004611,  model checking: 0.002547):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 4  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 7
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> a  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 10, which took 0.374233 s (model generation: 0.004983,  model checking: 0.369250):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 7  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 5  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 7
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 11, which took 0.010368 s (model generation: 0.006550,  model checking: 0.003818):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 7  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 6  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 7
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 12, which took 0.012303 s (model generation: 0.005733,  model checking: 0.006570):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 7  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 7  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 7
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(a, nil2)
})

-------------------------------------------
Step 13, which took 0.010658 s (model generation: 0.005786,  model checking: 0.004872):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2237, q_gen_2217) -> q_gen_2236
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2237
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 7  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 7  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 7
}
Sat witness: Yes: (() -> zip([cons2(z, x2), nil2, nil]), {
x2 -> nil2  ;  z -> a
})

-------------------------------------------
Step 14, which took 0.008099 s (model generation: 0.005956,  model checking: 0.002143):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2239},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2239, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2239
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 7  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 7  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 10
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 15, which took 0.956403 s (model generation: 0.006059,  model checking: 0.950344):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2237},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2237, q_gen_2217) -> q_gen_2236
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2237
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 10  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 8  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 10
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 16, which took 0.013678 s (model generation: 0.007972,  model checking: 0.005706):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 10  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 9  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 10
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 17, which took 0.018799 s (model generation: 0.007045,  model checking: 0.011754):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 10  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 10  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 10
}
Sat witness: Yes: (() -> zip([nil2, y, nil]), {
y -> cons2(a, cons2(a, nil2))
})

-------------------------------------------
Step 18, which took 0.016007 s (model generation: 0.007550,  model checking: 0.008457):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<nil2, nil>() -> q_gen_2222
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 10  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 10  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 13
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(a, nil2)
})

-------------------------------------------
Step 19, which took 0.998356 s (model generation: 0.007524,  model checking: 0.990832):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, b>() -> q_gen_2276
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 13  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 11  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 13
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> a
})

-------------------------------------------
Step 20, which took 0.022859 s (model generation: 0.009384,  model checking: 0.013475):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, b>() -> q_gen_2276
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 13  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 12  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 13
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> cons2(b, cons2(b, nil2))
})

-------------------------------------------
Step 21, which took 0.030747 s (model generation: 0.008858,  model checking: 0.021889):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, b>() -> q_gen_2276
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 13  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 13  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 16
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(a, nil2)
})

-------------------------------------------
Step 22, which took 5.819934 s (model generation: 0.009297,  model checking: 5.810637):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 16  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 14  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 16
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 23, which took 0.046968 s (model generation: 0.011061,  model checking: 0.035907):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2239, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<nil2, b>() -> q_gen_2293
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2239, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2239
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 16  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 15  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 19
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(a, cons2(b, nil2))
})

-------------------------------------------
Step 24, which took 4.569124 s (model generation: 0.011871,  model checking: 4.557253):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<nil2, b>() -> q_gen_2293
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 19  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 16  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 19
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, nil2)  ;  z -> b
})

-------------------------------------------
Step 25, which took 0.050880 s (model generation: 0.013989,  model checking: 0.036891):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<nil2, a>() -> q_gen_2293
<nil2, b>() -> q_gen_2293
<b, a>() -> q_gen_2294
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 19  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 17  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 22
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(a, cons2(b, nil2))
})

-------------------------------------------
Step 26, which took 4.663558 s (model generation: 0.013707,  model checking: 4.649851):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<nil2, a>() -> q_gen_2293
<nil2, b>() -> q_gen_2293
<b, a>() -> q_gen_2294
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, a>(q_gen_2224, q_gen_2258) -> q_gen_2276
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 22  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 18  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 22
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, cons2(b, nil2))  ;  z -> b
})

-------------------------------------------
Step 27, which took 0.056561 s (model generation: 0.016128,  model checking: 0.040433):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, a>(q_gen_2220, q_gen_2219) -> q_gen_2293
<cons2, b>(q_gen_2220, q_gen_2219) -> q_gen_2293
<nil2, a>() -> q_gen_2293
<nil2, b>() -> q_gen_2293
<b, a>() -> q_gen_2294
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, a>(q_gen_2224, q_gen_2258) -> q_gen_2276
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 22  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 19  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 25
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(b, nil2)
})

-------------------------------------------
Step 28, which took 4.636283 s (model generation: 0.017515,  model checking: 4.618768):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2238, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, a>(q_gen_2220, q_gen_2219) -> q_gen_2293
<cons2, b>(q_gen_2220, q_gen_2219) -> q_gen_2293
<nil2, a>() -> q_gen_2293
<nil2, b>() -> q_gen_2293
<b, a>() -> q_gen_2294
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2238, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2238
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, a>(q_gen_2224, q_gen_2258) -> q_gen_2276
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<b, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 25  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 20  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 25
}
Sat witness: Yes: ((zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]), {
_pca -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> cons2(b, cons2(a, nil2))  ;  z -> b
})

-------------------------------------------
Step 29, which took 0.057859 s (model generation: 0.020123,  model checking: 0.037736):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2217, q_gen_2219, q_gen_2220, q_gen_2228, q_gen_2229, q_gen_2230, q_gen_2231, q_gen_2232, q_gen_2233, q_gen_2234, q_gen_2235, q_gen_2236, q_gen_2240, q_gen_2293, q_gen_2294},
Q_f={q_gen_2217},
Delta=
{
<cons2>(q_gen_2220, q_gen_2219) -> q_gen_2219
<cons2>(q_gen_2229, q_gen_2219) -> q_gen_2219
<nil2>() -> q_gen_2219
<b>() -> q_gen_2220
<a>() -> q_gen_2229
<cons2, a>(q_gen_2220, q_gen_2219) -> q_gen_2293
<cons2, a>(q_gen_2229, q_gen_2219) -> q_gen_2293
<cons2, b>(q_gen_2220, q_gen_2219) -> q_gen_2293
<cons2, b>(q_gen_2229, q_gen_2219) -> q_gen_2293
<nil2, a>() -> q_gen_2293
<nil2, b>() -> q_gen_2293
<b, a>() -> q_gen_2294
<b, b>() -> q_gen_2294
<cons2, cons2, cons>(q_gen_2235, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<cons2, nil2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2217
<nil2, cons2, nil>(q_gen_2229, q_gen_2219) -> q_gen_2217
<nil2, nil2, nil>() -> q_gen_2217
<nil2, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2228
<nil2, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2228
<nil2, a, nil>() -> q_gen_2230
<nil2, b, nil>() -> q_gen_2230
<nil2, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2231
<nil2, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2231
<nil2, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2231
<nil2, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2231
<a, nil2, nil>() -> q_gen_2232
<b, cons2, nil>(q_gen_2220, q_gen_2219) -> q_gen_2232
<b, nil2, nil>() -> q_gen_2232
<a, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2233
<a, nil2, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2233
<b, cons2, pair2>(q_gen_2294, q_gen_2294, q_gen_2293, q_gen_2293) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2233
<b, nil2, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2233
<a, a, nil>() -> q_gen_2234
<a, b, nil>() -> q_gen_2234
<b, a, nil>() -> q_gen_2234
<b, b, nil>() -> q_gen_2234
<a, a, pair2>(q_gen_2229, q_gen_2229) -> q_gen_2235
<a, b, pair2>(q_gen_2229, q_gen_2220) -> q_gen_2235
<b, a, pair2>(q_gen_2220, q_gen_2229) -> q_gen_2235
<b, b, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2235
<cons2, cons2, cons>(q_gen_2240, q_gen_2234, q_gen_2233, q_gen_2232, q_gen_2231, q_gen_2230, q_gen_2228, q_gen_2217) -> q_gen_2236
<a, a, pair2>(q_gen_2220, q_gen_2220) -> q_gen_2240
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2216, q_gen_2222, q_gen_2223, q_gen_2224, q_gen_2225, q_gen_2226, q_gen_2258, q_gen_2276, q_gen_2277},
Q_f={q_gen_2216},
Delta=
{
<a>() -> q_gen_2224
<b>() -> q_gen_2224
<cons2>(q_gen_2224, q_gen_2258) -> q_gen_2258
<nil2>() -> q_gen_2258
<cons2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2222
<nil2, nil>() -> q_gen_2222
<cons2, pair2>(q_gen_2277, q_gen_2277, q_gen_2276, q_gen_2276) -> q_gen_2223
<nil2, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2223
<a, nil>() -> q_gen_2225
<b, nil>() -> q_gen_2225
<a, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<b, pair2>(q_gen_2224, q_gen_2224) -> q_gen_2226
<cons2, a>(q_gen_2224, q_gen_2258) -> q_gen_2276
<cons2, b>(q_gen_2224, q_gen_2258) -> q_gen_2276
<nil2, a>() -> q_gen_2276
<nil2, b>() -> q_gen_2276
<a, a>() -> q_gen_2277
<a, b>() -> q_gen_2277
<b, b>() -> q_gen_2277
<a, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<a, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<a, nil2, nil2, nil>() -> q_gen_2216
<b, cons2, nil2, nil>(q_gen_2224, q_gen_2258) -> q_gen_2216
<b, nil2, cons2, cons>(q_gen_2226, q_gen_2225, q_gen_2223, q_gen_2222) -> q_gen_2216
<b, nil2, nil2, nil>() -> q_gen_2216
}

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, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 25  ;  (zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 21  ;  (zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 28
}
Sat witness: Yes: ((zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]), {
_uca -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> a  ;  ys -> cons2(b, nil2)
})

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