Consider the following premises. ~p. p_17 or w_1. p_17 -> r. s -> p. p -> w_3. w_3 -> s. w_1 -> r. Can we infer ~r from them? If possible, name the inference rules being used at each step.
 From p -> w_3, w_3 -> s we can infer p -> s via transitivity. Finally, from p_17 -> r, w_1 -> r, p_17 or w_1 we can infer r via disjunction elimination, which contradicts ~r. Therefore, the answer is no.