Consider the following premises. r. q -> p_5. p_5 or ~r. Can we infer ~p_5 from them? If possible, name the inference rules being used at each step.
 From p_5 or ~r we can infer r -> p_5 via rewriting. From r we can infer r or q via addition. Finally, from r -> p_5, q -> p_5, r or q we can infer p_5 via disjunction elimination, which contradicts ~p_5. Therefore, the answer is no.