Consider the following premises. R_5(a_5) or p. forall x_5: R_5(x_5) -> S_5(x_5). p -> S_5(a_5). Can we infer S_5(a_5) from them?
 From forall x_5: R_5(x_5) -> S_5(x_5) we can infer R_5(a_5) -> S_5(a_5). Finally, from R_5(a_5) -> S_5(a_5), p -> S_5(a_5), R_5(a_5) or p we can infer S_5(a_5). Therefore, the answer is yes.