Consider the following premises. forall x_12: R_12(x_12) <-> S_12(x_12). p -> s. s -> S_12(d). Can we infer ~(p -> R_12(d)) from them?
 From forall x_12: R_12(x_12) <-> S_12(x_12) we can infer R_12(d) <-> S_12(d). From p -> s, s -> S_12(d) we can infer p -> S_12(d). From R_12(d) <-> S_12(d) we can infer S_12(d) -> R_12(d). Finally, from p -> S_12(d), S_12(d) -> R_12(d) we can infer p -> R_12(d), which contradicts ~(p -> R_12(d)). Therefore, the answer is no.