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