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 <-> S_17(a_17). w. R_17(a_17) -> ~w. forall x_17: R_17(x_17) <-> S_17(x_17).
~R_17(a_17) can be inferred via the modus tollens rule. t -> S_17(a_17) can be inferred via the biconditional elimination rule. S_17(a_17) -> t can be inferred via the biconditional elimination rule. forall x_17: R_17(x_17) -> S_17(x_17) can be inferred via the universal biconditional elimination rule. forall x_17: S_17(x_17) -> R_17(x_17) can be inferred via the universal biconditional elimination rule.