Consider the following premises. u_2. ~p_3 -> s. p_12 -> ~u_2. p_3 -> p_12. Can we infer ~s from them? If possible, name the inference rules being used at each step.
 From p_12 -> ~u_2, u_2 we can infer ~p_12 via modus tollens. From p_3 -> p_12, ~p_12 we can infer ~p_3 via modus tollens. Finally, from ~p_3 -> s, ~p_3 we can infer s via modus ponens, which contradicts ~s. Therefore, the answer is no.