Consider the following premises. u -> S_7(c_2). S_4(c_2) or u. forall x_7: S_4(x_7) <-> S_7(x_7). Can we infer ~S_7(c_2) from them?
 From forall x_7: S_4(x_7) <-> S_7(x_7) we can infer S_4(c_2) <-> S_7(c_2). From S_4(c_2) <-> S_7(c_2) we can infer S_4(c_2) -> S_7(c_2). Finally, from S_4(c_2) -> S_7(c_2), u -> S_7(c_2), S_4(c_2) or u we can infer S_7(c_2), which contradicts ~S_7(c_2). Therefore, the answer is no.