# How to prove this using resolution theorem or resolution refutation?

I need to prove $$\{P \vee (Q \wedge R), S \} \models (S \wedge P) \vee Q$$ using resolution theorem or resolution refutation. This is my proof:

1. Convert $$P \vee (Q \wedge R)$$ to $$(P \vee Q) \wedge (P \wedge R)$$
2. Convert conclusion to $$(S \vee Q ) \wedge (P \vee Q)$$
3. Negate conclusion $$\neg((S \vee Q ) \wedge (P \vee Q))$$
4. De Morgan's law to conclusion $$\neg(S \vee Q) \vee \neg(P \vee Q)$$
5. De Morgan's Law again to conclusion $$(\neg S \wedge \neg Q) \vee (\neg P \wedge \neg Q)$$

After this I am lost what to do next. Can anyone help?

Yes, the conjunctive normal form for $P\vee(Q\wedge R)$ is $(P\vee Q)\wedge (P\vee R)$
The CNF for $S$ is of course, $S$.
And your work at finding the CNF for the negation of the conclusion is okay so far.†   Next distribute $(\neg S \wedge \neg Q) \vee (\neg P \wedge \neg Q)$ to obtain its CNF: $(\neg S\vee \neg P)\wedge\neg Q$.
So you just need to resolve $\{(P,Q),(P,R),S,(\neg S,\neg P),\neg Q\}$ to a contradiction.
$~$
† Though it would have been easier to just negate the DNF into a CNF using de Morgan's rule twice. $\neg((S\wedge P)\vee Q)=(\neg S\vee\neg P)\wedge\neg Q$ with no need to convert, negate, then convert again.