Consider the following premises. For all x, x will climb a mountain. There is at least one x for which x will not sleep or x is happy. For all x, if x were fast, then x is not climbing a mountain. For all x, x will sleep or x is fast. Can we infer the following from them? If we can, name the inference rule being used: For all x, x is not happy.
 From the fact that for all x, if x were fast, then x is not climbing a mountain, and that for all x, x will climb a mountain we can infer that for all x, x is not fast via universal modus tollens. From the fact that for all x, x will sleep or x is fast, and that there is at least one x for which x will not sleep or x is happy we can infer that there is at least one x for which x is fast or x is happy via existential resolution. Finally, from the fact that there is at least one x for which x is fast or x is happy, and that for all x, x is not fast we can infer that there is at least one x for which x is happy via existential disjunctive syllogism, which contradicts that For all x, x is not happy. Therefore, the answer is no.