Consider the following premises. t_1 or ~r. u <-> w. w -> r. t_3 -> u. Can we infer w -> r from them? If possible, name the inference rules being used at each step.
That is one of the premises. Therefore, the answer is yes.