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