Consider the following premises. forall x_13: P_13(x_13) or Q_13(x_13). p_7 -> q_7. forall x_13: ~P_13(x_13) or R_13(x_13). R_13(a_6) -> r. q_7 -> r. ~Q_13(a_6) or p_7. Can we infer ~r 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_7 -> q_7, q_7 -> r we can infer p_7 -> r. 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_7 we can infer R_13(a_6) or p_7. Finally, from R_13(a_6) -> r, p_7 -> r, R_13(a_6) or p_7 we can infer r, which contradicts ~r. Therefore, the answer is no.