Consider the following premises. forall x_8: P_9(x_8) -> S_8(x_8). forall x_9: P_9(x_9). q_1 -> S_8(a_9). Can we infer S_8(a_9) from them?
 From forall x_9: P_9(x_9) we can infer P_9(a_9). From forall x_8: P_9(x_8) -> S_8(x_8) we can infer P_9(a_9) -> S_8(a_9). From P_9(a_9) we can infer P_9(a_9) or q_1. Finally, from P_9(a_9) -> S_8(a_9), q_1 -> S_8(a_9), P_9(a_9) or q_1 we can infer S_8(a_9). Therefore, the answer is yes.