Consider the following premises. forall z_3: ~W_4(z_3). s_2 <-> s_3. s_3 -> W_4(j_4). Can we infer ~s_2 from them?
 From forall z_3: ~W_4(z_3) we can infer ~W_4(j_4). From s_3 -> W_4(j_4), ~W_4(j_4) we can infer ~s_3. Finally, from s_2 <-> s_3, ~s_3 we can infer ~s_2. Therefore, the answer is yes.