Consider the following crypto arithmetical puzzle: TWO + THREE + SEVEN = TWELVE. It is possible to substitute digits from 0 - 9 for letters in such a way that this is a correct arithmetic equation. Note that no two letters should be assigned the same value. Leading zeros are not permitted on numbers.

Write a query goal(T,W,O,H,R,E,S,V,N,L) such that the program finds letter values that, when read as base 10 numbers, satisfy the equation TWO + THREE + SEVEN = TWELVE.

Use the optimization techniques described in the course to rewrite your program as necessary to produce an answer as rapidly as possible. Do not apply any clever reformulations of the problem (e.g. solving the problem yourself and building in the answers); stick to simple optimization techniques, such as subgoal ordering and subgoal elimination. Hint: You will probably need to increase the unification limit for queries to 1,000,000 or more to get an answer.

Submission details: Head to Gradescope.