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