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