Consider the following premises. w_4 -> s. s_4. ~p_16. p_16 <-> s. Can we infer w_4 from them? If possible, name the inference rules being used at each step.
 From p_16 <-> s, ~p_16 we can infer ~s via biconditional elimination. Finally, from w_4 -> s, ~s we can infer ~w_4 via modus tollens, which contradicts w_4. Therefore, the answer is no.