Solving ../../benchmarks/smtlib/true/isaplanner_prop45.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), _cta)) <= zip(x2, x4, _cta)
}
eq_list(_fta, _gta) <= zip(_dta, _eta, _fta) /\ zip(_dta, _eta, _gta)
)
(zip_concat, F:
{
zip_concat(x, y, nil2, nil) <= True
zip_concat(x, y, cons2(y2, ys), cons(pair2(x, y2), _hta)) <= zip(y, ys, _hta)
}
eq_list(_lta, _mta) <= zip_concat(_ita, _jta, _kta, _lta) /\ zip_concat(_ita, _jta, _kta, _mta)
)
}

properties:
{
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)
}


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

Clause system for inference is:

{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}


Solving took 5.821995 seconds.
Yes: |_
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)) <= _r_2(x_2_1) /\ _r_3(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_2(x_2_1)
  _r_2(b) <= 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) /\ 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
}
]



--
Equality automata are defined for: {elt, list, list2, pair}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006049 s (model generation: 0.005958,  model checking: 0.000091):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

zip ->
[
zip : <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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
No: ()


-------------------------------------------
Step 1, which took 0.006342 s (model generation: 0.006285,  model checking: 0.000057):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), nil2, nil) <= True
zip(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
}
]



--
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(_yjyh_0, _yjyh_1)
}

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

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
No: ()


-------------------------------------------
Step 2, which took 0.009983 s (model generation: 0.009887,  model checking: 0.000096):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 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
}

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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(_fkyh_0, nil)  ;  _ota -> cons(_gkyh_0, _gkyh_1)  ;  xs -> cons2(_hkyh_0, _hkyh_1)  ;  ys -> cons2(_ikyh_0, _ikyh_1)
}


-------------------------------------------
Step 3, which took 0.012998 s (model generation: 0.012713,  model checking: 0.000285):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), 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)) <= 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(_hnyh_0, b), nil)  ;  _ota -> nil  ;  xs -> nil2  ;  y -> a  ;  ys -> cons2(_bnyh_0, _bnyh_1)
}


-------------------------------------------
Step 4, which took 0.021431 s (model generation: 0.021242,  model checking: 0.000189):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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_1_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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x4 -> cons2(_zoyh_0, _zoyh_1)
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(_ppyh_0, cons(_mqyh_0, _mqyh_1))  ;  _ota -> nil  ;  xs -> nil2  ;  ys -> nil2
}


-------------------------------------------
Step 5, which took 0.052131 s (model generation: 0.051692,  model checking: 0.000439):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), nil))
False <= zip(cons2(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(pair2(x_0_0, x_0_1)) <= _r_2(x_0_1)
  _r_2(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_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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(b, a), nil)  ;  _ota -> nil  ;  x -> a  ;  xs -> nil2  ;  ys -> nil2
}


-------------------------------------------
Step 6, which took 0.091401 s (model generation: 0.090792,  model checking: 0.000609):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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(nil2, cons2(a, nil2), nil) <= True
zip(nil2, nil2, nil) <= True
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, pair2(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ _r_2(x_1_1)
  _r_1(b, pair2(x_1_0, x_1_1)) <= True
  _r_2(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_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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x3 -> a  ;  x4 -> nil2  ;  z -> b
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(b, _lxyh_1), nil)  ;  _ota -> nil  ;  x -> a  ;  xs -> cons2(_zvyh_0, _zvyh_1)  ;  y -> b  ;  ys -> nil2
}


-------------------------------------------
Step 7, which took 0.170863 s (model generation: 0.170498,  model checking: 0.000365):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, cons2(x_1_0, x_1_1), pair2(x_2_0, x_2_1)) <= _r_2(x_2_1)
  _r_1(a, nil2, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0)
  _r_1(b, nil2, pair2(x_2_0, x_2_1)) <= True
  _r_2(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_1, 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x4 -> cons2(_ayyh_0, _ayyh_1)  ;  z -> b
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(_mazh_0, b), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> nil2  ;  y -> a  ;  ys -> nil2
}


-------------------------------------------
Step 8, which took 0.141190 s (model generation: 0.140765,  model checking: 0.000425):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_2(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_1)
  _r_2(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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> nil2  ;  z -> b
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(a, a), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> nil2  ;  y -> a  ;  ys -> nil2
}


-------------------------------------------
Step 9, which took 0.648817 s (model generation: 0.648408,  model checking: 0.000409):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, cons2(x_1_0, x_1_1), pair2(x_2_0, x_2_1)) <= _r_3(x_2_1)
  _r_1(a, nil2, pair2(x_2_0, x_2_1)) <= _r_3(x_2_0)
  _r_1(b, cons2(x_1_0, x_1_1), pair2(x_2_0, x_2_1)) <= True
  _r_1(b, nil2, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0)
  _r_2(b) <= 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_1, 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
Yes: {
_cta -> nil  ;  x2 -> nil2  ;  x3 -> b  ;  x4 -> cons2(_zezh_0, _zezh_1)  ;  z -> a
}

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(b, b), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> nil2  ;  y -> a  ;  ys -> nil2
}


-------------------------------------------
Step 10, which took 0.662862 s (model generation: 0.661951,  model checking: 0.000911):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(a, b), 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, b), 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)) <= _r_2(x_2_1)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= True
  _r_2(b) <= 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) /\ 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(b, b), nil)  ;  _ota -> nil  ;  x -> a  ;  xs -> nil2  ;  y -> b  ;  ys -> nil2
}


-------------------------------------------
Step 11, which took 0.806205 s (model generation: 0.805282,  model checking: 0.000923):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(a, b), 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, b), nil))
}

Current best model:
|_
name: None

zip ->
[
zip : <list2 * list2 * list>
{
  _r_1(a, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_2(x_2_1)
  _r_1(a, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= True
  _r_2(a) <= True
  _r_3(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(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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(_kyzh_0, a), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> nil2  ;  y -> b  ;  ys -> nil2
}


-------------------------------------------
Step 12, which took 0.783918 s (model generation: 0.782945,  model checking: 0.000973):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(a, b), 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), 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)) <= _r_3(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_1)
  _r_2(b) <= 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) /\ 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(a, b), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> cons2(_zhai_0, _zhai_1)  ;  y -> b  ;  ys -> nil2
}


-------------------------------------------
Step 13, which took 0.926028 s (model generation: 0.925117,  model checking: 0.000911):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(a, b), 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), 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)) <= _r_3(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0)
  _r_2(b) <= 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) /\ 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(b, a), nil)  ;  _ota -> nil  ;  x -> b  ;  xs -> nil2  ;  y -> b  ;  ys -> nil2
}


-------------------------------------------
Step 14, which took 0.781151 s (model generation: 0.780202,  model checking: 0.000949):

Clauses:
{
zip(cons2(z, x2), nil2, nil) <= True -> 0
zip(nil2, y, nil) <= True -> 0
zip(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta) -> 0
eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta) -> 0
}

Accumulated learning constraints:
{
zip(cons2(a, nil2), cons2(a, 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, cons2(a, nil2)), cons(pair2(a, b), 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, cons2(a, nil2)), cons(pair2(b, a), 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
False <= zip(cons2(a, cons2(a, nil2)), cons2(a, cons2(a, nil2)), cons(pair2(a, a), nil))
False <= zip(cons2(a, cons2(a, nil2)), cons2(b, nil2), cons(pair2(b, a), nil))
False <= zip(cons2(a, nil2), cons2(a, cons2(a, nil2)), cons(pair2(a, b), 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), nil))
False <= zip(cons2(a, nil2), cons2(b, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, cons2(a, nil2)), cons2(b, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(a, b), nil))
False <= zip(cons2(b, nil2), cons2(a, nil2), cons(pair2(b, b), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(a, a), nil))
False <= zip(cons2(b, nil2), cons2(b, nil2), cons(pair2(b, 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)) <= _r_3(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_2(x_2_1)
  _r_2(b) <= 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) /\ 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
}
]



--
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(cons2(z, x2), cons2(x3, x4), cons(pair2(z, x3), _cta)) <= zip(x2, x4, _cta)  :
No: ()

eq_list(_nta, cons(pair2(x, y), _ota)) <= zip(xs, ys, _ota) /\ zip(cons2(x, xs), cons2(y, ys), _nta)  :
Yes: {
_nta -> cons(pair2(a, a), nil)  ;  _ota -> nil  ;  x -> a  ;  xs -> nil2  ;  y -> b  ;  ys -> cons2(_chbi_0, _chbi_1)
}


Total time: 5.821995
Learner time: 5.113737
Teacher time: 0.007631
Reasons for stopping: Yes: |_
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)) <= _r_2(x_2_1) /\ _r_3(x_2_0)
  _r_1(b, a, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_2_1)
  _r_1(b, b, pair2(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_2(x_2_1)
  _r_2(b) <= 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) /\ 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
}
]



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