Consider the following premises. p_13 or ~u. p -> p_13. ~u. p_13 -> u. Can we infer p from them?
 From p_13 or ~u we can infer u -> p_13. From p_13 -> u, u -> p_13 we can infer p_13 <-> u. From p_13 <-> u, ~u we can infer ~p_13. Finally, from p -> p_13, ~p_13 we can infer ~p, which contradicts p. Therefore, the answer is no.