Consider the following premises. q <-> p_2. u -> p_2. q or u. forall x_18: P_18(x_18). Can we infer ~p_2 from them?
 From q <-> p_2 we can infer q -> p_2. From forall x_18: P_18(x_18) we can infer P_18(h). Finally, from q -> p_2, u -> p_2, q or u we can infer p_2, which contradicts ~p_2. Therefore, the answer is no.