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