Consider the following premises. ~p. forall z: S(z) <-> R(z). p <-> R(i). Can we infer ~S(i) from them? If possible, name the inference rules being used at each step.
 From forall z: S(z) <-> R(z) we can infer S(i) <-> R(i) via universal instantiation. From p <-> R(i), ~p we can infer ~R(i) via biconditional elimination. Finally, from S(i) <-> R(i), ~R(i) we can infer ~S(i) via biconditional elimination. Therefore, the answer is yes.