Consider the following premises. forall z_3: ~R(z_3) or R_2(z_3). forall z_3: R(z_3) or T_4(z_3). ~T_4(a). Can we infer ~R_2(a) from them? If possible, name the inference rules being used at each step.
 From forall z_3: R(z_3) or T_4(z_3), forall z_3: ~R(z_3) or R_2(z_3) we can infer forall z_3: T_4(z_3) or R_2(z_3) via universal resolution. From forall z_3: T_4(z_3) or R_2(z_3) we can infer T_4(a) or R_2(a) via universal instantiation. Finally, from T_4(a) or R_2(a), ~T_4(a) we can infer R_2(a) via disjunctive syllogism, which contradicts ~R_2(a). Therefore, the answer is no.