Consider the following premises. Q(a_12) -> u. w -> u. forall y: Q(y). Can we infer ~u from them? If possible, name the inference rules being used at each step.
 From forall y: Q(y) we can infer Q(a_12) via universal instantiation. From Q(a_12) we can infer Q(a_12) or w via addition. Finally, from Q(a_12) -> u, w -> u, Q(a_12) or w we can infer u via disjunction elimination, which contradicts ~u. Therefore, the answer is no.