% Source: http://www.cs.kuleuven.ac.be/~dtai/prototypes/dppd/model_elim.html
solve((G1,G2),[]) :- solve(G1,[]),solve(G2,[]).

solve(G,A) :- 
        prove(G,A).

prove(G,A) :-
	member(G,A).
prove(G,A) :- neg(G,GN),
        contrapositive((GN:-B)),
        proveall(B,[GN|A]).

proveall([],_).
proveall([G|R],A) :- prove(G,A),
        proveall(R,A).

contrapositive((G:-B)) :- input_clause(_,_,[G|B]).
contrapositive((G:-[B|Bs1])) :- input_clause(_,_,[B|Bs]),
        contrapositive1(G,Bs,Bs1). 

contrapositive1(G,[G|Xs],Xs).
contrapositive1(G,[X|Xs],[X|Xs1]) :- contrapositive1(G,Xs,Xs1).

member(X,[X|_]).
member(X,[_|Xs]) :- member(X,Xs).

neg(neg(F),pos(F)).
neg(pos(F),neg(F)).

input_clause(app1,axiom,
    [pos(app([],L,L))]).

input_clause(app2,axiom,
    [pos(app([H|X],Y,[H|Z])),
     neg(app(X,Y,Z))]).

input_clause(testp1,axiom,
    [pos(q(X)),
     neg(p(X))]).
input_clause(testp2,axiom,
    [pos(p(X)),
     pos(q(a)),
     pos(q(b))]).