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

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


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

Clause system for inference is:

{
() -> zip([cons2(z, x2), nil2, nil]) -> 0
() -> zip([nil2, y, nil]) -> 0
() -> zip_concat([x, y, nil2, nil]) -> 0
(zip([x2, x4, _pca])) -> zip([cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _pca)]) -> 0
(zip([xs, ys, _bda]) /\ zip([cons2(x, xs), cons2(y, ys), _ada])) -> eq_list([_ada, cons(pair2(x, y), _bda)]) -> 0
(zip([y, ys, _uca])) -> zip_concat([x, y, cons2(y2, ys), cons(pair2(x, y2), _uca)]) -> 0
}


Solving took 0.841768 seconds.
Proved
Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<cons2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5761
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5783
<cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5783
<nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5783
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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.005958 s (model generation: 0.004819,  model checking: 0.001139):

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

-------------------------------------------
Step 1, which took 0.005050 s (model generation: 0.004609,  model checking: 0.000441):

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

}

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

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

-------------------------------------------
Step 2, which took 0.004794 s (model generation: 0.004473,  model checking: 0.000321):

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

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

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

-------------------------------------------
Step 3, which took 0.006075 s (model generation: 0.004759,  model checking: 0.001316):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759},
Q_f={q_gen_5756},
Delta=
{
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
}

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

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

-------------------------------------------
Step 4, which took 0.005411 s (model generation: 0.004966,  model checking: 0.000445):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759},
Q_f={q_gen_5756},
Delta=
{
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 5, which took 0.006608 s (model generation: 0.006063,  model checking: 0.000545):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765},
Q_f={q_gen_5756},
Delta=
{
<nil2>() -> q_gen_5758
<a>() -> q_gen_5759
<b>() -> q_gen_5759
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 6, which took 0.009595 s (model generation: 0.008391,  model checking: 0.001204):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 7, which took 0.013319 s (model generation: 0.012289,  model checking: 0.001030):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 8, which took 0.013989 s (model generation: 0.012918,  model checking: 0.001071):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 9, which took 0.015499 s (model generation: 0.012854,  model checking: 0.002645):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 10, which took 0.018700 s (model generation: 0.015396,  model checking: 0.003304):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 11, which took 0.023374 s (model generation: 0.015630,  model checking: 0.007744):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 12, which took 0.024908 s (model generation: 0.015785,  model checking: 0.009123):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 13, which took 0.019329 s (model generation: 0.016219,  model checking: 0.003110):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 14, which took 0.026423 s (model generation: 0.016760,  model checking: 0.009663):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 15, which took 0.028946 s (model generation: 0.017684,  model checking: 0.011262):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 16, which took 0.030754 s (model generation: 0.017781,  model checking: 0.012973):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 17, which took 0.023786 s (model generation: 0.019527,  model checking: 0.004259):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 18, which took 0.034690 s (model generation: 0.019855,  model checking: 0.014835):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 19, which took 0.038703 s (model generation: 0.021238,  model checking: 0.017465):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 20, which took 0.043996 s (model generation: 0.022975,  model checking: 0.021021):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 21, which took 0.039913 s (model generation: 0.014831,  model checking: 0.025082):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 22, which took 0.043296 s (model generation: 0.009947,  model checking: 0.033349):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 23, which took 0.062149 s (model generation: 0.022026,  model checking: 0.040123):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 24, which took 0.064814 s (model generation: 0.023748,  model checking: 0.041066):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<cons2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5761
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 25, which took 0.071445 s (model generation: 0.024600,  model checking: 0.046845):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<cons2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5761
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5783
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

-------------------------------------------
Step 26, which took 0.077202 s (model generation: 0.025885,  model checking: 0.051317):

Model:
|_
{
zip -> 
{{{
Q={q_gen_5756, q_gen_5758, q_gen_5759, q_gen_5765, q_gen_5766, q_gen_5767, q_gen_5768},
Q_f={q_gen_5756},
Delta=
{
<cons2>(q_gen_5759, q_gen_5758) -> q_gen_5758
<cons2>(q_gen_5766, q_gen_5758) -> q_gen_5758
<nil2>() -> q_gen_5758
<b>() -> q_gen_5759
<a>() -> q_gen_5766
<cons2, cons2, cons>(q_gen_5765, q_gen_5756) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<cons2, nil2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5759, q_gen_5758) -> q_gen_5756
<nil2, cons2, nil>(q_gen_5766, q_gen_5758) -> q_gen_5756
<nil2, nil2, nil>() -> q_gen_5756
<a, a, pair2>(q_gen_5766, q_gen_5766) -> q_gen_5765
<a, b, pair2>(q_gen_5766, q_gen_5759) -> q_gen_5765
<b, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5765
<b, b, pair2>(q_gen_5759, q_gen_5759) -> q_gen_5765
<cons2, cons2, cons>(q_gen_5768, q_gen_5756) -> q_gen_5767
<a, a, pair2>(q_gen_5759, q_gen_5766) -> q_gen_5768
}

Datatype: <list2, list2, list>
Convolution form: right
}}}
  ;  zip_concat -> 
{{{
Q={q_gen_5755, q_gen_5761, q_gen_5762, q_gen_5763, q_gen_5779, q_gen_5783, q_gen_5784},
Q_f={q_gen_5755},
Delta=
{
<a>() -> q_gen_5763
<b>() -> q_gen_5763
<cons2>(q_gen_5763, q_gen_5779) -> q_gen_5779
<nil2>() -> q_gen_5779
<cons2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5761
<nil2, nil>() -> q_gen_5761
<a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5762
<cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5783
<nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5783
<nil2, nil2, nil>() -> q_gen_5783
<a, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, a, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<b, b, pair2>(q_gen_5763, q_gen_5763) -> q_gen_5784
<a, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<a, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<a, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<a, nil2, nil2, nil>() -> q_gen_5755
<b, cons2, cons2, cons>(q_gen_5784, q_gen_5783) -> q_gen_5755
<b, cons2, nil2, nil>(q_gen_5763, q_gen_5779) -> q_gen_5755
<b, nil2, cons2, cons>(q_gen_5762, q_gen_5761) -> q_gen_5755
<b, nil2, nil2, nil>() -> q_gen_5755
}

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

Total time: 0.841768
Reason for stopping: Proved