Consider the following premises. r <-> s_1. forall x: P(x). r -> ~P(a_1). Can we infer ~s_1 from them? If possible, name the inference rules being used at each step.
 From forall x: P(x) we can infer P(a_1) via universal instantiation. From r -> ~P(a_1), P(a_1) we can infer ~r via modus tollens. Finally, from r <-> s_1, ~r we can infer ~s_1 via biconditional elimination. Therefore, the answer is yes.