Consider the following premises. p_3 -> ~P_18(a). forall x_18: P_18(x_18). s. Can we infer s and ~p_3 from them?
 From forall x_18: P_18(x_18) we can infer P_18(a). From p_3 -> ~P_18(a), P_18(a) we can infer ~p_3. Finally, from s, ~p_3 we can infer s and ~p_3. Therefore, the answer is yes.