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