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