Consider the following premises. forall x_10: ~Q_10(x_10). forall x_10: Q_10(x_10) -> R_4(x_10). forall x_10: R_4(x_10) -> Q_10(x_10). p -> R_4(h). Can we infer ~p from them?
 From forall x_10: R_4(x_10) -> Q_10(x_10), forall x_10: Q_10(x_10) -> R_4(x_10) we can infer forall x_10: R_4(x_10) <-> Q_10(x_10). From forall x_10: R_4(x_10) <-> Q_10(x_10), forall x_10: ~Q_10(x_10) we can infer forall x_10: ~R_4(x_10). From forall x_10: ~R_4(x_10) we can infer ~R_4(h). Finally, from p -> R_4(h), ~R_4(h) we can infer ~p. Therefore, the answer is yes.