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