Consider the following premises. ~p_12. s_1 -> p_1. p_1 -> r_15. t -> s_1. p_12 <-> r_15. Can we infer ~t from them? If possible, name the inference rules being used at each step.
 From s_1 -> p_1, p_1 -> r_15 we can infer s_1 -> r_15 via transitivity. From p_12 <-> r_15, ~p_12 we can infer ~r_15 via biconditional elimination. From s_1 -> r_15, ~r_15 we can infer ~s_1 via modus tollens. Finally, from t -> s_1, ~s_1 we can infer ~t via modus tollens. Therefore, the answer is yes.