Consider the following premises. ~q_17. w_4 <-> q_17. forall x: Q(x). Can we infer Q(a_9) and ~w_4 from them?
 From w_4 <-> q_17, ~q_17 we can infer ~w_4. From forall x: Q(x) we can infer Q(a_9). Finally, from Q(a_9), ~w_4 we can infer Q(a_9) and ~w_4. Therefore, the answer is yes.