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_18(a_18) <-> q_15. ~q_15. forall x_18: R_18(x_18) <-> S_18(x_18). q_1.
~q_15 and q_1 can be inferred via the conjunction rule. q_1 and ~q_15 can be inferred via the conjunction rule. S_18(a_18) -> q_15 can be inferred via the biconditional elimination rule. q_15 -> S_18(a_18) can be inferred via the biconditional elimination rule. ~S_18(a_18) can be inferred via the biconditional elimination rule. forall x_18: R_18(x_18) -> S_18(x_18) can be inferred via the universal biconditional elimination rule. forall x_18: S_18(x_18) -> R_18(x_18) can be inferred via the universal biconditional elimination rule.