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