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