1 {~p,r} Premise 2 {~q,r} Premise 3 {~r,p,q} Premise 4 {p,q,r} Premise 5 {~r,~p} Premise 6 {~r,~q} Premise 7 {~p} Resolution 1 5 8 {~q} Resolution 2 6 9 {~r,q} Resolution 3 7 10 {~r} Resolution 9 8 11 {q,r} Resolution 4 7 12 {r} Resolution 11 8 13 {} Resolution 12 10 1 {p,~q} Premise 2 {~p,q} Premise 3 {~r,~q} Premise 4 {r,q} Premise 5 {~r,~s} Premise 6 {s,p} Premise 7 {~p,~q,r} Premise 8 {p,~r} Resolution 6 5 9 {~r,q} Resolution 8 2 10 {q} Resolution 4 9 11 {p} Resolution 10 1 12 {~q,r} Resolution 11 7 13 {r} Resolution 10 12 14 {~q} Resolution 13 3 15 {} Resolution 10 14 1 {p,q} Premise 2 {~p,r} Premise 3 {~p,~r} Premise 4 {p,~q} Premise 5 {p} Resolution 1 4 6 {r} Resolution 5 2 7 {~r} Resolution 5 3 8 {} Resolution 6 7 1 {~p,q} Premise 2 {~r,s} Premise 3 {p,r} Negated Goal 4 {~q} Negated Goal 5 {~s} Negated Goal 6 {~p} Resolution 1 4 7 {~r} Resolution 2 5 8 {r} Resolution 3 6 9 {} Resolution 8 7 1 {p(a),q(a)} Premise 2 {~p(X),r(X)} Premise 3 {~q(X),r(X)} Premise 4 {q(a),r(a)} Resolution 1 2 5 {r(a)} Resolution 4 3 1 {~p(X),q(X)} Premise 2 {~q(X),r(X)} Premise 3 {p(a)} Negated Goal 4 {~r(a)} Negated Goal 5 {q(a)} Resolution 3 1 6 {r(a)} Resolution 5 2 7 {} Resolution 6 4 1 {~p(X),q(X)} Premise 2 {p(X)} Negated Goal 3 {~q(c)} Negated Goal 4 {q(X)} Resolution 2 1 5 {} Resolution 4 3 1 {p(c)} Negated Goal 2 {~q(c),p(c)} Negated Goal 3 {~p(c)} Negated Goal 4 {} Resolution 1 3 1 {~p(X,Y),~p(Y,Z),p(X,Z)} Premise 2 {p(X,a)} Premise 3 {p(a,Y)} Premise 4 {~p(b,c)} Negated Goal 5 {~p(b,V35),~p(V35,c)} Resolution 1 4 6 {~p(a,c)} Resolution 2 5 7 {} Resolution 3 6 1 {~p(X,Y),q(X,Y,f(X,Y))} Premise 2 {~r(Y,Z),q(a,Y,Z)} Premise 3 {r(Y,Z),~q(a,Y,Z)} Premise 4 {p(X,g(X)),q(X,g(X),Z)} Premise 5 {~r(X,Y),~q(X,W,Z)} Premise 6 {~q(a,X,Y),~q(X,W,Z)} Resolution 3 5 7 {q(X,g(X),V34),q(X,g(X),f(X,g(X)))} Resolution 4 1 8 {q(X,g(X),f(X,g(X)))} Factoring 7 9 {~q(a,X,Y)} Resolution 8 6 10 {} Resolution 8 9 1 {p(a)} Premise 2 {~p(X),q(X),r(X)} Premise 3 {~q(X),goal(X)} Premise 4 {~r(X),goal(X)} Premise 5 {q(a),r(a)} Resolution 1 2 6 {r(a),goal(a)} Resolution 5 3 7 {goal(a)} Resolution 6 4 1 {~p,q} Premise 2 {~q,r} Premise 3 {~r} Negated Goal 4 {p} Negated Goal 5 {q} Resolution 4 1 6 {r} Resolution 5 2 7 {} Resolution 6 3