Consider the following premises. ~P(b_1). forall x_5: ~P_5(x_5) or U(x_5). forall x_5: P_5(x_5) or P(x_5). Can we infer ~U(b_1) from them?
 From forall x_5: P_5(x_5) or P(x_5), forall x_5: ~P_5(x_5) or U(x_5) we can infer forall x_5: P(x_5) or U(x_5). From forall x_5: P(x_5) or U(x_5) we can infer P(b_1) or U(b_1). Finally, from P(b_1) or U(b_1), ~P(b_1) we can infer U(b_1), which contradicts ~U(b_1). Therefore, the answer is no.