Consider the following premises. forall x_28: R_28(x_28) -> S_28(x_28). p_2 -> t_3. ~r. r <-> t_3. R_28(a_28). Can we infer S_28(a_28) and ~p_2 from them? If possible, name the inference rules being used at each step.
 From forall x_28: R_28(x_28) -> S_28(x_28) we can infer R_28(a_28) -> S_28(a_28) via universal instantiation. From r <-> t_3, ~r we can infer ~t_3 via biconditional elimination. From R_28(a_28) -> S_28(a_28), R_28(a_28) we can infer S_28(a_28) via modus ponens. From p_2 -> t_3, ~t_3 we can infer ~p_2 via modus tollens. Finally, from S_28(a_28), ~p_2 we can infer S_28(a_28) and ~p_2 via conjunction. Therefore, the answer is yes.