Consider the following premises. forall x_14: ~P_14(x_14) or R_14(x_14). t_4. forall x_14: P_14(x_14) or P_3(x_14). R_14(a_12) -> r_6. P_3(a_12) -> r_6. Can we infer ~r_6 from them?
 From forall x_14: P_14(x_14) or P_3(x_14), forall x_14: ~P_14(x_14) or R_14(x_14) we can infer forall x_14: P_3(x_14) or R_14(x_14). From forall x_14: P_3(x_14) or R_14(x_14) we can infer P_3(a_12) or R_14(a_12). Finally, from P_3(a_12) -> r_6, R_14(a_12) -> r_6, P_3(a_12) or R_14(a_12) we can infer r_6, which contradicts ~r_6. Therefore, the answer is no.