Consider the following premises. forall x_17: R_17(x_17) or S_17(x_17). R_17(a_17) -> u. u or ~S_17(a_17). Can we infer ~u from them?
 From forall x_17: R_17(x_17) or S_17(x_17) we can infer R_17(a_17) or S_17(a_17). From u or ~S_17(a_17) we can infer S_17(a_17) -> u. Finally, from R_17(a_17) -> u, S_17(a_17) -> u, R_17(a_17) or S_17(a_17) we can infer u, which contradicts ~u. Therefore, the answer is no.