Consider the following premises. r_2. forall x_17: R_17(x_17) <-> S_17(x_17). S_17(c_1) or ~r_2. Can we infer ~R_17(c_1) from them?
 From forall x_17: R_17(x_17) <-> S_17(x_17) we can infer R_17(c_1) <-> S_17(c_1). From S_17(c_1) or ~r_2 we can infer r_2 -> S_17(c_1). From R_17(c_1) <-> S_17(c_1) we can infer S_17(c_1) -> R_17(c_1). From r_2 -> S_17(c_1), S_17(c_1) -> R_17(c_1) we can infer r_2 -> R_17(c_1). Finally, from r_2 -> R_17(c_1), r_2 we can infer R_17(c_1), which contradicts ~R_17(c_1). Therefore, the answer is no.