Consider the following premises. forall y_1: ~P_4(y_1). t <-> w. w <-> P_4(a_10). Can we infer t from them?
 From forall y_1: ~P_4(y_1) we can infer ~P_4(a_10). From w <-> P_4(a_10), ~P_4(a_10) we can infer ~w. Finally, from t <-> w, ~w we can infer ~t, which contradicts t. Therefore, the answer is no.