Consider the following premises. p <-> S(a_12). forall x_13: S(x_13) -> Q_13(x_13). forall x_13: Q_13(x_13) -> R_13(x_13). ~p. R_13(a_12) -> S(a_12). Can we infer ~R_13(a_12) from them? If possible, name the inference rules being used at each step.
 From forall x_13: S(x_13) -> Q_13(x_13), forall x_13: Q_13(x_13) -> R_13(x_13) we can infer forall x_13: S(x_13) -> R_13(x_13) via universal transitivity. From forall x_13: S(x_13) -> R_13(x_13) we can infer S(a_12) -> R_13(a_12) via universal instantiation. From R_13(a_12) -> S(a_12), S(a_12) -> R_13(a_12) we can infer R_13(a_12) <-> S(a_12) via biconditional introduction. From p <-> S(a_12), ~p we can infer ~S(a_12) via biconditional elimination. Finally, from R_13(a_12) <-> S(a_12), ~S(a_12) we can infer ~R_13(a_12) via biconditional elimination. Therefore, the answer is yes.