Consider the following premises. forall x_10: R_4(x_10) -> T(x_10). forall x_10: R_4(x_10) or U_4(x_10). forall x_10: U_4(x_10) -> T(x_10). forall x: T(x) -> U(x). Can we infer ~U(g) from them?
 From forall x_10: R_4(x_10) -> T(x_10), forall x_10: U_4(x_10) -> T(x_10), forall x_10: R_4(x_10) or U_4(x_10) we can infer forall x_10: T(x_10). From forall x_10: T(x_10) we can infer T(g). From forall x: T(x) -> U(x) we can infer T(g) -> U(g). Finally, from T(g) -> U(g), T(g) we can infer U(g), which contradicts ~U(g). Therefore, the answer is no.