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


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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)])}
(zip([_ac, _bc, _cc]) /\ zip([_ac, _bc, _dc])) -> eq_list([_cc, _dc])
)
(zip_concat, F:
{() -> zip_concat([x, y, nil2, nil])
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)])}
(zip_concat([_fc, _gc, _hc, _ic]) /\ zip_concat([_fc, _gc, _hc, _jc])) -> eq_list([_ic, _jc])
)
}

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


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

Clause system for inference is:

{
() -> zip([cons2(z, x2), nil2, nil]) -> 0
() -> zip([nil2, y, nil]) -> 0
() -> zip_concat([x, y, nil2, nil]) -> 0
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 0
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 0
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 0
}


Solving took 0.584603 seconds.
Proved
Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<cons2, nil>(q_gen_616, q_gen_632) -> q_gen_614
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_636
<cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_636
<nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_636
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009644 s (model generation: 0.008336,  model checking: 0.001308):

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

}

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

}

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

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

-------------------------------------------
Step 1, which took 0.008555 s (model generation: 0.008346,  model checking: 0.000209):

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

}

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

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

}
--
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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 1
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 1
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 1
}
Sat witness: Found: (() -> zip([nil2, y, nil]), {
y -> nil2
})

-------------------------------------------
Step 2, which took 0.008677 s (model generation: 0.008466,  model checking: 0.000211):

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

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

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

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

-------------------------------------------
Step 3, which took 0.011995 s (model generation: 0.010148,  model checking: 0.001847):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612},
Q_f={q_gen_609},
Delta=
{
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
}

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

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

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

-------------------------------------------
Step 4, which took 0.009408 s (model generation: 0.008442,  model checking: 0.000966):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612},
Q_f={q_gen_609},
Delta=
{
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 5, which took 0.008521 s (model generation: 0.008103,  model checking: 0.000418):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618},
Q_f={q_gen_609},
Delta=
{
<nil2>() -> q_gen_611
<a>() -> q_gen_612
<b>() -> q_gen_612
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_618
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 6, which took 0.010844 s (model generation: 0.009608,  model checking: 0.001236):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 7, which took 0.010600 s (model generation: 0.009602,  model checking: 0.000998):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 4
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 5
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 4
}
Sat witness: Found: (() -> zip([nil2, y, nil]), {
y -> cons2(b, cons2(b, nil2))
})

-------------------------------------------
Step 8, which took 0.009555 s (model generation: 0.009063,  model checking: 0.000492):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 9, which took 0.010919 s (model generation: 0.009197,  model checking: 0.001722):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 10, which took 0.012057 s (model generation: 0.010457,  model checking: 0.001600):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 7
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 5
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 7
}
Sat witness: Found: ((zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]), {
_zb -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 11, which took 0.014184 s (model generation: 0.010728,  model checking: 0.003456):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 12, which took 0.015098 s (model generation: 0.011398,  model checking: 0.003700):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 7
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 7
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 7
}
Sat witness: Found: (() -> zip([nil2, y, nil]), {
y -> cons2(b, cons2(a, nil2))
})

-------------------------------------------
Step 13, which took 0.013041 s (model generation: 0.011548,  model checking: 0.001493):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 14, which took 0.016505 s (model generation: 0.011624,  model checking: 0.004881):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 7
() -> zip([nil2, y, nil]) -> 9
() -> zip_concat([x, y, nil2, nil]) -> 9
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 10
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 8
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 10
}
Sat witness: Found: ((zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]), {
_zb -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> b
})

-------------------------------------------
Step 15, which took 0.018967 s (model generation: 0.013534,  model checking: 0.005433):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 8
() -> zip([nil2, y, nil]) -> 9
() -> zip_concat([x, y, nil2, nil]) -> 12
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 10
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 9
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 10
}
Sat witness: Found: (() -> zip_concat([x, y, nil2, nil]), {
x -> a  ;  y -> cons2(b, nil2)
})

-------------------------------------------
Step 16, which took 0.017335 s (model generation: 0.012424,  model checking: 0.004911):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 10
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 10
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 10
}
Sat witness: Found: (() -> zip([nil2, y, nil]), {
y -> cons2(a, nil2)
})

-------------------------------------------
Step 17, which took 0.015553 s (model generation: 0.013477,  model checking: 0.002076):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 18, which took 0.020753 s (model generation: 0.014564,  model checking: 0.006189):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

-------------------------------------------
Step 19, which took 0.022703 s (model generation: 0.014845,  model checking: 0.007858):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

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

-------------------------------------------
Step 20, which took 0.023084 s (model generation: 0.014932,  model checking: 0.008152):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

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

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

-------------------------------------------
Step 21, which took 0.033944 s (model generation: 0.016247,  model checking: 0.017697):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 14
() -> zip_concat([x, y, nil2, nil]) -> 16
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 14
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 14
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 19
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> nil  ;  x -> a  ;  y -> cons2(a, nil2)  ;  y2 -> a  ;  ys -> nil2
})

-------------------------------------------
Step 22, which took 0.036264 s (model generation: 0.017958,  model checking: 0.018306):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 15
() -> zip_concat([x, y, nil2, nil]) -> 17
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 15
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 15
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 22
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> nil  ;  x -> a  ;  y -> cons2(a, nil2)  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 23, which took 0.036597 s (model generation: 0.018327,  model checking: 0.018270):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 16
() -> zip_concat([x, y, nil2, nil]) -> 18
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 16
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 16
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 25
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(a, nil2)
})

-------------------------------------------
Step 24, which took 0.036808 s (model generation: 0.018451,  model checking: 0.018357):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<cons2, nil>(q_gen_616, q_gen_632) -> q_gen_614
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 17
() -> zip_concat([x, y, nil2, nil]) -> 19
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 17
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 17
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 28
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> nil  ;  x -> b  ;  y -> cons2(a, cons2(b, nil2))  ;  y2 -> b  ;  ys -> nil2
})

-------------------------------------------
Step 25, which took 0.044337 s (model generation: 0.019994,  model checking: 0.024343):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<cons2, nil>(q_gen_616, q_gen_632) -> q_gen_614
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_636
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 18
() -> zip_concat([x, y, nil2, nil]) -> 20
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 18
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 18
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 31
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> cons(pair2(a, b), nil)  ;  x -> b  ;  y -> cons2(a, nil2)  ;  y2 -> b  ;  ys -> cons2(b, nil2)
})

-------------------------------------------
Step 26, which took 0.043779 s (model generation: 0.020779,  model checking: 0.023000):

Model:
|_
{
zip -> 
{{{
Q={q_gen_609, q_gen_611, q_gen_612, q_gen_618, q_gen_619, q_gen_620, q_gen_621},
Q_f={q_gen_609},
Delta=
{
<cons2>(q_gen_612, q_gen_611) -> q_gen_611
<cons2>(q_gen_619, q_gen_611) -> q_gen_611
<nil2>() -> q_gen_611
<b>() -> q_gen_612
<a>() -> q_gen_619
<cons2, cons2, cons>(q_gen_618, q_gen_609) -> q_gen_609
<cons2, nil2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<cons2, nil2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_612, q_gen_611) -> q_gen_609
<nil2, cons2, nil>(q_gen_619, q_gen_611) -> q_gen_609
<nil2, nil2, nil>() -> q_gen_609
<a, a, pair2>(q_gen_619, q_gen_619) -> q_gen_618
<a, b, pair2>(q_gen_619, q_gen_612) -> q_gen_618
<b, a, pair2>(q_gen_612, q_gen_619) -> q_gen_618
<b, b, pair2>(q_gen_612, q_gen_612) -> q_gen_618
<cons2, cons2, cons>(q_gen_621, q_gen_609) -> q_gen_620
<a, a, pair2>(q_gen_612, q_gen_612) -> q_gen_621
}

Datatype: <list2, list2, list>
Convolution form: left
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_608, q_gen_614, q_gen_615, q_gen_616, q_gen_632, q_gen_636, q_gen_637},
Q_f={q_gen_608},
Delta=
{
<a>() -> q_gen_616
<b>() -> q_gen_616
<cons2>(q_gen_616, q_gen_632) -> q_gen_632
<nil2>() -> q_gen_632
<cons2, nil>(q_gen_616, q_gen_632) -> q_gen_614
<nil2, nil>() -> q_gen_614
<a, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<b, pair2>(q_gen_616, q_gen_616) -> q_gen_615
<cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_636
<nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_636
<nil2, nil2, nil>() -> q_gen_636
<a, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, a, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<b, b, pair2>(q_gen_616, q_gen_616) -> q_gen_637
<a, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<a, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<a, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<a, nil2, nil2, nil>() -> q_gen_608
<b, cons2, cons2, cons>(q_gen_637, q_gen_636) -> q_gen_608
<b, cons2, nil2, nil>(q_gen_616, q_gen_632) -> q_gen_608
<b, nil2, cons2, cons>(q_gen_615, q_gen_614) -> q_gen_608
<b, nil2, nil2, nil>() -> q_gen_608
}

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

}
--
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]) -> 19
() -> zip_concat([x, y, nil2, nil]) -> 21
(zip([x2, x4, _zb])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _zb)]) -> 19
(zip([xs, ys, _lc]) /\ zip([cons2(x, xs), cons2(y, ys), _kc])) -> eq_list([_kc, cons(pair2(x, y), _lc)]) -> 19
(zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]) -> 34
}
Sat witness: Found: ((zip([y, ys, _ec])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _ec)]), {
_ec -> cons(pair2(b, b), nil)  ;  x -> b  ;  y -> cons2(b, cons2(b, nil2))  ;  y2 -> a  ;  ys -> cons2(b, nil2)
})

Total time: 0.584603
Reason for stopping: Proved