Consider the following premises. forall x_14: P_14(x_14). t -> r_1. r_1 -> ~P_14(a). Can we infer ~t from them? If possible, name the inference rules being used at each step.
 From forall x_14: P_14(x_14) we can infer P_14(a) via universal instantiation. From r_1 -> ~P_14(a), P_14(a) we can infer ~r_1 via modus tollens. Finally, from t -> r_1, ~r_1 we can infer ~t via modus tollens. Therefore, the answer is yes.