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