Apply first-order resolution to the following KB to indicate whether or not the following sentence is true:

Happy(Joe)

If the sentence is true, show the steps to get there. If the truth of this sentence cannot be determined, explain why.

Show each step clearly, including any substitutions. The domain of variables includes peoples names and the constants High and Low. Assume that Equals(x, y) is a built-in function that can be evaluated as True if x and y are the same object, and False otherwise.

For all KB sentences with variables, the universal quantifier for those variables is implicit.

KB:

- ScoreOnGREs(x, High) Grades(x, High) AcceptedToUCSB(x)

- (ScoreOnGREs(x, High) ScoreOnGREs(x, Low)) Letters(x, High) AcceptedToUCB(x)

- ScoreOnGREs(x, High) ScoreOnGREs(x, Low)

- Exercise(x) Happy(x)

- Smart(x) AcceptedToUCB(x)

- Smart(x) Exercise(x)

- ScoreOnGREs(Joe, Low)

- Letters(Joe, High)

Query: ASK(KB, Happy(Joe))

(That is, were asking the KB, Is the sentence Happy(Joe) true?)