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