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