Apply the Davis Putnam Procedure $($DPP$)$ to determine whether or not the following

argument is valid:

Premise $1$: $(pr)harr(sq)$

Premise $2$: $p^{{?}^{?}}(qvvs)$

Premise $3$: not$(qharrs)$

Conclusion: rharrs

$($a$)$ Use the laws of propositional logic to transform the logical formulas intended as in$-$

put to resolution into conjunctive normal form $($CNF$)($explicitly state each propo$-$

sitional logic law that you use$).$ Convert all obtained CNF formulas into clauses, in

DPP format.

$($b$)$ Eliminate the variables in the order p$,$ q$,$ r$,$ s$.$ At each iteration step i$,$ number the

parent clauses and, for each resolvent, explicitly indicate its parent clauses. Explic$-$

itly display, for each iteration step $i,$ the sets $S_i^{\text{'}},T_i,U_i$ and $S_{i+1}.$

$($c$)$ Interpret the outcome of DPP$,$ to determine whether the provided argument is valid

or not. Justify your answer.