Consider the following premises. q_1 -> W_3(a_7). W_3(a_7) -> q_1. forall x_2: ~W_3(x_2). Can we infer q_1 from them?
 From forall x_2: ~W_3(x_2) we can infer ~W_3(a_7). From W_3(a_7) -> q_1, q_1 -> W_3(a_7) we can infer W_3(a_7) <-> q_1. Finally, from W_3(a_7) <-> q_1, ~W_3(a_7) we can infer ~q_1, which contradicts q_1. Therefore, the answer is no.