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