Consider the following premises. forall x_13: P_2(x_13) -> Q_13(x_13). P_2(a_12) or ~q_3. forall x_13: Q_13(x_13) -> P_2(x_13). Can we infer q_3 -> Q_13(a_12) from them?
 From forall x_13: P_2(x_13) -> Q_13(x_13), forall x_13: Q_13(x_13) -> P_2(x_13) we can infer forall x_13: P_2(x_13) <-> Q_13(x_13). From forall x_13: P_2(x_13) <-> Q_13(x_13) we can infer P_2(a_12) <-> Q_13(a_12). From P_2(a_12) or ~q_3 we can infer q_3 -> P_2(a_12). From P_2(a_12) <-> Q_13(a_12) we can infer P_2(a_12) -> Q_13(a_12). Finally, from q_3 -> P_2(a_12), P_2(a_12) -> Q_13(a_12) we can infer q_3 -> Q_13(a_12). Therefore, the answer is yes.