Consider the following premises. ~S_16(d_1). S_16(d_1) -> R_16(d_1). forall x_16: R_16(x_16) -> S_16(x_16). Can we infer ~R_16(d_1) or p_3 from them? If possible, name the inference rules being used at each step.
 From forall x_16: R_16(x_16) -> S_16(x_16) we can infer R_16(d_1) -> S_16(d_1) via universal instantiation. From S_16(d_1) -> R_16(d_1), R_16(d_1) -> S_16(d_1) we can infer S_16(d_1) <-> R_16(d_1) via biconditional introduction. From S_16(d_1) <-> R_16(d_1), ~S_16(d_1) we can infer ~R_16(d_1) via biconditional elimination. Finally, from ~R_16(d_1) we can infer ~R_16(d_1) or p_3 via addition. Therefore, the answer is yes.