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