Consider the following premises. p_18 -> Q_1(a_21). p_18 <-> p_4. ~S_21(a_21). forall x_21: Q_1(x_21) <-> S_21(x_21). Can we infer ~p_4 from them? If possible, name the inference rules being used at each step.
 From forall x_21: Q_1(x_21) <-> S_21(x_21) we can infer Q_1(a_21) <-> S_21(a_21) via universal instantiation. From p_18 <-> p_4 we can infer p_4 -> p_18 via biconditional elimination. From Q_1(a_21) <-> S_21(a_21), ~S_21(a_21) we can infer ~Q_1(a_21) via biconditional elimination. From p_18 -> Q_1(a_21), ~Q_1(a_21) we can infer ~p_18 via modus tollens. Finally, from p_4 -> p_18, ~p_18 we can infer ~p_4 via modus tollens. Therefore, the answer is yes.