Consider the following premises. w_1 -> ~r. s <-> w_1. forall x_19: ~R_19(x_19). R_19(c) or r. Can we infer ~s from them?
 From forall x_19: ~R_19(x_19) we can infer ~R_19(c). From R_19(c) or r, ~R_19(c) we can infer r. From w_1 -> ~r, r we can infer ~w_1. Finally, from s <-> w_1, ~w_1 we can infer ~s. Therefore, the answer is yes.