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