Consider the following premises. forall y_2: U(y_2). u or r. p -> w_4. r -> w_4. ~u or p. Can we infer U(f_3) and w_4 from them? If possible, name the inference rules being used at each step.
 From u or r, ~u or p we can infer r or p via resolution. From r -> w_4, p -> w_4, r or p we can infer w_4 via disjunction elimination. From forall y_2: U(y_2) we can infer U(f_3) via universal instantiation. Finally, from U(f_3), w_4 we can infer U(f_3) and w_4 via conjunction. Therefore, the answer is yes.