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