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