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