Consider the following premises. forall z: ~U_3(z). s_2 -> ~R_2(c_4). forall z: U_3(z) or R_2(z). Can we infer ~s_2 from them?
 From forall z: U_3(z) or R_2(z), forall z: ~U_3(z) we can infer forall z: R_2(z). From forall z: R_2(z) we can infer R_2(c_4). Finally, from s_2 -> ~R_2(c_4), R_2(c_4) we can infer ~s_2. Therefore, the answer is yes.