Consider the following premises. p_7 -> R_15(d). forall x_15: R_15(x_15) -> S_15(x_15). p_7 or ~S_15(d). Can we infer ~(p_7 <-> S_15(d)) from them?
 From forall x_15: R_15(x_15) -> S_15(x_15) we can infer R_15(d) -> S_15(d). From p_7 or ~S_15(d) we can infer S_15(d) -> p_7. From p_7 -> R_15(d), R_15(d) -> S_15(d) we can infer p_7 -> S_15(d). Finally, from p_7 -> S_15(d), S_15(d) -> p_7 we can infer p_7 <-> S_15(d), which contradicts ~(p_7 <-> S_15(d)). Therefore, the answer is no.