Consider the following premises. S_13(a_13) <-> q_8. forall x_13: R_13(x_13) or S_13(x_13). R_13(a_13) <-> q_8. Can we infer q_8 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 R_13(a_13) <-> q_8 we can infer R_13(a_13) -> q_8 via biconditional elimination. From S_13(a_13) <-> q_8 we can infer S_13(a_13) -> q_8 via biconditional elimination. Finally, from R_13(a_13) -> q_8, S_13(a_13) -> q_8, R_13(a_13) or S_13(a_13) we can infer q_8 via disjunction elimination. Therefore, the answer is yes.