Consider the following premises. forall x_9: P_9(x_9). p_1 -> S_8(d). forall x_8: P_9(x_8) -> S_8(x_8). Can we infer S_8(d) from them? If possible, name the inference rules being used at each step.
 From forall x_9: P_9(x_9) we can infer P_9(d) via universal instantiation. From forall x_8: P_9(x_8) -> S_8(x_8) we can infer P_9(d) -> S_8(d) via universal instantiation. From P_9(d) we can infer P_9(d) or p_1 via addition. Finally, from P_9(d) -> S_8(d), p_1 -> S_8(d), P_9(d) or p_1 we can infer S_8(d) via disjunction elimination. Therefore, the answer is yes.