Consider the following premises. s_2 or P_2(a). w_4 -> ~S_14(a). s_2 -> S_14(a). forall x_14: P_2(x_14) -> S_14(x_14). Can we infer ~w_4 from them?
 From forall x_14: P_2(x_14) -> S_14(x_14) we can infer P_2(a) -> S_14(a). From s_2 -> S_14(a), P_2(a) -> S_14(a), s_2 or P_2(a) we can infer S_14(a). Finally, from w_4 -> ~S_14(a), S_14(a) we can infer ~w_4. Therefore, the answer is yes.