Consider the following premises. t_4 <-> q. Q_13(a_10) <-> t_4. forall x_13: P_13(x_13) <-> Q_13(x_13). forall x_13: ~P_13(x_13). Can we infer q from them?
 From forall x_13: P_13(x_13) <-> Q_13(x_13), forall x_13: ~P_13(x_13) we can infer forall x_13: ~Q_13(x_13). From forall x_13: ~Q_13(x_13) we can infer ~Q_13(a_10). From Q_13(a_10) <-> t_4, ~Q_13(a_10) we can infer ~t_4. Finally, from t_4 <-> q, ~t_4 we can infer ~q, which contradicts q. Therefore, the answer is no.