Consider the following premises. forall x_2: ~U_4(x_2). ~p_8 -> q. p_8 <-> U_4(a_14). Can we infer q from them?
 From forall x_2: ~U_4(x_2) we can infer ~U_4(a_14). From p_8 <-> U_4(a_14), ~U_4(a_14) we can infer ~p_8. Finally, from ~p_8 -> q, ~p_8 we can infer q. Therefore, the answer is yes.