Consider the following premises. u_3 <-> u. ~u. u_3 or r. Can we infer q_1 or r from them? If possible, name the inference rules being used at each step.
 From u_3 <-> u, ~u we can infer ~u_3 via biconditional elimination. From ~u_3 we can infer ~u_3 or q_1 via addition. Finally, from ~u_3 or q_1, u_3 or r we can infer q_1 or r via resolution. Therefore, the answer is yes.