Consider the following premises. forall z: T(z) -> U(z). U(b) -> T(b). T(b) -> t. ~t. Can we infer ~U(b) from them? If possible, name the inference rules being used at each step.
 From forall z: T(z) -> U(z) we can infer T(b) -> U(b) via universal instantiation. From U(b) -> T(b), T(b) -> U(b) we can infer U(b) <-> T(b) via biconditional introduction. From T(b) -> t, ~t we can infer ~T(b) via modus tollens. From U(b) <-> T(b) we can infer U(b) -> T(b) via biconditional elimination. Finally, from U(b) -> T(b), ~T(b) we can infer ~U(b) via modus tollens. Therefore, the answer is yes.