Consider the following premises. p -> t_4. W(a_8) -> t_4. forall x_9: W(x_9). Q_9(a_8) -> p. Can we infer t_4 from them?
 From forall x_9: W(x_9) we can infer forall x_9: W(x_9) or Q_9(x_9). From forall x_9: W(x_9) or Q_9(x_9) we can infer W(a_8) or Q_9(a_8). From Q_9(a_8) -> p, p -> t_4 we can infer Q_9(a_8) -> t_4. Finally, from W(a_8) -> t_4, Q_9(a_8) -> t_4, W(a_8) or Q_9(a_8) we can infer t_4. Therefore, the answer is yes.