What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? Name the inference rule being used: T(i) <-> s. forall y_4: S(y_4) or T(y_4). forall y_4: ~S(y_4) or W_3(y_4). ~s.
T(i) -> s can be inferred via the biconditional elimination rule. s -> T(i) can be inferred via the biconditional elimination rule. ~T(i) can be inferred via the biconditional elimination rule. forall y_4: T(y_4) or W_3(y_4) can be inferred via the universal resolution rule.