Will this be a correct way in using the Davis Putnam Procedure in Propositional Logic? I can't really find much information about this topic, so it is difficult to know if I'm doing this right. Any feedback will be much appreciated. Thanks! 
(¬P → Q) ∧ ((Q ∧ R) → S) ∧ ¬(¬(P → R)) ⊨ S 
Convert to CNF: 
(P v Q) ∧ (¬ (Q ∧ R) v S) ∧  (¬P v ¬R)
(P v Q) ∧ (¬Q v ¬R v S) ∧  (¬P v R)
Negation of Conclusion: ¬S
Convert F to clause form:
F = (P v Q) ∧ (¬Q v ¬R v S) ∧  (¬P v R) ∧ ¬S
≡ {{P, Q}, {¬Q, ¬R, S},  {¬P, R}, {¬S}}
Proof by David-Putnam procedure:
Set of Literals of F = {P, Q, R, S}
By P: New clauses using Resolution on P: {R}
      F = {{P, Q}, {¬Q, ¬R, S},  {¬P, R}, {¬S}, {R}}

      Discard all clauses with P or ¬P in them.

      F = {{¬Q, ¬R, S}, {¬S}, {R}}

By Q: New clauses using Resolution on Q: {¬R v S}
      F = {{P, Q}, {¬Q, ¬R, S},  {¬P, R}, {¬S}, {R}, {¬R v S}}

      Discard all clauses with Q or ¬Q in them.

      F = {{¬P, R}, {¬S}, {R}, {¬R v S}}

By R: New clauses using Resolution on R: {S}
      F = {{¬P, R}, {¬S}, {R}, {¬R v S}, {S}}

      Discard all clauses with R or ¬R in them.

      F = {{¬S}, {S}}

By S: New clauses using Resolution on S: { }
      F = {{¬S}, {S}, { }}

      Discard all clauses with S or ¬S in them.

      F = { }

Are output is the empty clause, so F is unsatisfiable, therefore the Claim is true
 A: See :


*

*Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), Ch.6.2 Davis-Putnam Algorithm, page 115:



Input: A formula $F$ in clausal form.
Output: Report that $F$ is satisfiable or unsatisfiable.
Perform the following rules repeatedly, but the third rule is used only if the first two do not apply:

Unit-literal rule: If there is a unit clause $\{ l \}$, delete all clauses containing $l$ and delete all occurrences of $l^c$ from all other clauses.
Pure-literal rule: If there is a pure literal $l$ [i.e. a literal $l$ that appears in at least one clause of $S$, but its complement $l^c$ does not appear in any clause of $S$], delete all clauses containing $l$.
Eliminate a variable by resolution: Choose an atom $p$ and perform all possible resolutions on clauses that clash on $p$ and $\lnot p$. Add these resolvents to the set of clauses and then delete all clauses containing $p$ or $\lnot p$.

Terminate the algorithm under the following conditions:

If empty clause $\square$ (or: $\{ \}$) is produced, report that the formula is unsatisfiable.
If no more rules are applicable, report that the formula is satisfiable.



We have to apply it to the set $F_0$ of clauses:

$F_0 = \{ \{ P, Q \}, \{ ¬Q, ¬R, S \}, \{ ¬P, R \}, \{¬S \} \}$.

1) Apply Unit-literal rule : delete $\{¬S \}$ and delete all occurences of $S$.
Result: $F_1 = \{ \{ P, Q \}, \{ ¬Q, ¬R, \}, \{ ¬P, R \} \}$.
2) Apply Resolution with $P$. Result: $F_2 = \{ \{ Q, R \}, \{ ¬Q, ¬R, \} \}$.
3) Apply Resolution with $Q$. Result: $F_3 = \{ \{ R, ¬R \} \}$.
No more rules are applicable, and thus the formula $F$ is satisfiable, i.e.:


$(¬P → Q) ∧ ((Q ∧ R) → S) ∧ ¬(¬(P → R)) \nvDash S$.


Check: with a valuation $v$ such that $v(S)=v(Q)=$ f and $v(P)=v(R)=$ t, the premise is t and the conlcusion is f.
