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