Consider the following premises. forall x: R_1(x) -> S(x). ~s_3 or s_1. s_3 or R_1(a_8). s_1 -> S(a_8). Can we infer S(a_8) from them?
 From forall x: R_1(x) -> S(x) we can infer R_1(a_8) -> S(a_8). From s_3 or R_1(a_8), ~s_3 or s_1 we can infer R_1(a_8) or s_1. Finally, from R_1(a_8) -> S(a_8), s_1 -> S(a_8), R_1(a_8) or s_1 we can infer S(a_8). Therefore, the answer is yes.