Consider the following premises. forall x_16: P_16(x_16) or ~Q_16(x_16). P_16(a_14) -> t. Q_16(a_14). Can we infer ~t from them?
 From forall x_16: P_16(x_16) or ~Q_16(x_16) we can infer forall x_16: Q_16(x_16) -> P_16(x_16). From forall x_16: Q_16(x_16) -> P_16(x_16) we can infer Q_16(a_14) -> P_16(a_14). From Q_16(a_14) -> P_16(a_14), Q_16(a_14) we can infer P_16(a_14). Finally, from P_16(a_14) -> t, P_16(a_14) we can infer t, which contradicts ~t. Therefore, the answer is no.