Solving ../../benchmarks/true/isaplanner_prop44.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, _tf])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _tf)])}
(zip([_uf, _vf, _wf]) /\ zip([_uf, _vf, _xf])) -> eq_list([_wf, _xf])
)
(zip_concat, F:
{() -> zip_concat([x, y, nil2, nil])
(zip([y, ys, _yf])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _yf)])}
(zip_concat([_zf, _ag, _bg, _cg]) /\ zip_concat([_zf, _ag, _bg, _dg])) -> eq_list([_cg, _dg])
)
}

properties:
{(zip([cons2(x, xs), ys, _eg]) /\ zip_concat([x, xs, ys, _fg])) -> eq_list([_eg, _fg])}


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

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


Solving took 30.019978 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2112, q_gen_2113, q_gen_2114, q_gen_2121, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2131, q_gen_2132, q_gen_2133, q_gen_2134, q_gen_2136, q_gen_2137, q_gen_2138, q_gen_2144, q_gen_2145, q_gen_2146, q_gen_2147, q_gen_2148, q_gen_2149, q_gen_2150, q_gen_2156, q_gen_2157, q_gen_2160, q_gen_2161, q_gen_2162, q_gen_2163, q_gen_2164, q_gen_2165, q_gen_2168, q_gen_2169, q_gen_2173, q_gen_2174, q_gen_2175, q_gen_2176, q_gen_2177, q_gen_2178, q_gen_2188, q_gen_2189, q_gen_2190, q_gen_2191, q_gen_2192, q_gen_2193, q_gen_2202, q_gen_2203, q_gen_2204, q_gen_2205, q_gen_2206, q_gen_2209},
Q_f={},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2138
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2169
<nil2, b>() -> q_gen_2190
<b, b>() -> q_gen_2191
<nil2, a>() -> q_gen_2204
<b, a>() -> q_gen_2205
<nil2, nil2, nil>() -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2112
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2121
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2131, q_gen_2111) -> q_gen_2130
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2131
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2136
<cons2, nil2, nil>(q_gen_2114, q_gen_2138) -> q_gen_2137
<cons2, cons2, cons>(q_gen_2150, q_gen_2149, q_gen_2148, q_gen_2147, q_gen_2146, q_gen_2124, q_gen_2145, q_gen_2111) -> q_gen_2144
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2145
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2146
<b, nil2, nil>() -> q_gen_2147
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2148
<b, a, nil>() -> q_gen_2149
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2150
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2156
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2157
<cons2, cons2, cons>(q_gen_2165, q_gen_2164, q_gen_2163, q_gen_2147, q_gen_2162, q_gen_2161, q_gen_2131, q_gen_2111) -> q_gen_2160
<nil2, b, nil>() -> q_gen_2161
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2162
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2163
<b, b, nil>() -> q_gen_2164
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2165
<nil2, cons2, nil>(q_gen_2123, q_gen_2169) -> q_gen_2168
<cons2, cons2, cons>(q_gen_2178, q_gen_2177, q_gen_2176, q_gen_2126, q_gen_2175, q_gen_2161, q_gen_2174, q_gen_2111) -> q_gen_2173
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2174
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2175
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2176
<a, b, nil>() -> q_gen_2177
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2178
<cons2, cons2, cons>(q_gen_2165, q_gen_2164, q_gen_2193, q_gen_2192, q_gen_2162, q_gen_2161, q_gen_2189, q_gen_2136) -> q_gen_2188
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2189
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2192
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2193
<cons2, cons2, cons>(q_gen_2150, q_gen_2149, q_gen_2206, q_gen_2192, q_gen_2146, q_gen_2124, q_gen_2203, q_gen_2136) -> q_gen_2202
<nil2, cons2, pair2>(q_gen_2191, q_gen_2205, q_gen_2190, q_gen_2204) -> q_gen_2203
<b, cons2, pair2>(q_gen_2191, q_gen_2205, q_gen_2190, q_gen_2204) -> q_gen_2206
<nil2, cons2, nil>(q_gen_2123, q_gen_2138) -> q_gen_2209
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2115, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2135, q_gen_2139, q_gen_2140, q_gen_2141, q_gen_2142, q_gen_2143, q_gen_2151, q_gen_2152, q_gen_2153, q_gen_2154, q_gen_2155, q_gen_2158, q_gen_2159, q_gen_2166, q_gen_2167, q_gen_2170, q_gen_2171, q_gen_2172, q_gen_2179, q_gen_2180, q_gen_2181, q_gen_2182, q_gen_2183, q_gen_2184, q_gen_2185, q_gen_2186, q_gen_2187, q_gen_2194, q_gen_2195, q_gen_2196, q_gen_2197, q_gen_2198, q_gen_2199, q_gen_2200, q_gen_2201, q_gen_2207, q_gen_2208, q_gen_2210, q_gen_2211, q_gen_2212, q_gen_2213, q_gen_2214, q_gen_2215},
Q_f={},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<cons2>(q_gen_2118, q_gen_2155) -> q_gen_2198
<cons2>(q_gen_2141, q_gen_2155) -> q_gen_2208
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2140
<b, nil>() -> q_gen_2142
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2159
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2171
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2172
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2182
<cons2, pair2>(q_gen_2187, q_gen_2186, q_gen_2185, q_gen_2184) -> q_gen_2183
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2185
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2187
<cons2, nil>(q_gen_2118, q_gen_2198) -> q_gen_2197
<cons2, pair2>(q_gen_2186, q_gen_2187, q_gen_2201, q_gen_2200) -> q_gen_2199
<cons2, b>(q_gen_2118, q_gen_2155) -> q_gen_2200
<cons2, a>(q_gen_2118, q_gen_2155) -> q_gen_2201
<cons2, nil>(q_gen_2118, q_gen_2208) -> q_gen_2211
<cons2, pair2>(q_gen_2186, q_gen_2187, q_gen_2214, q_gen_2213) -> q_gen_2212
<cons2, b>(q_gen_2141, q_gen_2155) -> q_gen_2213
<cons2, a>(q_gen_2141, q_gen_2155) -> q_gen_2214
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2115
<a, nil2, nil2, nil>() -> q_gen_2135
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2140, q_gen_2116) -> q_gen_2139
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2154
<b, nil2, cons2, cons>(q_gen_2159, q_gen_2142, q_gen_2152, q_gen_2116) -> q_gen_2158
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2166
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2167
<b, nil2, cons2, cons>(q_gen_2172, q_gen_2119, q_gen_2171, q_gen_2116) -> q_gen_2170
<a, nil2, cons2, cons>(q_gen_2159, q_gen_2142, q_gen_2152, q_gen_2116) -> q_gen_2179
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2180
<b, nil2, cons2, cons>(q_gen_2172, q_gen_2119, q_gen_2183, q_gen_2182) -> q_gen_2181
<a, nil2, cons2, cons>(q_gen_2172, q_gen_2119, q_gen_2171, q_gen_2116) -> q_gen_2194
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2195
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2199, q_gen_2197) -> q_gen_2196
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2208) -> q_gen_2207
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2212, q_gen_2211) -> q_gen_2210
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2215
}

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.005812 s (model generation: 0.003631,  model checking: 0.002181):

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

-------------------------------------------
Step 1, which took 0.004269 s (model generation: 0.003433,  model checking: 0.000836):

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

}

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

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

-------------------------------------------
Step 2, which took 0.004204 s (model generation: 0.003477,  model checking: 0.000727):

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

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

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

-------------------------------------------
Step 3, which took 0.004573 s (model generation: 0.003589,  model checking: 0.000984):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
}

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

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

-------------------------------------------
Step 4, which took 0.010020 s (model generation: 0.003851,  model checking: 0.006169):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 5, which took 0.004735 s (model generation: 0.004236,  model checking: 0.000499):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<a>() -> q_gen_2114
<b>() -> q_gen_2114
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 6, which took 0.006139 s (model generation: 0.004589,  model checking: 0.001550):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2131},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2131, q_gen_2111) -> q_gen_2130
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2131
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 7, which took 0.009380 s (model generation: 0.004300,  model checking: 0.005080):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2131},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2131, q_gen_2111) -> q_gen_2130
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2131
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 8, which took 0.009451 s (model generation: 0.004341,  model checking: 0.005110):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 9, which took 0.007489 s (model generation: 0.004529,  model checking: 0.002960):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 10, which took 0.315906 s (model generation: 0.004792,  model checking: 0.311114):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 11, which took 0.008367 s (model generation: 0.006937,  model checking: 0.001430):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2118
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
}

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

-------------------------------------------
Step 12, which took 0.008083 s (model generation: 0.006271,  model checking: 0.001812):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2152},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 13, which took 0.010723 s (model generation: 0.006033,  model checking: 0.004690):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2152, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 14, which took 0.011051 s (model generation: 0.006272,  model checking: 0.004779):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2131},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2131, q_gen_2111) -> q_gen_2130
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2131
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 15, which took 0.011330 s (model generation: 0.006564,  model checking: 0.004766):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 16, which took 0.982769 s (model generation: 0.006570,  model checking: 0.976199):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2131},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2131, q_gen_2111) -> q_gen_2130
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2131
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 17, which took 0.018402 s (model generation: 0.008623,  model checking: 0.009779):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 18, which took 0.010383 s (model generation: 0.008028,  model checking: 0.002355):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 19, which took 0.012636 s (model generation: 0.007810,  model checking: 0.004826):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 20, which took 0.018249 s (model generation: 0.007919,  model checking: 0.010330):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 21, which took 0.864930 s (model generation: 0.008891,  model checking: 0.856039):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 22, which took 0.055492 s (model generation: 0.010764,  model checking: 0.044728):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 23, which took 0.017703 s (model generation: 0.010761,  model checking: 0.006942):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2143, q_gen_2151, q_gen_2152, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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]) -> 12  ;  () -> zip_concat([x, y, nil2, nil]) -> 15  ;  (zip([x2, x4, _tf])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _tf)]) -> 13  ;  (zip([y, ys, _yf])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _yf)]) -> 13  ;  (zip([cons2(x, xs), ys, _eg]) /\ zip_concat([x, xs, ys, _fg])) -> eq_list([_eg, _fg]) -> 14
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 24, which took 0.047256 s (model generation: 0.010412,  model checking: 0.036844):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2134},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2134, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2134
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2142, q_gen_2143, q_gen_2151, q_gen_2155},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<b, nil>() -> q_gen_2142
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 25, which took 5.819698 s (model generation: 0.011059,  model checking: 5.808639):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2142, q_gen_2143, q_gen_2151, q_gen_2155, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<b, nil>() -> q_gen_2142
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 26, which took 0.053476 s (model generation: 0.012667,  model checking: 0.040809):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, b>() -> q_gen_2190
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2142, q_gen_2143, q_gen_2151, q_gen_2155, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<b, nil>() -> q_gen_2142
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2142, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 27, which took 0.025469 s (model generation: 0.012389,  model checking: 0.013080):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, b>() -> q_gen_2190
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2143, q_gen_2151, q_gen_2152, q_gen_2155, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2152
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2152
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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]) -> 18  ;  (zip([x2, x4, _tf])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _tf)]) -> 16  ;  (zip([y, ys, _yf])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _yf)]) -> 16  ;  (zip([cons2(x, xs), ys, _eg]) /\ zip_concat([x, xs, ys, _fg])) -> eq_list([_eg, _fg]) -> 17
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> cons2(a, nil2)
})

-------------------------------------------
Step 28, which took 0.122415 s (model generation: 0.012335,  model checking: 0.110080):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, b>() -> q_gen_2190
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2143, q_gen_2151, q_gen_2152, q_gen_2155, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2152
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 29, which took 4.575571 s (model generation: 0.013963,  model checking: 4.561608):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2132, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, b>() -> q_gen_2190
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2132, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2132
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155, q_gen_2159, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<cons2>(q_gen_2118, q_gen_2155) -> q_gen_2155
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2159
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2159
<cons2, a>(q_gen_2118, q_gen_2155) -> q_gen_2184
<cons2, b>(q_gen_2118, q_gen_2155) -> q_gen_2184
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 30, which took 0.087451 s (model generation: 0.015366,  model checking: 0.072085):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, a>() -> q_gen_2190
<nil2, b>() -> q_gen_2190
<b, a>() -> q_gen_2191
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155, q_gen_2159, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<cons2>(q_gen_2118, q_gen_2155) -> q_gen_2155
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2159
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2159
<cons2, a>(q_gen_2118, q_gen_2155) -> q_gen_2184
<cons2, b>(q_gen_2118, q_gen_2155) -> q_gen_2184
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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]) -> 21  ;  (zip([x2, x4, _tf])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _tf)]) -> 19  ;  (zip([y, ys, _yf])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _yf)]) -> 19  ;  (zip([cons2(x, xs), ys, _eg]) /\ zip_concat([x, xs, ys, _fg])) -> eq_list([_eg, _fg]) -> 18
}
Sat witness: Yes: (() -> zip_concat([x, y, nil2, nil]), {
x -> b  ;  y -> cons2(b, cons2(b, nil2))
})

-------------------------------------------
Step 31, which took 0.093417 s (model generation: 0.015617,  model checking: 0.077800):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, a>() -> q_gen_2190
<nil2, b>() -> q_gen_2190
<b, a>() -> q_gen_2191
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2151, q_gen_2153, q_gen_2155, q_gen_2159, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<cons2>(q_gen_2118, q_gen_2155) -> q_gen_2155
<cons2>(q_gen_2141, q_gen_2155) -> q_gen_2155
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2153
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2159
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2159
<cons2, a>(q_gen_2118, q_gen_2155) -> q_gen_2184
<cons2, b>(q_gen_2118, q_gen_2155) -> q_gen_2184
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2159, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2153, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2151
}

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

-------------------------------------------
Step 32, which took 0.070462 s (model generation: 0.017335,  model checking: 0.053127):

Model:
|_
{
zip -> 
{{{
Q={q_gen_2111, q_gen_2113, q_gen_2114, q_gen_2122, q_gen_2123, q_gen_2124, q_gen_2125, q_gen_2126, q_gen_2127, q_gen_2128, q_gen_2129, q_gen_2130, q_gen_2133, q_gen_2190, q_gen_2191},
Q_f={q_gen_2111},
Delta=
{
<cons2>(q_gen_2114, q_gen_2113) -> q_gen_2113
<cons2>(q_gen_2123, q_gen_2113) -> q_gen_2113
<nil2>() -> q_gen_2113
<b>() -> q_gen_2114
<a>() -> q_gen_2123
<nil2, a>() -> q_gen_2190
<nil2, b>() -> q_gen_2190
<b, a>() -> q_gen_2191
<b, b>() -> q_gen_2191
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2127, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<cons2, nil2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2111
<nil2, cons2, nil>(q_gen_2123, q_gen_2113) -> q_gen_2111
<nil2, nil2, nil>() -> q_gen_2111
<nil2, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2122
<nil2, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2122
<nil2, a, nil>() -> q_gen_2124
<nil2, b, nil>() -> q_gen_2124
<nil2, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2125
<nil2, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2125
<nil2, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2125
<nil2, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2125
<a, nil2, nil>() -> q_gen_2126
<b, cons2, nil>(q_gen_2114, q_gen_2113) -> q_gen_2126
<b, nil2, nil>() -> q_gen_2126
<a, nil2, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2127
<a, nil2, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2127
<b, cons2, pair2>(q_gen_2191, q_gen_2191, q_gen_2190, q_gen_2190) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2127
<b, nil2, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2127
<a, a, nil>() -> q_gen_2128
<a, b, nil>() -> q_gen_2128
<b, a, nil>() -> q_gen_2128
<b, b, nil>() -> q_gen_2128
<a, a, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<a, a, pair2>(q_gen_2123, q_gen_2123) -> q_gen_2129
<a, b, pair2>(q_gen_2123, q_gen_2114) -> q_gen_2129
<b, a, pair2>(q_gen_2114, q_gen_2123) -> q_gen_2129
<b, b, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2129
<cons2, cons2, cons>(q_gen_2129, q_gen_2128, q_gen_2133, q_gen_2126, q_gen_2125, q_gen_2124, q_gen_2122, q_gen_2111) -> q_gen_2130
<a, nil2, pair2>(q_gen_2114, q_gen_2114) -> q_gen_2133
}

Datatype: <list2, list2, list>
Convolution form: complete
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_2110, q_gen_2116, q_gen_2117, q_gen_2118, q_gen_2119, q_gen_2120, q_gen_2141, q_gen_2143, q_gen_2151, q_gen_2152, q_gen_2155, q_gen_2184, q_gen_2186},
Q_f={q_gen_2110},
Delta=
{
<a>() -> q_gen_2118
<b>() -> q_gen_2141
<cons2>(q_gen_2118, q_gen_2155) -> q_gen_2155
<cons2>(q_gen_2141, q_gen_2155) -> q_gen_2155
<nil2>() -> q_gen_2155
<cons2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2116
<nil2, nil>() -> q_gen_2116
<cons2, pair2>(q_gen_2186, q_gen_2186, q_gen_2184, q_gen_2184) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2117
<nil2, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2117
<a, nil>() -> q_gen_2119
<b, nil>() -> q_gen_2119
<a, pair2>(q_gen_2118, q_gen_2118) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2120
<b, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2120
<a, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2143
<b, pair2>(q_gen_2118, q_gen_2141) -> q_gen_2143
<nil2, pair2>(q_gen_2141, q_gen_2118) -> q_gen_2152
<nil2, pair2>(q_gen_2141, q_gen_2141) -> q_gen_2152
<cons2, a>(q_gen_2118, q_gen_2155) -> q_gen_2184
<cons2, a>(q_gen_2141, q_gen_2155) -> q_gen_2184
<cons2, b>(q_gen_2118, q_gen_2155) -> q_gen_2184
<cons2, b>(q_gen_2141, q_gen_2155) -> q_gen_2184
<nil2, a>() -> q_gen_2184
<nil2, b>() -> q_gen_2184
<a, a>() -> q_gen_2186
<a, b>() -> q_gen_2186
<a, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<a, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<a, nil2, nil2, nil>() -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2118, q_gen_2155) -> q_gen_2110
<b, cons2, nil2, nil>(q_gen_2141, q_gen_2155) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2117, q_gen_2116) -> q_gen_2110
<b, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2110
<b, nil2, nil2, nil>() -> q_gen_2110
<a, nil2, cons2, cons>(q_gen_2120, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<a, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
<b, nil2, cons2, cons>(q_gen_2143, q_gen_2119, q_gen_2152, q_gen_2116) -> q_gen_2151
}

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

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