Consider the following premises. ~R_9(a_9). forall x_9: R_9(x_9) <-> S_9(x_9). S_9(a_9) -> r_4. r_4 -> S_9(a_9). Can we infer r_4 from them?
 From forall x_9: R_9(x_9) <-> S_9(x_9) we can infer R_9(a_9) <-> S_9(a_9). From R_9(a_9) <-> S_9(a_9), ~R_9(a_9) we can infer ~S_9(a_9). From S_9(a_9) -> r_4, r_4 -> S_9(a_9) we can infer S_9(a_9) <-> r_4. Finally, from S_9(a_9) <-> r_4, ~S_9(a_9) we can infer ~r_4, which contradicts r_4. Therefore, the answer is no.