Solving ../../benchmarks/smtlib/true/fst_elist.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: {
elist -> {econs, enil}  ;  elpair -> {elpair}  ;  elt -> {a, b}  ;  nat -> {s, z}
}
definition:
{
(fst_elist, F:
{
fst_elist(elpair(l1, l2), l1) <= True
}
eq_elist(_rr, _sr) <= fst_elist(_qr, _rr) /\ fst_elist(_qr, _sr)
)
}

properties:
{
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)
}


over-approximation: {fst_elist}
under-approximation: {}

Clause system for inference is:

{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}


Solving took 4.802030 seconds.
Yes: |_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_4(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_3(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_1, x_1_1)
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_1)
  _r_3(b) <= True
  _r_4(a) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006140 s (model generation: 0.006094,  model checking: 0.000046):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> enil
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
No: ()


-------------------------------------------
Step 1, which took 0.005925 s (model generation: 0.005848,  model checking: 0.000077):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(enil, enil), enil) <= True
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  fst_elist(elpair(x_0_0, x_0_1), enil) <= True
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(_able_0, _able_1)
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> enil  ;  l1 -> econs(_cble_0, _cble_1)
}


-------------------------------------------
Step 2, which took 0.009710 s (model generation: 0.009653,  model checking: 0.000057):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), enil)
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= True
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_1(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(_ible_0, _ible_1)  ;  l1 -> enil
}


-------------------------------------------
Step 3, which took 0.013986 s (model generation: 0.013905,  model checking: 0.000081):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(enil) <= True
  _r_2(econs(x_0_0, x_0_1)) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_2(x_0_0)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_1(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(a, _qble_1)  ;  l1 -> econs(b, _rble_1)
}


-------------------------------------------
Step 4, which took 0.022194 s (model generation: 0.022070,  model checking: 0.000124):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(a) <= True
  _r_2(econs(x_0_0, x_0_1)) <= _r_1(x_0_0)
  _r_3(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_2(x_0_0)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(b, _acle_1)
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(_ccle_0, econs(_ucle_0, _ucle_1))  ;  l1 -> econs(a, enil)
}


-------------------------------------------
Step 5, which took 0.031781 s (model generation: 0.031665,  model checking: 0.000116):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_2(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= True
  _r_2(a) <= True
  _r_3(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(_zcle_0, econs(_kdle_0, _kdle_1))
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(b, enil)  ;  l1 -> econs(a, _edle_1)
}


-------------------------------------------
Step 6, which took 0.097333 s (model generation: 0.096621,  model checking: 0.000712):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(econs(x_0_0, x_0_1), enil) <= _r_2(x_0_0)
  _r_2(a) <= True
  _r_3(b) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_3(x_0_0)
  _r_4(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_0)
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(a, econs(b, enil))
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> enil  ;  l1 -> econs(b, _iele_1)
}


-------------------------------------------
Step 7, which took 0.401221 s (model generation: 0.400948,  model checking: 0.000273):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_3(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_2(x_0_0)
  _r_2(b) <= True
  _r_3(a) <= True
  _r_4(econs(x_0_0, x_0_1)) <= _r_5(x_0_1)
  _r_4(enil) <= True
  _r_5(econs(x_0_0, x_0_1)) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_0)
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> enil  ;  l1 -> econs(_ofle_0, econs(_egle_0, _egle_1))
}


-------------------------------------------
Step 8, which took 0.393750 s (model generation: 0.393504,  model checking: 0.000246):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), enil)
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_4(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_3(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0)
  _r_2(econs(x_0_0, x_0_1), enil) <= True
  _r_3(b) <= True
  _r_4(a) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(b, enil)  ;  l1 -> econs(b, econs(_file_0, _file_1))
}


-------------------------------------------
Step 9, which took 0.412666 s (model generation: 0.412185,  model checking: 0.000481):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), enil)
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, econs(a, enil)), enil), econs(b, enil))
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_4(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_3(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0)
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_1)
  _r_3(b) <= True
  _r_4(a) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(a, econs(b, econs(_nlle_0, _nlle_1)))  ;  l1 -> econs(a, econs(b, enil))
}


-------------------------------------------
Step 10, which took 0.560090 s (model generation: 0.559770,  model checking: 0.000320):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), enil)
False <= fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, econs(a, enil))))
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, econs(a, enil)), enil), econs(b, enil))
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_3(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_4(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_1)
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_1)
  _r_3(a) <= True
  _r_4(b) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
No: ()

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(b, econs(a, enil))  ;  l1 -> econs(b, econs(b, enil))
}


-------------------------------------------
Step 11, which took 0.495817 s (model generation: 0.495514,  model checking: 0.000303):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), enil)
False <= fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, econs(a, enil))))
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, econs(a, enil)), enil), econs(b, enil))
False <= fst_elist(elpair(econs(b, econs(b, enil)), enil), econs(b, econs(a, enil)))
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_3(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_4(x_0_0) /\ _r_5(x_0_1)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_1)
  _r_2(econs(x_0_0, x_0_1), enil) <= True
  _r_3(a) <= True
  _r_4(b) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(b, econs(_ople_0, _ople_1))
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(a, enil)  ;  l1 -> econs(a, econs(_zple_0, _zple_1))
}


-------------------------------------------
Step 12, which took 0.829146 s (model generation: 0.828624,  model checking: 0.000522):

Clauses:
{
fst_elist(elpair(l1, l2), l1) <= True -> 0
eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr) -> 0
}

Accumulated learning constraints:
{
fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, econs(a, enil))) <= True
fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, enil))) <= True
fst_elist(elpair(econs(a, enil), enil), econs(a, enil)) <= True
fst_elist(elpair(econs(b, econs(a, enil)), enil), econs(b, econs(a, enil))) <= True
fst_elist(elpair(econs(b, enil), enil), econs(b, enil)) <= True
fst_elist(elpair(enil, enil), enil) <= True
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), econs(a, enil))
False <= fst_elist(elpair(econs(a, econs(a, enil)), enil), enil)
False <= fst_elist(elpair(econs(a, econs(b, enil)), enil), econs(a, econs(b, econs(a, enil))))
False <= fst_elist(elpair(econs(a, enil), enil), econs(a, econs(a, enil)))
False <= fst_elist(elpair(econs(a, enil), enil), econs(b, enil))
False <= fst_elist(elpair(econs(a, enil), enil), enil)
False <= fst_elist(elpair(econs(b, econs(a, enil)), enil), econs(b, enil))
False <= fst_elist(elpair(econs(b, econs(b, enil)), enil), econs(b, econs(a, enil)))
False <= fst_elist(elpair(econs(b, enil), enil), econs(a, enil))
False <= fst_elist(elpair(econs(b, enil), enil), enil)
False <= fst_elist(elpair(enil, enil), econs(a, enil))
}

Current best model:
|_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_3(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_4(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_5(x_1_1)
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_1)
  _r_3(a) <= True
  _r_4(b) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|




Answer of teacher:

fst_elist(elpair(l1, l2), l1) <= True  :
Yes: {
l1 -> econs(_qqle_0, econs(_drle_0, econs(_vrle_0, _vrle_1)))
}

eq_elist(_tr, l1) <= fst_elist(elpair(l1, l2), _tr)  :
Yes: {
_tr -> econs(a, econs(b, enil))  ;  l1 -> econs(a, econs(b, econs(_etle_0, _etle_1)))
}


Total time: 4.802030
Learner time: 3.276401
Teacher time: 0.003358
Reasons for stopping: Yes: |_
name: None

fst_elist ->
[
fst_elist : <elpair * elist>
{
  _r_1(econs(x_0_0, x_0_1), a) <= _r_4(x_0_0)
  _r_1(econs(x_0_0, x_0_1), b) <= _r_3(x_0_0)
  _r_2(econs(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_1, x_1_1)
  _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_1)
  _r_3(b) <= True
  _r_4(a) <= True
  _r_5(enil) <= True
  fst_elist(elpair(x_0_0, x_0_1), econs(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_1_1)
  fst_elist(elpair(x_0_0, x_0_1), enil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elist, elpair, elt, nat}
_|