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