What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? forall z: R(z) <-> W(z). ~W(a_12). R(a_12) <-> q_3. q_3 <-> t.
R(a_12) -> q_3. q_3 -> t. q_3 -> R(a_12). t -> q_3. forall z: R(z) -> W(z). forall z: W(z) -> R(z).