Consider the following premises. q -> T(a_5). forall y_2: T(y_2) -> ~U_3(y_2). forall y_2: U_3(y_2). Can we infer q from them? If possible, name the inference rules being used at each step.
 From forall y_2: T(y_2) -> ~U_3(y_2), forall y_2: U_3(y_2) we can infer forall y_2: ~T(y_2) via universal modus tollens. From forall y_2: ~T(y_2) we can infer ~T(a_5) via universal instantiation. Finally, from q -> T(a_5), ~T(a_5) we can infer ~q via modus tollens, which contradicts q. Therefore, the answer is no.