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