Consider the following premises. ~q_11. w <-> S_1(a_7). forall z: S_1(z) <-> S(z). w <-> q_11. Can we infer ~S(a_7) from them?
 From w <-> q_11, ~q_11 we can infer ~w. From forall z: S_1(z) <-> S(z) we can infer S_1(a_7) <-> S(a_7). From w <-> S_1(a_7), ~w we can infer ~S_1(a_7). Finally, from S_1(a_7) <-> S(a_7), ~S_1(a_7) we can infer ~S(a_7). Therefore, the answer is yes.