Consider the following premises. ~p_10. forall x: U_1(x) <-> S_2(x). p_10 <-> q_10. S_2(d_1) <-> q_10. Can we infer ~U_1(d_1) from them? If possible, name the inference rules being used at each step.
 From p_10 <-> q_10, ~p_10 we can infer ~q_10 via biconditional elimination. From forall x: U_1(x) <-> S_2(x) we can infer U_1(d_1) <-> S_2(d_1) via universal instantiation. From S_2(d_1) <-> q_10, ~q_10 we can infer ~S_2(d_1) via biconditional elimination. Finally, from U_1(d_1) <-> S_2(d_1), ~S_2(d_1) we can infer ~U_1(d_1) via biconditional elimination. Therefore, the answer is yes.