Consider the following premises. w or u. r_20 -> t. forall x: Q(x). u -> t. ~w or r_20. Can we infer ~t from them? If possible, name the inference rules being used at each step.
 From w or u, ~w or r_20 we can infer u or r_20 via resolution. Finally, from u -> t, r_20 -> t, u or r_20 we can infer t via disjunction elimination, which contradicts ~t. Therefore, the answer is no.