What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? u_3 <-> u. ~u_1. w_4 -> u_3. u_1 <-> u.
u_3 -> u. u_1 -> u. u -> u_3. u -> u_1. ~u.