Consider the following premises. ~q. w <-> u. q or s. ~u. Can we infer ~w and s from them? If possible, name the inference rules being used at each step.
 From w <-> u, ~u we can infer ~w via biconditional elimination. From q or s, ~q we can infer s via disjunctive syllogism. Finally, from ~w, s we can infer ~w and s via conjunction. Therefore, the answer is yes.