Consider the following premises. U_1(i_3) <-> S_14(d). ~S(d). forall x_14: S(x_14) <-> S_14(x_14). forall y_4: U_3(y_4) <-> U_1(y_4). Can we infer ~U_3(i_3) from them?
 From forall x_14: S(x_14) <-> S_14(x_14) we can infer S(d) <-> S_14(d). From forall y_4: U_3(y_4) <-> U_1(y_4) we can infer U_3(i_3) <-> U_1(i_3). From S(d) <-> S_14(d), ~S(d) we can infer ~S_14(d). From U_1(i_3) <-> S_14(d), ~S_14(d) we can infer ~U_1(i_3). Finally, from U_3(i_3) <-> U_1(i_3), ~U_1(i_3) we can infer ~U_3(i_3). Therefore, the answer is yes.