Prolog - algoritmo de resolucion (ayuda)

Me estoy volviendo loco con un algoritmo de resolucion (de lógica formal) que tengo que "pasar" a prolog, simplemente no entiende porque me devuelve ciertos datos. Si alguien me puede echar una mano le estaria muy agradecido

La estructura elegida para representar las clausulas es: [[clausula],[clausula2],...,[clausulan]], y cada clausula es otra lista con atomos del estilo a o neg a

ejemplo= [[a, b],[b, c, neg d],[d, neg a, neg b],[neg c],[d, a, b, c]]

El programa es algo como lo que sigue

"clashing(C1,C2):-
member(L,C1), member(neg L,C2).

%Es verdadero cuando las dos clausulas que se le pasan tienen miembros contradictorios, es decir, una tiene a y la otra neg a entre sus componentes

conseguir_resolvente(S,[R3|S3]):-
member(C1,S),member(C2,S),
clashing(C1,C2),
append(C1,C2,R1),
limpiar_complementarios(R1,R2),
limpiar_repetidos(R2,R3),
sacar(C1,S,S2),sacar(C2,S2,S3).

%Si la lista de clausulas tiene dos clausulas con literales contradictorios, consigue una resolvente que se obtiene uniendo los miembros de las dos clausulas en una tercera, eliminando contradictorios y repetidos. Además, las dos clausulas contradictorias se eliminan, y la tercera se introduce en la lista

%limpiar_complementarios: Se carga todos las "contradicciones" de la clausula, es decir, si hay un a y un neg a en la clausula, se carga todos los a y neg a que aparezcan en ella

%limpiar_repetidos: Se carga todos los literales repetidos que haya en la clausula

%Sacar: Saca la clausula de la lista

resolve_set(S):-member([],S).

%Si hay una clausula vacia en la lista, se ha descubierto que el conjunto de clausulas NO tiene solucion y se responde SI

resolve_set(S):-
conseguir_resolvente(S,S2),
resolve_set(S2).

%Si no hay clausulas vacias en la lista, se intenta conseguir una resolvente, y una vez conseguida, se añade a la lista, y se sacan las dos contradictorias. Despues se vuelve a empezar. Si no hay clausulas contradictorias, se devuelve No"

Se que no es el algoritmo de resolución exactamente, ya que en el original no se eliminan las clausulas contradictorias de la lista asi como así, pero eso me encargare de hacerlo despues

El caso es que, en la teoria, cuando le pase una lista de clausulas, iria encontrando resolventes hasta que ya no haya clausulas contradictorias, momento en el que devolvería no (ya que la función conseguir_resolvente fallaría, por tanto resolve_set también). En el caso de que en algun momento se llegara a la clausula vacía ([]), devolvería yes. Pero en la práctica no me ha salido así. Funciona cuando le paso, por ejemplo
-[[a]]: devuelve no
-[[a],[neg a]]: devuelve si
-[[a],[b]]: devuelve no
-[[a],[b],[c,d]]: devuelve no
-[[neg a, b],[neg b, c],[neg c, a]]: devuelve si

y en general, siempre que se llegue a la clausula vacia, funciona. El problema esta cuando le paso algo como lo siguiente

resolve_set([[b,c],[a,neg b],[neg a],[neg c, a]])

En ese momento, le entra la locura y se va a calculos infinitos que no vienen al cuento

Y lo mejor de todo es que, intentandolo paso por paso (es decir, aplicando yo mismo manualmente el procedimiento que segun la teoria debería seguir el programa), el programa funciona...

(al aplicar resolve_set, no concuerda con la primera definicion, ya que no hay listas vacias, asi que pasa a la segunda)

conseguir_resolvente([[b,c],[a,neg b],[neg a],[neg c, a]], R)
R=[[c,a],[neg a],[neg c,a]]

(de nuevo, al aplicar resolve set sobre R, no tiene listas vacias, asi que...)

conseguir_resolvente([[c,a],[neg a],[neg c,a]],R)
R=[[c],[neg c, a]]

conseguir_resolvente([[c],[neg c, a]],R)
R=[[a]]

(de nuevo, se que el verdadero proceso de resolucion no daría eso, pero es un problema que arreglare cuando arregle este)

(Este ultimo R, no tiene listas vacias, pero tampoco clausulas contradictorias, así que no concuerda con ninguno de los dos.Al aplicarlo, falla, por tanto, todo el proceso debería fallar)

Como veis, por pasos, el proceso debería fallar al final, y devolver no. Pero cuando no se hace paso por paso, es decir, cuando aplico directamente resolve_set sobre el conjunto inicial, le entra la locura, y puedes esperar sentado...

Alguna idea???

Gracias de antemano