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