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 y: U_2(y) <-> P_2(y). p_13 -> s. ~P_2(a).
~p_13 can be inferred via the modus tollens rule. ~s and ~P_2(a) can be inferred via the conjunction rule. ~P_2(a) and ~s can be inferred via the conjunction rule. forall y: U_2(y) -> P_2(y) can be inferred via the universal biconditional elimination rule. forall y: P_2(y) -> U_2(y) can be inferred via the universal biconditional elimination rule.