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: forall x_13: R_13(x_13) -> S_13(x_13). ~p or R_13(a_13). p or w. w <-> S_13(a_13).
w or R_13(a_13) can be inferred via the resolution rule. R_1(a_13) -> ~p can be inferred via the rewriting rule. w -> S_13(a_13) can be inferred via the biconditional elimination rule. S_13(a_13) -> w can be inferred via the biconditional elimination rule.