Consider the following premises. s -> s_1. q or ~s_1. q -> s. Can we infer ~(s_1 -> q) from them? If possible, name the inference rules being used at each step.
 From q -> s, s -> s_1 we can infer q -> s_1 via transitivity. Finally, from q or ~s_1 we can infer s_1 -> q via rewriting, which contradicts ~(s_1 -> q). Therefore, the answer is no.