Consider the following premises. r or ~u_4. r_3 -> u_4. r or ~q_2. r_3 or q_2. Can we infer r from them? If possible, name the inference rules being used at each step.
 From r or ~u_4 we can infer u_4 -> r via rewriting. From r_3 -> u_4, u_4 -> r we can infer r_3 -> r via transitivity. From r or ~q_2 we can infer q_2 -> r via rewriting. Finally, from r_3 -> r, q_2 -> r, r_3 or q_2 we can infer r via disjunction elimination. Therefore, the answer is yes.