Solving ../../benchmarks/smtlib/true/isaplanner_prop44.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  list -> {cons, nil}  ;  list2 -> {cons2, nil2}  ;  pair -> {pair2}
}
definition:
{
(zip, F:
{
zip(cons2(z, x2), nil2, nil) <= True
zip(nil2, y, nil) <= True
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)
}
eq_list(_vl, _wl) <= zip(_tl, _ul, _vl) /\ zip(_tl, _ul, _wl)
)
(zip_concat, F:
{
zip_concat(x, y, nil2, nil) <= True
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)
}
eq_list(_bm, _cm) <= zip_concat(_yl, _zl, _am, _bm) /\ zip_concat(_yl, _zl, _am, _cm)
)
}

properties:
{
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)
}


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

Clause system for inference is:

{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}


Solving took 60.052633 seconds.
Maybe:  timeout during learnerLast solver state:

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip(cons2(b, cons2(a, cons2(a, nil2))), cons2(a, nil2), cons(pair2(b, a), nil)) <= zip(cons2(a, cons2(a, nil2)), nil2, nil)
False <= zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), cons(pair2(a, a), nil)))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
zip_concat(a, cons2(b, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(b, a), nil))) <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= zip(cons2(b, nil2), nil2, nil)
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(a, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_1(b, pair2(x_1_0, x_1_1)) <= _r_4(x_1_1)
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_3(a, nil) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= zip(x_1_1, x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_1_0, x_3_0) /\ _r_1(x_2_0, x_3_0)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006201 s (model generation: 0.006131,  model checking: 0.000070):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
Yes: {

}

zip(nil2, y, nil) <= True  :
Yes: {
y -> nil2
}

zip_concat(x, y, nil2, nil) <= True  :
Yes: {
x -> b  ;  y -> nil2
}

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
No: ()


-------------------------------------------
Step 1, which took 0.006668 s (model generation: 0.006542,  model checking: 0.000126):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), nil2, nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(b, nil2, nil2, nil) <= True
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
Yes: {
y -> cons2(_olth_0, _olth_1)
}

zip_concat(x, y, nil2, nil) <= True  :
Yes: {
x -> b  ;  y -> cons2(_ulth_0, _ulth_1)
}

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> nil2  ;  x4 -> nil2
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> nil2  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
No: ()


-------------------------------------------
Step 2, which took 0.011633 s (model generation: 0.011514,  model checking: 0.000119):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
Yes: {
x -> a  ;  y -> nil2
}

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> cons2(_jnth_0, _jnth_1)  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(_tnth_0, nil)  ;  _em -> cons(_unth_0, cons(_koth_0, _koth_1))  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(_xnth_0, _xnth_1)
}


-------------------------------------------
Step 3, which took 0.024387 s (model generation: 0.024163,  model checking: 0.000224):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
Yes: {
x -> a  ;  y -> cons2(_moth_0, _moth_1)
}

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> nil2  ;  x4 -> nil2  ;  z -> b
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> a  ;  y -> nil2  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
No: ()


-------------------------------------------
Step 4, which took 0.027982 s (model generation: 0.027817,  model checking: 0.000165):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> a  ;  y -> cons2(_rqth_0, _rqth_1)  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(_grth_0, nil)  ;  _em -> cons(_hrth_0, cons(_nsth_0, _nsth_1))  ;  x -> b  ;  xs -> cons2(_jrth_0, _jrth_1)  ;  ys -> cons2(_krth_0, _krth_1)
}


-------------------------------------------
Step 5, which took 0.034700 s (model generation: 0.034506,  model checking: 0.000194):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> cons(_osth_0, _osth_1)  ;  x -> b  ;  y -> cons2(_qsth_0, _qsth_1)  ;  ys -> cons2(_rsth_0, _rsth_1)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(_jtth_0, nil)  ;  _em -> cons(_ktth_0, cons(_avth_0, _avth_1))  ;  x -> a  ;  xs -> nil2  ;  ys -> cons2(_ntth_0, _ntth_1)
}


-------------------------------------------
Step 6, which took 0.041984 s (model generation: 0.041735,  model checking: 0.000249):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> nil2  ;  ys -> cons2(_qvth_0, _qvth_1)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(_zvth_0, nil)  ;  _em -> cons(_awth_0, cons(_yxth_0, _yxth_1))  ;  x -> a  ;  xs -> cons2(_cwth_0, _cwth_1)  ;  ys -> cons2(_dwth_0, _dwth_1)
}


-------------------------------------------
Step 7, which took 0.044805 s (model generation: 0.044583,  model checking: 0.000222):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons2(x_0_0, x_0_1), nil) <= True
  _r_1(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _zauh_1), _zzth_1)  ;  _em -> cons(pair2(a, _abuh_1), nil)  ;  x -> a  ;  xs -> cons2(_cauh_0, _cauh_1)  ;  ys -> cons2(_dauh_0, nil2)
}


-------------------------------------------
Step 8, which took 0.109354 s (model generation: 0.108983,  model checking: 0.000371):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(nil2) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> cons2(_lbuh_0, _lbuh_1)  ;  x4 -> nil2
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(_ieuh_0, b), _sduh_1)  ;  _em -> cons(pair2(_jeuh_0, a), nil)  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(_wduh_0, _wduh_1)
}


-------------------------------------------
Step 9, which took 0.322567 s (model generation: 0.322158,  model checking: 0.000409):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), pair2(x_1_0, x_1_1)) <= _r_3(x_1_0)
  _r_1(nil2, pair2(x_1_0, x_1_1)) <= _r_3(x_1_1)
  _r_3(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(_vhuh_0, a), cons(_ajuh_0, _ajuh_1))  ;  _em -> cons(_wguh_0, nil)  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(_zguh_0, nil2)
}


-------------------------------------------
Step 10, which took 0.403655 s (model generation: 0.403128,  model checking: 0.000527):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons2(x_0_0, x_0_1), nil) <= True
  _r_1(nil2, nil) <= True
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_3(x_1_0)
  _r_2(b, pair2(x_1_0, x_1_1)) <= _r_3(x_1_1)
  _r_3(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons2(x_0_0, x_0_1), nil) <= True
  _r_1(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> b
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(a, b), nil)  ;  _em -> cons(pair2(_jnuh_0, a), nil)  ;  x -> a  ;  xs -> cons2(_cmuh_0, _cmuh_1)  ;  ys -> cons2(_dmuh_0, nil2)
}


-------------------------------------------
Step 11, which took 0.520275 s (model generation: 0.519704,  model checking: 0.000571):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(nil2, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_1)
  _r_1(nil2, b, pair2(x_2_0, x_2_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  _r_3(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_0, x_2_0) /\ _r_2(x_1_1, x_2_1)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> cons2(_oouh_0, _oouh_1)  ;  x3 -> b  ;  x4 -> nil2
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(_vsuh_0, b), nil)  ;  _em -> cons(pair2(_wsuh_0, a), nil)  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(b, nil2)
}


-------------------------------------------
Step 12, which took 0.742383 s (model generation: 0.741763,  model checking: 0.000620):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  _r_3(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0) /\ _r_2(x_1_1, x_2_1)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  _r_3(a) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1) /\ _r_3(x_2_0)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(_qzuh_0, b), nil)  ;  _em -> cons(pair2(_rzuh_0, a), nil)  ;  x -> b  ;  xs -> cons2(_qxuh_0, _qxuh_1)  ;  ys -> cons2(b, nil2)
}


-------------------------------------------
Step 13, which took 5.880362 s (model generation: 5.879837,  model checking: 0.000525):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_3(a) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> cons(pair2(_revh_0, _revh_1), _kbvh_1)  ;  x -> a  ;  y -> cons2(a, _mbvh_1)  ;  ys -> cons2(b, _nbvh_1)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _bfvh_1), nil)  ;  _em -> cons(_qcvh_0, cons(_mfvh_0, _mfvh_1))  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(b, _tcvh_1)
}


-------------------------------------------
Step 14, which took 8.633597 s (model generation: 8.633080,  model checking: 0.000517):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_3(a) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _mjvh_1), nil)  ;  _em -> cons(_ihvh_0, cons(_ckvh_0, _ckvh_1))  ;  x -> b  ;  xs -> cons2(_khvh_0, _khvh_1)  ;  ys -> cons2(b, _lhvh_1)
}


-------------------------------------------
Step 15, which took 6.556434 s (model generation: 6.556067,  model checking: 0.000367):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_4(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_3(b) <= True
  _r_4(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> a  ;  y -> nil2  ;  ys -> cons2(_alvh_0, _alvh_1)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _unvh_1), nil)  ;  _em -> cons(_vlvh_0, cons(_kovh_0, _kovh_1))  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(a, _ylvh_1)
}


-------------------------------------------
Step 16, which took 4.414210 s (model generation: 4.413668,  model checking: 0.000542):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_3(a) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _ssvh_1), cons(_nuvh_0, _nuvh_1))  ;  _em -> cons(_tqvh_0, nil)  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(b, nil2)
}


-------------------------------------------
Step 17, which took 5.609401 s (model generation: 5.608880,  model checking: 0.000521):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_4(x_2_1)
  _r_3(a) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
No: ()

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _nyvh_1), nil)  ;  _em -> cons(_jwvh_0, cons(_fzvh_0, _fzvh_1))  ;  x -> b  ;  xs -> cons2(_lwvh_0, _lwvh_1)  ;  ys -> cons2(a, _mwvh_1)
}


-------------------------------------------
Step 18, which took 2.876538 s (model generation: 2.875931,  model checking: 0.000607):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_4(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_3(b) <= True
  _r_4(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_4(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= True
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_3(x_2_1)
  _r_2(a, nil) <= True
  _r_2(b, nil) <= True
  _r_3(b) <= True
  _r_4(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_1_0, x_2_0, x_3_0) /\ zip(x_1_1, x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_0, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= zip(x_1_1, x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_0, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> cons(_xawh_0, _xawh_1)  ;  x -> b  ;  y -> nil2  ;  y2 -> b  ;  ys -> cons2(_abwh_0, _abwh_1)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _aewh_1), nil)  ;  _em -> cons(_ccwh_0, cons(_ahwh_0, _ahwh_1))  ;  x -> b  ;  xs -> cons2(_ecwh_0, nil2)  ;  ys -> cons2(a, cons2(_chwh_0, _chwh_1))
}


-------------------------------------------
Step 19, which took 3.146143 s (model generation: 3.144969,  model checking: 0.001174):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_4(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= _r_3(x_2_1)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_4(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0)
  _r_3(b) <= True
  _r_4(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0, x_2_0) /\ zip(x_0_1, x_1_1, x_2_1)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_2(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_2(cons2(x_0_0, x_0_1), nil) <= True
  _r_2(nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_1_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_2(x_2_1, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> cons(pair2(b, _tnwh_1), nil)  ;  x -> a  ;  y -> cons2(b, nil2)  ;  ys -> cons2(b, nil2)
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, b), nil)  ;  _em -> cons(pair2(_iowh_0, a), nil)  ;  x -> b  ;  xs -> nil2  ;  ys -> cons2(b, nil2)
}


-------------------------------------------
Step 20, which took 3.769522 s (model generation: 3.768028,  model checking: 0.001494):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
zip_concat(a, cons2(b, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(b, a), nil))) <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_3(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_3(a) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) /\ zip(x_0_1, x_1_1, x_2_1)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  _r_1(cons2(x_0_0, x_0_1), nil) <= True
  _r_1(nil2, nil) <= True
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_3(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_3(a) <= True
  _r_4(b) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1) /\ _r_3(x_2_0)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1) /\ _r_2(x_2_0, x_3_0)
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_1) /\ _r_3(x_2_0)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> cons2(_nbxh_0, _nbxh_1)  ;  y2 -> b  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(_nixh_0, b), _fgxh_1)  ;  _em -> cons(pair2(_oixh_0, a), nil)  ;  x -> a  ;  xs -> nil2  ;  ys -> cons2(b, nil2)
}


-------------------------------------------
Step 21, which took 4.164176 s (model generation: 4.162903,  model checking: 0.001273):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
zip_concat(a, cons2(b, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(b, a), nil))) <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), pair2(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_1, x_1_1)
  _r_1(nil2, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_2(cons2(x_0_0, x_0_1), b) <= True
  _r_2(nil2, a) <= True
  _r_3(a, nil) <= True
  _r_4(b) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_1_0) /\ _r_3(x_0_0, x_2_1)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(cons2(x_0_0, x_0_1), pair2(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_1, x_1_1)
  _r_1(nil2, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_2(cons2(x_0_0, x_0_1), b) <= True
  _r_2(nil2, a) <= True
  _r_3(a, nil) <= True
  _r_4(b) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_0)
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_1_1, x_3_0)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_1, x_3_0)
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
Yes: {
_sl -> nil  ;  x2 -> cons2(_epxh_0, cons2(_wyxh_0, _wyxh_1))  ;  x3 -> a  ;  x4 -> nil2  ;  z -> b
}

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> a  ;  y -> nil2  ;  y2 -> b  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(b, _myxh_1), cons(_tzxh_0, _tzxh_1))  ;  _em -> cons(_trxh_0, nil)  ;  x -> a  ;  xs -> nil2  ;  ys -> cons2(a, _wrxh_1)
}


-------------------------------------------
Step 22, which took 9.565299 s (model generation: 9.564434,  model checking: 0.000865):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip(cons2(b, cons2(a, cons2(a, nil2))), cons2(a, nil2), cons(pair2(b, a), nil)) <= zip(cons2(a, cons2(a, nil2)), nil2, nil)
False <= zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), cons(pair2(a, a), nil)))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
zip_concat(a, cons2(b, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(b, a), nil))) <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(a, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_1(b, pair2(x_1_0, x_1_1)) <= _r_4(x_1_1)
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_3(a, nil) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= zip(x_1_1, x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_1_0, x_3_0) /\ _r_1(x_2_0, x_3_0)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|




Answer of teacher:

zip(cons2(z, x2), nil2, nil) <= True  :
No: ()

zip(nil2, y, nil) <= True  :
No: ()

zip_concat(x, y, nil2, nil) <= True  :
No: ()

zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl)  :
No: ()

zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl)  :
Yes: {
_xl -> nil  ;  x -> b  ;  y -> cons2(b, _qbyh_1)  ;  y2 -> a  ;  ys -> nil2
}

eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em)  :
Yes: {
_dm -> cons(pair2(a, a), cons(_vjyh_0, _vjyh_1))  ;  _em -> cons(_fdyh_0, nil)  ;  x -> a  ;  xs -> nil2  ;  ys -> cons2(a, _idyh_1)
}


Total time: 60.052633
Learner time: 56.900524
Teacher time: 0.011751
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip_concat(x, y, nil2, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _sl)) <= zip(x2, x4, _sl) -> 0
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _xl)) <= zip(y, ys, _xl) -> 0
eq_list(_dm, _em) <= zip(cons2(x, xs), ys, _dm) /\ zip_concat(x, xs, ys, _em) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip(cons2(a, nil2), nil2, nil) <= True
zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, cons2(a, nil2), nil2, nil) <= True
zip_concat(a, nil2, cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), nil)) <= True
zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, b), nil)) <= True
zip_concat(a, nil2, nil2, nil) <= True
zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(b, a), cons(pair2(a, a), nil))) <= True
zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, cons2(a, nil2), nil2, nil) <= True
zip_concat(b, nil2, cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(a, nil2), cons(pair2(b, a), nil)) <= True
zip_concat(b, nil2, cons2(b, nil2), cons(pair2(b, b), nil)) <= True
zip_concat(b, nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil))
zip(cons2(b, cons2(a, cons2(a, nil2))), cons2(a, nil2), cons(pair2(b, a), nil)) <= zip(cons2(a, cons2(a, nil2)), nil2, nil)
False <= zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(a, nil2), cons2(a, nil2), cons(pair2(b, a), cons(pair2(a, a), nil)))
zip_concat(a, cons2(a, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil))) <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(a, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(a, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, cons2(a, nil2), cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil))) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil)) /\ zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), nil))
zip_concat(a, cons2(b, nil2), cons2(a, cons2(b, nil2)), cons(pair2(a, a), cons(pair2(b, a), nil))) <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, a), nil)) /\ zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
zip_concat(b, cons2(b, nil2), cons2(a, nil2), cons(pair2(b, a), nil)) <= zip(cons2(b, nil2), nil2, nil)
zip_concat(b, nil2, cons2(b, cons2(a, nil2)), cons(pair2(b, b), cons(pair2(a, a), nil))) <= zip(nil2, cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip_concat(a, cons2(a, nil2), cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(a, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip_concat(b, nil2, cons2(a, nil2), cons(pair2(a, a), cons(pair2(a, a), nil)))
False <= zip_concat(b, nil2, cons2(b, nil2), cons(pair2(a, a), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
}
]


;
zip_concat ->
[
zip_concat : <elt * list2 * list2 * list>
{
  _r_1(a, pair2(x_1_0, x_1_1)) <= _r_4(x_1_0)
  _r_1(b, pair2(x_1_0, x_1_1)) <= _r_4(x_1_1)
  _r_2(a, pair2(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_5(x_1_1)
  _r_2(b, pair2(x_1_0, x_1_1)) <= True
  _r_3(a, nil) <= True
  _r_4(b) <= True
  _r_5(a) <= True
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(cons2(x_0_0, x_0_1), nil2, nil) <= True
  zip(nil2, cons2(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  zip(nil2, cons2(x_1_0, x_1_1), nil) <= True
  zip(nil2, nil2, nil) <= True
  zip_concat(a, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= zip(x_1_1, x_2_1, x_3_1)
  zip_concat(a, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(a, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_3(x_2_0, x_3_1)
  zip_concat(a, nil2, nil2, nil) <= True
  zip_concat(b, cons2(x_1_0, x_1_1), cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_1_0, x_3_0) /\ _r_1(x_2_0, x_3_0)
  zip_concat(b, cons2(x_1_0, x_1_1), nil2, nil) <= True
  zip_concat(b, nil2, cons2(x_2_0, x_2_1), cons(x_3_0, x_3_1)) <= _r_1(x_2_0, x_3_0)
  zip_concat(b, nil2, nil2, nil) <= True
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|