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