Consider the following premises. forall x_6: ~Q_6(x_6). P_6(a_5) <-> s. forall x_6: P_6(x_6) -> Q_6(x_6). Can we infer ~s from them?
 From forall x_6: P_6(x_6) -> Q_6(x_6), forall x_6: ~Q_6(x_6) we can infer forall x_6: ~P_6(x_6). From forall x_6: ~P_6(x_6) we can infer ~P_6(a_5). Finally, from P_6(a_5) <-> s, ~P_6(a_5) we can infer ~s. Therefore, the answer is yes.