Consider the following premises. forall x_19: S(x_19) -> ~Q_19(x_19). forall x_19: P_19(x_19). w_1 -> S(a_14). forall x_19: P_19(x_19) -> Q_19(x_19). t_4. Can we infer t_4 and ~w_1 from them?
 From forall x_19: P_19(x_19) -> Q_19(x_19), forall x_19: P_19(x_19) we can infer forall x_19: Q_19(x_19). From forall x_19: S(x_19) -> ~Q_19(x_19), forall x_19: Q_19(x_19) we can infer forall x_19: ~S(x_19). From forall x_19: ~S(x_19) we can infer ~S(a_14). From w_1 -> S(a_14), ~S(a_14) we can infer ~w_1. Finally, from t_4, ~w_1 we can infer t_4 and ~w_1. Therefore, the answer is yes.