[10 pts.] Resolution is a technique for proving theorems in predicate calculus. Given the following rules and facts, prove that ' happy(ali)' is true with resolution refutation method. \[ \begin{array}{l} \forall x[\operatorname{pass}(x, S E) \wedge \operatorname{win}(x, \text { lottery }) ightarrow \operatorname{happy}(x)] \\ \forall x \forall y[\operatorname{studies}(x) \vee \operatorname{lucky}(x) ightarrow \operatorname{pass}(x, y)] \\ \text { study(ali) ^ lucky(ali) } \\ \forall x[\operatorname{lucky}(x) ightarrow \operatorname{win}(x, \text { lottery })] \\ \end{array} \]