Consider the following premises. r_4 -> T(a_7). forall z: ~Q_2(z). T(a_7) -> r_4. forall z: T(z) -> Q_2(z). Can we infer r_4 from them?
 From forall z: T(z) -> Q_2(z), forall z: ~Q_2(z) we can infer forall z: ~T(z). From forall z: ~T(z) we can infer ~T(a_7). From T(a_7) -> r_4, r_4 -> T(a_7) we can infer T(a_7) <-> r_4. Finally, from T(a_7) <-> r_4, ~T(a_7) we can infer ~r_4, which contradicts r_4. Therefore, the answer is no.