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