Please let Bijan know if there are any typos or other errors. I didn't "show work" here.
Propositional
\(\neg p \rightarrow (\neg q \land (r \land \neg s))\)
\(\{\{\neg p\}, \{q, \neg r, s\}\}\) (remember we negated the above formula!)
There
are no matching literals, thus no applications of the resolution rule.
Thus there is no way to derive the empty clause and this formula is
satisfiable.
We can use tableau either directly on the formulae
or on the negation. Here I'm working directly on the formulae and it's
pretty trivial (implication and double negation elimination is all you
need). \[p \lor (\neg q \land (r \land s))\]
We get a completed branch in one step by applying the OR-rule.