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