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