What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? q_1 <-> U(a_16). forall x_2: ~U(x_2). u_4.
q_1 -> U(a_16). U(a_16) -> q_1.