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