Consider the following premises. w. ~q_1 or p_3. q_1 or r_3. ~r_3. Can we infer ~p_3 from them? If possible, name the inference rules being used at each step.
 From q_1 or r_3, ~q_1 or p_3 we can infer r_3 or p_3 via resolution. Finally, from r_3 or p_3, ~r_3 we can infer p_3 via disjunctive syllogism, which contradicts ~p_3. Therefore, the answer is no.