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: ~s. forall x_21: S_1(x_21) <-> S_21(x_21). ~S_1(d_3) <-> q_1. S_21(d_3) <-> s.
~S_1(d_3) -> q_1 can be inferred via the biconditional elimination rule. S_21(d_3) -> s can be inferred via the biconditional elimination rule. q_1 -> ~S_1(d_3) can be inferred via the biconditional elimination rule. s -> S_21(d_3) can be inferred via the biconditional elimination rule. ~S_21(d_3) can be inferred via the biconditional elimination rule. forall x_21: S_1(x_21) -> S_21(x_21) can be inferred via the universal biconditional elimination rule. forall x_21: S_21(x_21) -> S_1(x_21) can be inferred via the universal biconditional elimination rule.