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