Infinite recursion when trying to build a resolution solver in prolog in prolog

Question

I am trying to build a resolution solver in prolog. My program works fine when I use primary connectives, but there is infinite recursion when I try to add secondary connectives(equivalence, not equivalence). To be more specific when I run:

clauseform(a equiv b, L).

I get:

L = [[neg a, b], [neg b, a]] 

But when I run:

test(a equiv b).

program enters into infinite recursion.

This is what I have:

?-op(140, fy, neg).
?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow, notimp, notrevimp]).
?-op(180, xfy, [equiv, notequiv]).

/* member(Item, List) :- Item occurs in List */
member(X, [X | _]).
member(X, [_ | Tail]) :- member(X, Tail). 

/* remove(Item, List, Newlist) :- Newlist is the result of removing all occurences 
                                  of Item from List */

remove(_, [], []).
remove(X, [X | Tail], Newtail) :- remove(X, Tail, Newtail).
remove(X, [Head | Tail], [Head | Newtail]) :- remove(X, Tail, Newtail). 

/* conjunctive(X)  :- X is an alpha formula. */

conjunctive(_ and _).
conjunctive(neg(_ or _ )).
conjunctive(neg(_ imp _)).
conjunctive(neg(_ revimp _)).
conjunctive(neg(_ uparrow _)).
conjunctive(_ downarrow _).
conjunctive(_ notimp _).
conjunctive(_ notrevimp _).
conjunctive(_ equiv _).
conjunctive(neg(_ notequiv _)).

/* disjunctive(X) :- X is a beta formula */

disjunctive(neg(_ and _)).
disjunctive(_ or _).
disjunctive(_ imp _).
disjunctive(_ revimp _).
disjunctive(_ uparrow _).
disjunctive(neg(_ downarrow _)).
disjunctive(neg(_ notimp _)).
disjunctive(neg(_ notrevimp _)).
disjunctive(neg(_ equiv _)).
disjunctive(_ notequiv _).

/* unary(X) :- X is a double negation, or a negated constant */

unary(neg neg _).
unary(neg true).
unary(neg false).

/* components(X, Y, Z) :- Y and Z are the components of the formula X,
                          as defined in the alpha and beta table. */

components(X and Y, X, Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y, X, Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X revimp Y, X, neg Y).
components(neg(X revimp Y), neg X, Y).
components(X uparrow Y, neg X, neg Y).
components(neg(X uparrow Y), X, Y).
components(X downarrow Y,neg X, neg Y).
components(neg(X downarrow Y), X, Y).
components(X notimp Y, X, neg Y).
components(neg(X notimp Y), neg X, Y).
components(X notrevimp Y, neg X, Y).
components(neg(X notrevimp Y), X , neg Y).
components(X equiv Y, X imp Y, Y imp X).
components(neg(X equiv Y), neg(X imp Y), neg(Y imp X)).
components(X notequiv Y, neg(X imp Y), neg(Y imp X)).
components(neg(X notequiv Y), X imp Y, Y imp X). 

/* component(X, Y) :- Y is the component of the unary formula X. */

component(neg neg X, X).
component(neg true, false).
component(neg false, true).

resolve(neg neg X, X).
resolve(X, X).


/* singlestep(Old, New) :- New is the result of applying a single step of the 
                           expansion process to Old, which is a generalized 
                           conjunction of generalized disjunctions. */

resolutionstep([Disjunction | Rest], New) :- 
    member(Formula, Disjunction),
    unary(Formula),
    component(Formula, Newformula),
    remove(Formula, Disjunction, Temporary),
    Newdisjunction = [Newformula | Temporary],
    New = [Newdisjunction | Rest].

resolutionstep([Disjunction | Rest], New) :-
    member(Beta, Disjunction),
    disjunctive(Beta),
    components(Beta, Betaone, Betatwo),
    remove(Beta, Disjunction, Temporary),
    Newdis = [Betaone, Betatwo | Temporary],
    New = [Newdis | Rest].

resolutionstep([Disjunction | Rest], New) :-
    member(Alpha, Disjunction),
    conjunctive(Alpha),
    components(Alpha, Alphaone, Alphatwo),
    remove(Alpha, Disjunction, Temporary),
    Newdisone = [Alphaone | Temporary],
    Newdistwo = [Alphatwo | Temporary],
    New = [Newdisone, Newdistwo | Rest].

resolutionstep([Disjunction | Rest], [Disjunction|Newrest]) :-
    resolutionstep(Rest, Newrest).

/* expand(Old, New) :- New is the result of applying singlestep as many
                       times as possible, starting with Old. */

resolution(Con, Newcon) :- 
    resolutionstep(Con, Temp),
    resolution(Temp, Newcon).

resolution(Con, Con).

/* dualclauseform(X, Y) :- Y is the dual clause form of X. */
/* change later from neg X to X */

clauseform(X, Y) :- resolution([[X]], Y). 

closed([Branch | Rest]) :-
    member(false, Branch),
    closed(Rest). 

closed([Branch | Rest]) :-
    member(Y, Rest),
    select(X, Branch, B),
    resolve(neg X, L),
    select(L, Y, Y2),
    append(B, Y2, Rest0),
    sort(Rest0, Rs),
    remove(Y, Rest, Rest1),
    append([Rs], Rest1, FRest),
    write('FRest: '), write(FRest), nl,
    sort(FRest, Result),
    write('Resul: '), write(Result), nl,
    closed(Result).

closed([[]]).

/* if_then_else(P, Q, R) :- either P and Q, or not P and R */
if_then_else(P, Q, _) :- P, !, Q.

if_then_else(_, _, R) :- R.

test(X) :-
    resolution([[neg X]], Y),
    if_then_else(closed(Y), yes, no).

yes :- write('YES'), nl.

no :- write('NO'), nl.

I am suspecting that the problem is in this block of code:

closed([Branch | Rest]) :-
        member(Y, Rest),
        select(X, Branch, B),
        resolve(neg X, L),
        select(L, Y, Y2),
        append(B, Y2, Rest0),
        sort(Rest0, Rs),
        remove(Y, Rest, Rest1),
        append([Rs], Rest1, FRest),
        write('FRest: '), write(FRest), nl,
        sort(FRest, Result),
        write('Resul: '), write(Result), nl,
        closed(Result).

How can I fix it?