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