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