Consider the following premises. p and r_1. forall x_23: ~R_23(x_23). t_4 -> R_23(f). Can we infer t_4 from them?
 From forall x_23: ~R_23(x_23) we can infer ~R_23(f). Finally, from t_4 -> R_23(f), ~R_23(f) we can infer ~t_4, which contradicts t_4. Therefore, the answer is no.