Solving ../../benchmarks/smtlib/false/timbuk_reverseBUGimplies.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}  ;  eltlist -> {cons, nil}
}
definition:
{
(append_bug, F:
{
append_bug(nil, l2, nil) <= True
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)
}
eq_eltlist(_mib, _nib) <= append_bug(_kib, _lib, _mib) /\ append_bug(_kib, _lib, _nib)
)
(reverse, F:
{
reverse(nil, nil) <= True
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)
}
eq_eltlist(_rib, _sib) <= reverse(_qib, _rib) /\ reverse(_qib, _sib)
)
(member, P:
{
member(h1, cons(h1, t1)) <= True
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))
False <= member(e, nil)
}
)
}

properties:
{
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)
}


over-approximation: {append_bug, reverse}
under-approximation: {}

Clause system for inference is:

{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}


Solving took 0.631696 seconds.
No: Contradictory set of ground constraints:
{
append_bug(cons(a, nil), cons(a, nil), cons(a, nil)) <= True
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, cons(b, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(a, cons(b, cons(a, nil))) <= True
member(b, cons(a, cons(a, cons(b, nil)))) <= True
member(b, cons(a, cons(b, nil))) <= True
member(b, cons(b, nil)) <= True
reverse(cons(a, nil), nil) <= True
reverse(nil, nil) <= True
False <= append_bug(nil, cons(b, nil), nil)
False <= member(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), nil)
False <= member(a, cons(b, cons(b, nil)))
False <= member(a, cons(b, nil))
False <= member(a, nil)
False <= member(b, cons(a, cons(a, nil)))
False <= member(b, cons(a, nil))
False <= member(b, nil)
False <= reverse(cons(b, nil), nil)
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005543 s (model generation: 0.005470,  model checking: 0.000073):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  
}
]


;
member ->
[
member : <elt * eltlist>
{
  
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
Yes: {
l2 -> nil
}

member(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> b
}

reverse(nil, nil) <= True  :
Yes: {

}

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
No: ()

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
No: ()

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
No: ()

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
No: ()

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
No: ()

False <= member(e, nil)  :
No: ()


-------------------------------------------
Step 1, which took 0.006482 s (model generation: 0.006323,  model checking: 0.000159):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{
append_bug(nil, nil, nil) <= True
member(b, cons(b, nil)) <= True
reverse(nil, nil) <= True
}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  append_bug(nil, nil, nil) <= True
}
]


;
member ->
[
member : <elt * eltlist>
{
  member(b, cons(x_1_0, x_1_1)) <= True
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
Yes: {
l2 -> cons(_xctqw_0, _xctqw_1)
}

member(h1, cons(h1, t1)) <= True  :
Yes: {
h1 -> a
}

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
No: ()

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
Yes: {
_jib -> nil  ;  l2 -> nil  ;  t1 -> nil
}

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
No: ()

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
No: ()

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
Yes: {
e -> b  ;  h1 -> a  ;  t1 -> nil
}

False <= member(e, nil)  :
No: ()


-------------------------------------------
Step 2, which took 0.008725 s (model generation: 0.008631,  model checking: 0.000094):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(b, cons(b, nil)) <= True
reverse(nil, nil) <= True
member(b, nil) <= member(b, cons(a, nil))
}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  append_bug(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append_bug(nil, cons(x_1_0, x_1_1), nil) <= True
  append_bug(nil, nil, nil) <= True
}
]


;
member ->
[
member : <elt * eltlist>
{
  member(a, cons(x_1_0, x_1_1)) <= True
  member(b, cons(x_1_0, x_1_1)) <= True
  member(b, nil) <= True
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
No: ()

member(h1, cons(h1, t1)) <= True  :
No: ()

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
Yes: {
_oib -> nil  ;  _pib -> nil  ;  t1 -> nil
}

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
Yes: {
_jib -> nil  ;  l2 -> cons(_jdtqw_0, _jdtqw_1)  ;  t1 -> nil
}

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
No: ()

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
No: ()

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
Yes: {
e -> a  ;  h1 -> b  ;  t1 -> nil
}

False <= member(e, nil)  :
Yes: {
e -> b
}


-------------------------------------------
Step 3, which took 0.015406 s (model generation: 0.015275,  model checking: 0.000131):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{
append_bug(cons(a, nil), cons(a, nil), cons(a, nil)) <= True
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(b, cons(b, nil)) <= True
reverse(cons(a, nil), nil) <= True
reverse(nil, nil) <= True
member(a, nil) <= member(a, cons(b, nil))
False <= member(b, cons(a, nil))
False <= member(b, nil)
}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  append_bug(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append_bug(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append_bug(nil, cons(x_1_0, x_1_1), nil) <= True
  append_bug(nil, nil, nil) <= True
}
]


;
member ->
[
member : <elt * eltlist>
{
  _r_1(b) <= True
  member(a, cons(x_1_0, x_1_1)) <= True
  member(a, nil) <= True
  member(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_0)
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  reverse(cons(x_0_0, x_0_1), nil) <= True
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
No: ()

member(h1, cons(h1, t1)) <= True  :
No: ()

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
No: ()

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
No: ()

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
Yes: {
_tib -> nil  ;  e -> b  ;  l1 -> cons(b, _sdtqw_1)
}

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
Yes: {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, _vdtqw_1)
}

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
No: ()

False <= member(e, nil)  :
Yes: {
e -> a
}


-------------------------------------------
Step 4, which took 0.037920 s (model generation: 0.037575,  model checking: 0.000345):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{
append_bug(cons(a, nil), cons(a, nil), cons(a, nil)) <= True
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(b, cons(a, cons(b, nil))) <= True
member(b, cons(b, nil)) <= True
reverse(cons(a, nil), nil) <= True
reverse(nil, nil) <= True
False <= member(a, cons(b, nil))
False <= member(a, nil)
False <= member(b, cons(a, nil))
False <= member(b, nil)
False <= reverse(cons(b, nil), nil)
}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  append_bug(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append_bug(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append_bug(nil, cons(x_1_0, x_1_1), nil) <= True
  append_bug(nil, nil, nil) <= True
}
]


;
member ->
[
member : <elt * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= True
  _r_2(a) <= True
  _r_3(b) <= True
  member(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_0)
  member(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  member(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_2(a) <= True
  reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_0)
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
No: ()

member(h1, cons(h1, t1)) <= True  :
No: ()

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
Yes: {
_oib -> nil  ;  _pib -> nil  ;  h1 -> b  ;  t1 -> nil
}

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
No: ()

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
Yes: {
_tib -> nil  ;  e -> b  ;  l1 -> cons(a, cons(_zftqw_0, _zftqw_1))
}

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
Yes: {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, _yetqw_1)
}

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
Yes: {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, nil)
}

False <= member(e, nil)  :
No: ()


-------------------------------------------
Step 5, which took 0.063445 s (model generation: 0.062864,  model checking: 0.000581):

Clauses:
{
append_bug(nil, l2, nil) <= True -> 0
member(h1, cons(h1, t1)) <= True -> 0
reverse(nil, nil) <= True -> 0
reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib) -> 0
append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib) -> 0
member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib) -> 0
eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1) -> 0
eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1)) -> 0
False <= member(e, nil) -> 0
}

Accumulated learning constraints:
{
append_bug(cons(a, nil), cons(a, nil), cons(a, nil)) <= True
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(a, cons(b, cons(a, nil))) <= True
member(b, cons(a, cons(b, nil))) <= True
member(b, cons(b, nil)) <= True
reverse(cons(a, nil), nil) <= True
reverse(nil, nil) <= True
False <= append_bug(nil, cons(b, nil), nil)
False <= member(a, cons(b, nil))
False <= member(a, nil)
False <= member(b, cons(a, cons(a, nil)))
False <= member(b, cons(a, nil))
False <= member(b, nil)
False <= reverse(cons(b, nil), nil)
}

Current best model:
|_
name: None

append_bug ->
[
append_bug : <eltlist * eltlist * eltlist>
{
  _r_4(a) <= True
  append_bug(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append_bug(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append_bug(nil, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_0)
  append_bug(nil, nil, nil) <= True
}
]


;
member ->
[
member : <elt * eltlist>
{
  _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0)
  _r_2(cons(x_0_0, x_0_1)) <= True
  _r_3(b) <= True
  _r_4(a) <= True
  member(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1)
  member(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0)
  member(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1)
  member(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0)
}
]


;
reverse ->
[
reverse : <eltlist * eltlist>
{
  _r_4(a) <= True
  reverse(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0)
  reverse(nil, nil) <= True
}
]



--
Equality automata are defined for: {elt, eltlist}
_|




Answer of teacher:

append_bug(nil, l2, nil) <= True  :
Yes: {
l2 -> cons(b, _ggtqw_1)
}

member(h1, cons(h1, t1)) <= True  :
No: ()

reverse(nil, nil) <= True  :
No: ()

reverse(cons(h1, t1), _pib) <= append_bug(_oib, cons(h1, nil), _pib) /\ reverse(t1, _oib)  :
No: ()

append_bug(cons(h1, t1), l2, cons(h1, _jib)) <= append_bug(t1, l2, _jib)  :
No: ()

member(e, _tib) <= member(e, l1) /\ reverse(l1, _tib)  :
Yes: {
_tib -> nil  ;  e -> a  ;  l1 -> cons(a, cons(_qitqw_0, _qitqw_1))
}

eq_elt(e, h1) \/ member(e, cons(h1, t1)) <= member(e, t1)  :
Yes: {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(b, _uitqw_1))
}

eq_elt(e, h1) \/ member(e, t1) <= member(e, cons(h1, t1))  :
Yes: {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, nil)
}

False <= member(e, nil)  :
No: ()


Total time: 0.631696
Learner time: 0.136138
Teacher time: 0.001383
Reasons for stopping: No: Contradictory set of ground constraints:
{
append_bug(cons(a, nil), cons(a, nil), cons(a, nil)) <= True
append_bug(cons(a, nil), nil, cons(a, nil)) <= True
append_bug(nil, cons(a, nil), nil) <= True
append_bug(nil, cons(b, nil), nil) <= True
append_bug(nil, nil, nil) <= True
member(a, cons(a, nil)) <= True
member(a, cons(b, cons(a, nil))) <= True
member(b, cons(a, cons(a, cons(b, nil)))) <= True
member(b, cons(a, cons(b, nil))) <= True
member(b, cons(b, nil)) <= True
reverse(cons(a, nil), nil) <= True
reverse(nil, nil) <= True
False <= append_bug(nil, cons(b, nil), nil)
False <= member(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), nil)
False <= member(a, cons(b, cons(b, nil)))
False <= member(a, cons(b, nil))
False <= member(a, nil)
False <= member(b, cons(a, cons(a, nil)))
False <= member(b, cons(a, nil))
False <= member(b, nil)
False <= reverse(cons(b, nil), nil)
}