Consider the following premises. forall x_4: P_4(x_4). P_4(a_3) -> p_2. Q_4(a_3) -> p_2. Can we infer ~p_2 from them?
 From forall x_4: P_4(x_4) we can infer forall x_4: P_4(x_4) or Q_4(x_4). From forall x_4: P_4(x_4) or Q_4(x_4) we can infer P_4(a_3) or Q_4(a_3). Finally, from P_4(a_3) -> p_2, Q_4(a_3) -> p_2, P_4(a_3) or Q_4(a_3) we can infer p_2, which contradicts ~p_2. Therefore, the answer is no.