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