Consider the following premises. s. ~p. ~s or r_7. p <-> t. Can we infer r_7 from them? If possible, name the inference rules being used at each step.
 From s we can infer s or t via addition. From s or t, ~s or r_7 we can infer t or r_7 via resolution. From p <-> t, ~p we can infer ~t via biconditional elimination. Finally, from t or r_7, ~t we can infer r_7 via disjunctive syllogism. Therefore, the answer is yes.