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