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


Learning problem is:

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

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


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

Clause system for inference is:

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


Solving took 0.875920 seconds.
Proved
Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<cons2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4036
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4058
<cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4058
<nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4058
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.009408 s (model generation: 0.007633,  model checking: 0.001775):

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

}

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.010441 s (model generation: 0.010079,  model checking: 0.000362):

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.011450 s (model generation: 0.010457,  model checking: 0.000993):

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

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

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

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

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

-------------------------------------------
Step 3, which took 0.012274 s (model generation: 0.011378,  model checking: 0.000896):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034},
Q_f={q_gen_4031},
Delta=
{
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
}

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

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

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

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

-------------------------------------------
Step 4, which took 0.013301 s (model generation: 0.011702,  model checking: 0.001599):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034},
Q_f={q_gen_4031},
Delta=
{
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 5, which took 0.013338 s (model generation: 0.012329,  model checking: 0.001009):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040},
Q_f={q_gen_4031},
Delta=
{
<nil2>() -> q_gen_4033
<a>() -> q_gen_4034
<b>() -> q_gen_4034
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 6, which took 0.014330 s (model generation: 0.013283,  model checking: 0.001047):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 7, which took 0.014206 s (model generation: 0.012974,  model checking: 0.001232):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 8, which took 0.013786 s (model generation: 0.012580,  model checking: 0.001206):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 9, which took 0.014794 s (model generation: 0.012851,  model checking: 0.001943):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 10, which took 0.015907 s (model generation: 0.013198,  model checking: 0.002709):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 11, which took 0.020897 s (model generation: 0.014177,  model checking: 0.006720):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 12, which took 0.021200 s (model generation: 0.014395,  model checking: 0.006805):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 13, which took 0.018656 s (model generation: 0.016008,  model checking: 0.002648):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 14, which took 0.024294 s (model generation: 0.016273,  model checking: 0.008021):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 15, which took 0.027229 s (model generation: 0.017198,  model checking: 0.010031):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 16, which took 0.027651 s (model generation: 0.017516,  model checking: 0.010135):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 17, which took 0.022106 s (model generation: 0.018749,  model checking: 0.003357):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 18, which took 0.032269 s (model generation: 0.019134,  model checking: 0.013135):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 19, which took 0.034001 s (model generation: 0.019506,  model checking: 0.014495):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 20, which took 0.035838 s (model generation: 0.019931,  model checking: 0.015907):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

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

-------------------------------------------
Step 21, which took 0.056383 s (model generation: 0.020544,  model checking: 0.035839):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 22, which took 0.057969 s (model generation: 0.021861,  model checking: 0.036108):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 23, which took 0.059112 s (model generation: 0.023427,  model checking: 0.035685):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 24, which took 0.060429 s (model generation: 0.024581,  model checking: 0.035848):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<cons2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4036
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 25, which took 0.067687 s (model generation: 0.026624,  model checking: 0.041063):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<cons2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4036
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4058
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

-------------------------------------------
Step 26, which took 0.070684 s (model generation: 0.027186,  model checking: 0.043498):

Model:
|_
{
zip -> 
{{{
Q={q_gen_4031, q_gen_4033, q_gen_4034, q_gen_4040, q_gen_4041, q_gen_4042, q_gen_4043},
Q_f={q_gen_4031},
Delta=
{
<cons2>(q_gen_4034, q_gen_4033) -> q_gen_4033
<cons2>(q_gen_4041, q_gen_4033) -> q_gen_4033
<nil2>() -> q_gen_4033
<b>() -> q_gen_4034
<a>() -> q_gen_4041
<cons2, cons2, cons>(q_gen_4040, q_gen_4031) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<cons2, nil2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4034, q_gen_4033) -> q_gen_4031
<nil2, cons2, nil>(q_gen_4041, q_gen_4033) -> q_gen_4031
<nil2, nil2, nil>() -> q_gen_4031
<a, a, pair2>(q_gen_4041, q_gen_4041) -> q_gen_4040
<a, b, pair2>(q_gen_4041, q_gen_4034) -> q_gen_4040
<b, a, pair2>(q_gen_4034, q_gen_4041) -> q_gen_4040
<b, b, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4040
<cons2, cons2, cons>(q_gen_4043, q_gen_4031) -> q_gen_4042
<a, a, pair2>(q_gen_4034, q_gen_4034) -> q_gen_4043
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_4030, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4054, q_gen_4058, q_gen_4059},
Q_f={q_gen_4030},
Delta=
{
<a>() -> q_gen_4038
<b>() -> q_gen_4038
<cons2>(q_gen_4038, q_gen_4054) -> q_gen_4054
<nil2>() -> q_gen_4054
<cons2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4036
<nil2, nil>() -> q_gen_4036
<a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4037
<cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4058
<nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4058
<nil2, nil2, nil>() -> q_gen_4058
<a, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, a, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<b, b, pair2>(q_gen_4038, q_gen_4038) -> q_gen_4059
<a, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<a, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<a, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<a, nil2, nil2, nil>() -> q_gen_4030
<b, cons2, cons2, cons>(q_gen_4059, q_gen_4058) -> q_gen_4030
<b, cons2, nil2, nil>(q_gen_4038, q_gen_4054) -> q_gen_4030
<b, nil2, cons2, cons>(q_gen_4037, q_gen_4036) -> q_gen_4030
<b, nil2, nil2, nil>() -> q_gen_4030
}

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

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

Total time: 0.875920
Reason for stopping: Proved