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