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