Consider the following premises. forall x_13: P_13(x_13) or Q_13(x_13). ~Q_13(a_6) or p. R_13(a_6) -> r_7. q_7 -> r_7. p -> q_7. forall x_13: ~P_13(x_13) or R_13(x_13). Can we infer ~r_7 from them?
 From forall x_13: P_13(x_13) or Q_13(x_13), forall x_13: ~P_13(x_13) or R_13(x_13) we can infer forall x_13: Q_13(x_13) or R_13(x_13). From p -> q_7, q_7 -> r_7 we can infer p -> r_7. From forall x_13: Q_13(x_13) or R_13(x_13) we can infer Q_13(a_6) or R_13(a_6). From Q_13(a_6) or R_13(a_6), ~Q_13(a_6) or p we can infer R_13(a_6) or p. Finally, from R_13(a_6) -> r_7, p -> r_7, R_13(a_6) or p we can infer r_7, which contradicts ~r_7. Therefore, the answer is no.