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