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