Consider the following premises. q_3 -> ~T_1(a_3). forall z: T_1(z). ~q_3 -> u_3. Can we infer u_3 from them? If possible, name the inference rules being used at each step.
 From forall z: T_1(z) we can infer T_1(a_3) via universal instantiation. From q_3 -> ~T_1(a_3), T_1(a_3) we can infer ~q_3 via modus tollens. Finally, from ~q_3 -> u_3, ~q_3 we can infer u_3 via modus ponens. Therefore, the answer is yes.