Consider the following premises. forall x_14: P_2(x_14) -> Q_14(x_14). forall x_14: Q_14(x_14) -> P_2(x_14). ~P_2(a_13). s_3. Can we infer ~Q_14(a_13) from them?
 From forall x_14: P_2(x_14) -> Q_14(x_14), forall x_14: Q_14(x_14) -> P_2(x_14) we can infer forall x_14: P_2(x_14) <-> Q_14(x_14). From forall x_14: P_2(x_14) <-> Q_14(x_14) we can infer P_2(a_13) <-> Q_14(a_13). Finally, from P_2(a_13) <-> Q_14(a_13), ~P_2(a_13) we can infer ~Q_14(a_13). Therefore, the answer is yes.