Consider the following premises. w_4 -> q. ~q. s <-> s_1. s_1 -> w_4. Can we infer ~s from them? If possible, name the inference rules being used at each step.
 From s_1 -> w_4, w_4 -> q we can infer s_1 -> q via transitivity. From s_1 -> q, ~q we can infer ~s_1 via modus tollens. Finally, from s <-> s_1, ~s_1 we can infer ~s via biconditional elimination. Therefore, the answer is yes.