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