Consider the following premises. forall x_20: Q(x_20) and S_20(x_20). ~q_1. s <-> q_1. Can we infer ~Q(a_20) from them?
 From forall x_20: Q(x_20) and S_20(x_20) we can infer Q(a_20) and S_20(a_20). From s <-> q_1, ~q_1 we can infer ~s. Finally, from Q(a_20) and S_20(a_20) we can infer Q(a_20), which contradicts ~Q(a_20). Therefore, the answer is no.