Consider the following premises. ~t. p_2 -> t. forall x_18: P_18(x_18). Can we infer P_18(c) and ~p_2 from them? If possible, name the inference rules being used at each step.
 From forall x_18: P_18(x_18) we can infer P_18(c) via universal instantiation. From p_2 -> t, ~t we can infer ~p_2 via modus tollens. Finally, from P_18(c), ~p_2 we can infer P_18(c) and ~p_2 via conjunction. Therefore, the answer is yes.