% -------------------------------------------------------------
% resolve(+A,+B,-R)
% succeeds if R is a resolvent of clauses A and B

resolve(A,B,Resolvent) :- 
  ( select(-L,A,RestA), 
    select(L,B,RestB)
    ;
    select(-L,B,RestB), 
    select(L,A,RestA)
  ),
  append(RestA,RestB,Resolvent).


% -------------------------------------------------------------
% unsat(+Clauses)
% succeeds is Clauses is an unsatisfiable clause set

unsat(Clauses) :-
  member([],Clauses),write(Clauses),nl.

unsat(Clauses) :-                               write(Clauses),nl,nl,
  findall(Res, ( member(C1,Clauses),
		 member(C2,Clauses),
		 C1 @< C2,                      % avoid symmetry
		 resolve(C1,C2,ResTmp),
		 sort(ResTmp,Res),              % ensure clause is a set
		 \+member(Res,Clauses)          % poor man's subsumption
	       ),
          AllRes),
  AllRes \= [],                                 % termination if nothing new
  sort(AllRes,AllRes2),                         % remove duplicates 
  append(Clauses,AllRes2,NewClauses),
  unsat(NewClauses).



% ====================================================
% TESTS

test1 :- unsat([[p,-p],[-p,p]]).

test2 :- unsat([[p,q],[-p,q],[-q,p],[-p,-q]]).

% Pigeon hole n=2
test3 :- unsat([[-p1h1,-p2h1],[-p1h1,-p3h1],[-p2h1,-p3h1],
                [-p1h2,-p2h2],[-p1h2,-p3h2],[-p2h2,-p3h2],
                [p1h1,p1h2],
                [p2h1,p2h2],
                [p3h1,p3h2]]).