Consider the following premises. t -> r_1. p_4 -> r_17. w -> r_17. p_4 or w. t. Can we infer ~r_1 from them? If possible, name the inference rules being used at each step.
 From p_4 -> r_17, w -> r_17, p_4 or w we can infer r_17 via disjunction elimination. Finally, from t -> r_1, t we can infer r_1 via modus ponens, which contradicts ~r_1. Therefore, the answer is no.