Consider the following premises. U(a_9) -> t. forall x: U(x) and W(x). Can we infer t from them? If possible, name the inference rules being used at each step.
 From forall x: U(x) and W(x) we can infer forall x: U(x) via universal simplification. From forall x: U(x) we can infer U(a_9) via universal instantiation. Finally, from U(a_9) -> t, U(a_9) we can infer t via modus ponens. Therefore, the answer is yes.