Consider the following premises. w_1 -> r_4. t. s -> ~t. r_4 -> s. Can we infer ~w_1 from them? If possible, name the inference rules being used at each step.
 From s -> ~t, t we can infer ~s via modus tollens. From r_4 -> s, ~s we can infer ~r_4 via modus tollens. Finally, from w_1 -> r_4, ~r_4 we can infer ~w_1 via modus tollens. Therefore, the answer is yes.