Consider the following premises. ~T(h_4) or r_5. ~S(h_4) or r_2. forall y_4: T(y_4) or S(y_4). ~r_5. Can we infer ~r_2 from them? If possible, name the inference rules being used at each step.
 From forall y_4: T(y_4) or S(y_4) we can infer T(h_4) or S(h_4) via universal instantiation. From T(h_4) or S(h_4), ~T(h_4) or r_5 we can infer S(h_4) or r_5 via resolution. From S(h_4) or r_5, ~S(h_4) or r_2 we can infer r_5 or r_2 via resolution. Finally, from r_5 or r_2, ~r_5 we can infer r_2 via disjunctive syllogism, which contradicts ~r_2. Therefore, the answer is no.