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