Consider the following premises. There is at least one x_12 for which if x_12 were excited, then x_12 is a police officer. For all x_12, x_12 is a police officer if and only if x_12 will sleep. For all x_12, x_12 will not sleep. For all x_12, if x_12 were fast, then x_12 is excited. Can we infer the following from them? If we can, name the inference rule being used: There is at least one x_12 for which x_12 is not fast.
 From the fact that for all x_12, x_12 is a police officer if and only if x_12 will sleep, and that for all x_12, x_12 will not sleep we can infer that for all x_12, x_12 is not a police officer via universal biconditional elimination. From the fact that there is at least one x_12 for which if x_12 were excited, then x_12 is a police officer, and that for all x_12, x_12 is not a police officer we can infer that there is at least one x_12 for which x_12 is not excited via existential modus tollens. Finally, from the fact that for all x_12, if x_12 were fast, then x_12 is excited, and that there is at least one x_12 for which x_12 is not excited we can infer that there is at least one x_12 for which x_12 is not fast via existential modus tollens. Therefore, the answer is yes.