Solving ../../benchmarks/smtlib/true/fst_nlist.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}  ;  nat -> {s, z}  ;  nlist -> {ncons, nnil}  ;  nlpair -> {nlpair}
}
definition:
{
(fst_nlist, F:
{
fst_nlist(nlpair(l1, l2), l1) <= True
}
eq_nlist(_bd, _cd) <= fst_nlist(_ad, _bd) /\ fst_nlist(_ad, _cd)
)
}

properties:
{
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)
}


over-approximation: {fst_nlist}
under-approximation: {}

Clause system for inference is:

{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}


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

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_4(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(s(x_0_0), z) <= _r_5(x_0_0)
  _r_4(nnil) <= True
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005671 s (model generation: 0.005642,  model checking: 0.000029):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> nnil
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
No: ()


-------------------------------------------
Step 1, which took 0.006129 s (model generation: 0.006089,  model checking: 0.000040):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(nnil, nnil), nnil) <= True
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= True
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(_pyle_0, _pyle_1)
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> nnil  ;  l1 -> ncons(_ryle_0, _ryle_1)
}


-------------------------------------------
Step 2, which took 0.010268 s (model generation: 0.010219,  model checking: 0.000049):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(nnil) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_1(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(_xyle_0, _xyle_1)  ;  l1 -> nnil
}


-------------------------------------------
Step 3, which took 0.013757 s (model generation: 0.013598,  model checking: 0.000159):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(nnil) <= True
  _r_2(ncons(x_0_0, x_0_1)) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_1(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(_fzle_0, ncons(_qzle_0, _qzle_1))  ;  l1 -> ncons(_gzle_0, nnil)
}


-------------------------------------------
Step 4, which took 0.014778 s (model generation: 0.014693,  model checking: 0.000085):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), nnil) <= True
  _r_2(nnil) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_2(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(_tzle_0, ncons(_dame_0, _dame_1))
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(_xzle_0, nnil)  ;  l1 -> ncons(_yzle_0, ncons(_eame_0, _eame_1))
}


-------------------------------------------
Step 5, which took 0.021463 s (model generation: 0.021307,  model checking: 0.000156):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_2(x_0_1)
  _r_2(nnil) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_2(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(_kame_0, ncons(s(_obme_0), nnil))  ;  l1 -> ncons(_lame_0, ncons(z, nnil))
}


-------------------------------------------
Step 6, which took 0.041007 s (model generation: 0.040843,  model checking: 0.000164):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_3(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), z) <= True
  _r_3(nnil) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(_xbme_0, ncons(s(_jcme_0), _hcme_1))
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(s(_xcme_0), ncons(z, _wcme_1))  ;  l1 -> ncons(z, ncons(_kdme_0, _kdme_1))
}


-------------------------------------------
Step 7, which took 0.190843 s (model generation: 0.190457,  model checking: 0.000386):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_3(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= True
  _r_3(nnil) <= True
  _r_4(s(x_0_0)) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(z, ncons(z, _gfme_1))  ;  l1 -> ncons(s(_ffme_0), ncons(_tfme_0, _tfme_1))
}


-------------------------------------------
Step 8, which took 0.202946 s (model generation: 0.202679,  model checking: 0.000267):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1)
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_2(x_0_1)
  _r_2(ncons(x_0_0, x_0_1)) <= _r_4(x_0_0)
  _r_2(nnil) <= True
  _r_3(z) <= True
  _r_4(s(x_0_0)) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_2(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(s(_ngme_0), _wfme_1)
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> nnil  ;  l1 -> ncons(s(_dhme_0), _fgme_1)
}


-------------------------------------------
Step 9, which took 0.660082 s (model generation: 0.659642,  model checking: 0.000440):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(s(z), nnil)) <= True
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), nnil)
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_3(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_3(nnil) <= True
  _r_4(s(x_0_0)) <= True
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(s(s(_tjme_0)), ncons(z, _uime_1))  ;  l1 -> ncons(s(z), ncons(z, _njme_1))
}


-------------------------------------------
Step 10, which took 0.672197 s (model generation: 0.671757,  model checking: 0.000440):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(s(z), nnil)) <= True
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(s(s(z)), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), nnil)
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0) /\ _r_3(x_0_0, x_1_1)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_5(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0, x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= True
  _r_3(z, nnil) <= True
  _r_4(s(x_0_0), z) <= True
  _r_5(nnil) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_5(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(z, ncons(_ikme_0, ncons(_olme_0, _olme_1)))
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(z, nnil)  ;  l1 -> ncons(s(_imme_0), nnil)
}


-------------------------------------------
Step 11, which took 1.420724 s (model generation: 1.420290,  model checking: 0.000434):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(s(z), nnil)) <= True
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, ncons(z, nnil))), nnil), ncons(z, ncons(z, ncons(z, nnil)))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(s(s(z)), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), nnil)
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_4(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_3(s(x_0_0), z) <= True
  _r_4(nnil) <= True
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(s(s(_eome_0)), _smme_1)
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(s(z), nnil)  ;  l1 -> ncons(s(s(_fpme_0)), nnil)
}


-------------------------------------------
Step 12, which took 1.612769 s (model generation: 1.612058,  model checking: 0.000711):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(s(s(z)), nnil), nnil), ncons(s(s(z)), nnil)) <= True
fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(s(z), nnil)) <= True
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, ncons(z, nnil))), nnil), ncons(z, ncons(z, ncons(z, nnil)))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(s(z)), nnil), nnil), ncons(s(z), nnil))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(s(s(z)), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), nnil)
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_3(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0) /\ _r_5(x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_2(nnil, s(x_1_0)) <= _r_4(x_1_0)
  _r_3(nnil) <= True
  _r_4(s(x_0_0)) <= _r_5(x_0_0)
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1, x_1_0) /\ _r_3(x_1_1)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_3(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
Yes: {
l1 -> ncons(s(s(_ftme_0)), ncons(_rrme_0, _rrme_1))
}

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(z, ncons(s(s(z)), _pume_1))  ;  l1 -> ncons(z, nnil)
}


-------------------------------------------
Step 13, which took 4.039040 s (model generation: 4.038473,  model checking: 0.000567):

Clauses:
{
fst_nlist(nlpair(l1, l2), l1) <= True -> 0
eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd) -> 0
}

Accumulated learning constraints:
{
fst_nlist(nlpair(ncons(s(s(z)), ncons(z, nnil)), nnil), ncons(s(s(z)), ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(s(s(z)), nnil), nnil), ncons(s(s(z)), nnil)) <= True
fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(s(z), nnil)) <= True
fst_nlist(nlpair(ncons(z, ncons(s(z), nnil)), nnil), ncons(z, ncons(s(z), nnil))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, ncons(z, nnil))), nnil), ncons(z, ncons(z, ncons(z, nnil)))) <= True
fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil))) <= True
fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, nnil)) <= True
fst_nlist(nlpair(nnil, nnil), nnil) <= True
False <= fst_nlist(nlpair(ncons(s(s(z)), nnil), nnil), ncons(s(z), nnil))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(s(s(z)), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), ncons(z, nnil)), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(s(z), nnil), nnil), nnil)
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(s(z), ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, ncons(s(z), nnil)))
False <= fst_nlist(nlpair(ncons(z, ncons(z, nnil)), nnil), ncons(z, nnil))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(s(s(z)), nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), ncons(z, ncons(z, nnil)))
False <= fst_nlist(nlpair(ncons(z, nnil), nnil), nnil)
False <= fst_nlist(nlpair(nnil, nnil), ncons(z, nnil))
}

Current best model:
|_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_4(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(s(x_0_0), z) <= _r_5(x_0_0)
  _r_4(nnil) <= True
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|




Answer of teacher:

fst_nlist(nlpair(l1, l2), l1) <= True  :
No: ()

eq_nlist(_dd, l1) <= fst_nlist(nlpair(l1, l2), _dd)  :
Yes: {
_dd -> ncons(z, ncons(z, ncons(_oyme_0, _oyme_1)))  ;  l1 -> ncons(z, ncons(z, nnil))
}


Total time: 12.088388
Learner time: 8.907747
Teacher time: 0.003927
Reasons for stopping: Yes: |_
name: None

fst_nlist ->
[
fst_nlist : <nlpair * nlist>
{
  _r_1(ncons(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1, x_1_0)
  _r_1(ncons(x_0_0, x_0_1), nnil) <= _r_4(x_0_1)
  _r_2(ncons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_2(ncons(x_0_0, x_0_1), z) <= _r_5(x_0_0)
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(s(x_0_0), z) <= _r_5(x_0_0)
  _r_4(nnil) <= True
  _r_5(z) <= True
  fst_nlist(nlpair(x_0_0, x_0_1), ncons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0)
  fst_nlist(nlpair(x_0_0, x_0_1), nnil) <= _r_4(x_0_0)
}
]



--
Equality automata are defined for: {elt, nat, nlist, nlpair}
_|