Consider the following premises. ~w_3 -> u. ~s. u -> r_1. w_3 -> s. Can we infer ~r_1 from them? If possible, name the inference rules being used at each step.
 From w_3 -> s, ~s we can infer ~w_3 via modus tollens. From ~w_3 -> u, u -> r_1 we can infer ~w_3 -> r_1 via transitivity. Finally, from ~w_3 -> r_1, ~w_3 we can infer r_1 via modus ponens, which contradicts ~r_1. Therefore, the answer is no.