Consider the following premises. ~q_1. u -> p. p -> q_1. s_4 -> u. Can we infer ~s_4 from them? If possible, name the inference rules being used at each step.
 From s_4 -> u, u -> p we can infer s_4 -> p via transitivity. From p -> q_1, ~q_1 we can infer ~p via modus tollens. Finally, from s_4 -> p, ~p we can infer ~s_4 via modus tollens. Therefore, the answer is yes.