Consider the following premises. p_2 or t. ~p_2 or u. forall z: ~R_2(z). t -> R_2(a_13). Can we infer ~u from them?
 From forall z: ~R_2(z) we can infer ~R_2(a_13). From t -> R_2(a_13), ~R_2(a_13) we can infer ~t. From p_2 or t, ~p_2 or u we can infer t or u. Finally, from t or u, ~t we can infer u, which contradicts ~u. Therefore, the answer is no.