Consider the following premises. forall y: ~U(y). U(a_23) or q_13. ~p_3 -> q. p_3 -> ~q_13. Can we infer ~q from them? If possible, name the inference rules being used at each step.
 From forall y: ~U(y) we can infer ~U(a_23) via universal instantiation. From U(a_23) or q_13, ~U(a_23) we can infer q_13 via disjunctive syllogism. From p_3 -> ~q_13, q_13 we can infer ~p_3 via modus tollens. Finally, from ~p_3 -> q, ~p_3 we can infer q via modus ponens, which contradicts ~q. Therefore, the answer is no.