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