Consider the following premises. t or q_6. s. t -> r_6. q_6 -> r_6. p_12 -> ~s. Can we infer ~p_12 and r_6 from them? If possible, name the inference rules being used at each step.
 From p_12 -> ~s, s we can infer ~p_12 via modus tollens. From t -> r_6, q_6 -> r_6, t or q_6 we can infer r_6 via disjunction elimination. Finally, from ~p_12, r_6 we can infer ~p_12 and r_6 via conjunction. Therefore, the answer is yes.