Consider the following premises. forall x_14: ~R_14(x_14). p -> p_8. p_8 <-> R_14(a_14). Can we infer p from them?
 From forall x_14: ~R_14(x_14) we can infer ~R_14(a_14). From p_8 <-> R_14(a_14), ~R_14(a_14) we can infer ~p_8. Finally, from p -> p_8, ~p_8 we can infer ~p, which contradicts p. Therefore, the answer is no.