Consider the following premises. ~u_2. p -> ~t. ~t_4 or t. t_4 or u_2. Can we infer ~p or q from them? If possible, name the inference rules being used at each step.
 From t_4 or u_2, ~t_4 or t we can infer u_2 or t via resolution. From u_2 or t, ~u_2 we can infer t via disjunctive syllogism. From p -> ~t, t we can infer ~p via modus tollens. Finally, from ~p we can infer ~p or q via addition. Therefore, the answer is yes.