Consider the following premises. ~q_6. forall x_13: R_13(x_13) or S_13(x_13). p_6 -> q_6. R_13(a_13) <-> p_6. Can we infer ~S_13(a_13) from them? If possible, name the inference rules being used at each step.
 From forall x_13: R_13(x_13) or S_13(x_13) we can infer R_13(a_13) or S_13(a_13) via universal instantiation. From p_6 -> q_6, ~q_6 we can infer ~p_6 via modus tollens. From R_13(a_13) <-> p_6, ~p_6 we can infer ~R_13(a_13) via biconditional elimination. Finally, from R_13(a_13) or S_13(a_13), ~R_13(a_13) we can infer S_13(a_13) via disjunctive syllogism, which contradicts ~S_13(a_13). Therefore, the answer is no.