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