1Maude> ==========================================
2unify in TEST : g(f(X, X, Y, Y, h(Z)), f(X, Y, Y, Z, Z)) =? g(f(A, A, A, B, C),
3    f(A, B, B, h(C))) .
4
5Solution 1
6X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
7    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
8    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
9    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
10    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
11    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
12    #13:Foo, #13:Foo, #14:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
13    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
14    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
15    #14:Foo)))))
16Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo)
17Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
18    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
19    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
20A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
21    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
22    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
23    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
24    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
25    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
26B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
27    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
28    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
29    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
30    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
31C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
32    #13:Foo, #13:Foo, #14:Foo)
33
34Solution 2
35X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
36    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
37    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
38    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
39    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#3:Foo,
40    #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo,
41    #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
42    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
43    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
44Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo)
45Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
46    #10:Foo, #11:Foo, #12:Foo)
47A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
48    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
49    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#3:Foo, #5:Foo,
50    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
51    #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
52    #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
53B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
54    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
55    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
56    #13:Foo, #14:Foo)
57C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
58    #13:Foo, #13:Foo, #14:Foo)
59
60Solution 3
61X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
62    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
63    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
64    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
65    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
66    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
67    #13:Foo, #13:Foo, #14:Foo)))
68Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
69    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
70    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
71    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo,
72    #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo,
73    h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
74    #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
75    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
76    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
77    #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo,
78    #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
79    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
80Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
81    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
82    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
83A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
84    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
85    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
86    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
87    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
88    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo,
89    #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo,
90    h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
91    #13:Foo, #13:Foo, #14:Foo)))))
92B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
93    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
94    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
95    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
96    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo,
97    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(
98    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
99    #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
100    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
101    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
102    #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo,
103    #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
104    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
105C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
106    #13:Foo, #13:Foo, #14:Foo)
107
108Solution 4
109X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
110    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
111    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
112    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
113    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
114    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
115    #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
116    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
117Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
118    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
119    #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo,
120    #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo,
121    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(
122    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
123    #11:Foo, #12:Foo)))
124Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
125    #10:Foo, #11:Foo, #12:Foo)
126A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
127    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
128    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo,
129    #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo,
130    #12:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
131    #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
132    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
133B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
134    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
135    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
136    #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo,
137    #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo,
138    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(
139    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
140    #11:Foo, #12:Foo)))
141C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
142    #13:Foo, #13:Foo, #14:Foo)
143
144Solution 5
145X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
146    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
147    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
148    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
149    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))
150Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
151    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
152    #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
153    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
154Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
155    #10:Foo, #11:Foo, #12:Foo)
156A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
157    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
158    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#3:Foo, #5:Foo,
159    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
160    #14:Foo)))
161B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
162    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
163    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
164    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
165    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
166C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
167    #13:Foo, #13:Foo, #14:Foo)
168
169Solution 6
170X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
171    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
172    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
173    #11:Foo, #11:Foo, #13:Foo, #13:Foo)
174Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
175    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
176    #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo,
177    #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo,
178    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(
179    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
180    #11:Foo, #12:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
181    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
182    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
183Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
184    #10:Foo, #11:Foo, #12:Foo)
185A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
186    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
187    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo,
188    #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo,
189    #12:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
190    #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
191B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
192    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
193    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
194    #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo,
195    #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(#1:Foo, #2:Foo, #2:Foo,
196    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)), h(f(
197    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
198    #11:Foo, #12:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
199    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
200C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
201    #13:Foo, #13:Foo, #14:Foo)
202
203Solution 7
204X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo,
205    #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo,
206    #2:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo,
207    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo,
208    #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo, #5:Foo, #5:Foo,
209    #5:Foo, #5:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo,
210    #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo,
211    #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #8:Foo, #8:Foo,
212    #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo,
213    #8:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo,
214    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo,
215    #10:Foo, #10:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo,
216    #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo,
217    #12:Foo, #12:Foo, #13:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, #14:Foo,
218    #14:Foo, #14:Foo, #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo,
219    #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo,
220    #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo,
221    #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #17:Foo, #17:Foo, #17:Foo,
222    #17:Foo, #17:Foo, #17:Foo, #17:Foo, #17:Foo, #18:Foo, #18:Foo, #18:Foo,
223    #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #19:Foo,
224    #19:Foo, #19:Foo, #19:Foo, #19:Foo, #19:Foo, #19:Foo, #20:Foo, #20:Foo,
225    #20:Foo, #20:Foo, #20:Foo, #21:Foo, #21:Foo, #21:Foo, #21:Foo, #21:Foo,
226    #21:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo,
227    #22:Foo, #22:Foo, #22:Foo, #22:Foo, #23:Foo, #23:Foo, #23:Foo, #23:Foo,
228    #23:Foo, #23:Foo, #23:Foo, #24:Foo, #24:Foo, #24:Foo, #24:Foo, #24:Foo,
229    #24:Foo, #24:Foo, #24:Foo, #24:Foo, #25:Foo, #25:Foo, #25:Foo, #26:Foo,
230    #26:Foo, #26:Foo, #26:Foo, #26:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo,
231    #27:Foo, #27:Foo, #27:Foo, #28:Foo, #28:Foo, #28:Foo, #28:Foo, #29:Foo,
232    #29:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo, #30:Foo, #30:Foo,
233    #30:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo,
234    #30:Foo, #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo,
235    #31:Foo, #31:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo,
236    #32:Foo, #32:Foo, #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo, #33:Foo,
237    #34:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo,
238    #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #36:Foo, #36:Foo,
239    #37:Foo, #37:Foo, #37:Foo, #37:Foo, #37:Foo, #37:Foo, #38:Foo, #38:Foo,
240    #38:Foo, #38:Foo, #38:Foo, #38:Foo, #38:Foo, #39:Foo, #39:Foo, #39:Foo,
241    #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #40:Foo,
242    #40:Foo, #40:Foo, #40:Foo, #40:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo,
243    #41:Foo, #41:Foo, #42:Foo, #42:Foo, #42:Foo, #42:Foo, #43:Foo, #43:Foo,
244    #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #44:Foo, #44:Foo,
245    #45:Foo, #45:Foo, #45:Foo, #45:Foo, #46:Foo, #46:Foo, #46:Foo, #46:Foo,
246    #46:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo,
247    #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo, #48:Foo, #48:Foo, #48:Foo,
248    #48:Foo, #49:Foo, #49:Foo, #50:Foo, #50:Foo, #50:Foo, #50:Foo, #50:Foo,
249    #50:Foo, #50:Foo, #50:Foo, #50:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo,
250    #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo,
251    #51:Foo, #51:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo,
252    #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #53:Foo,
253    #53:Foo, #53:Foo, #53:Foo, #53:Foo, #53:Foo, #53:Foo, #53:Foo, #54:Foo,
254    #54:Foo, #54:Foo, #54:Foo, #55:Foo, #55:Foo, #55:Foo, #56:Foo, #56:Foo,
255    #58:Foo, #58:Foo, #58:Foo, #59:Foo, #59:Foo, #59:Foo, #59:Foo, #59:Foo,
256    #60:Foo)
257Y --> f(#5:Foo, #9:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #17:Foo, #20:Foo,
258    #23:Foo, #25:Foo, #25:Foo, #26:Foo, #31:Foo, #33:Foo, #33:Foo, #34:Foo,
259    #36:Foo, #40:Foo, #41:Foo, #42:Foo, #42:Foo, #44:Foo, #46:Foo, #47:Foo,
260    #48:Foo, #48:Foo, #49:Foo, #49:Foo, #49:Foo, #53:Foo, #54:Foo, #55:Foo,
261    #55:Foo, #56:Foo, #56:Foo, #56:Foo, #57:Foo, #57:Foo, #60:Foo, #61:Foo,
262    #61:Foo, #61:Foo, #61:Foo, #61:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
263    #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #6:Foo,
264    #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo,
265    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo,
266    #11:Foo, #11:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #13:Foo,
267    #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #16:Foo, #16:Foo,
268    #16:Foo, #16:Foo, #16:Foo, #16:Foo, #17:Foo, #17:Foo, #17:Foo, #17:Foo,
269    #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #19:Foo, #19:Foo, #19:Foo,
270    #19:Foo, #20:Foo, #20:Foo, #20:Foo, #21:Foo, #21:Foo, #22:Foo, #22:Foo,
271    #23:Foo, #23:Foo, #24:Foo, #24:Foo, #24:Foo, #25:Foo, #25:Foo, #26:Foo,
272    #26:Foo, #26:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo, #28:Foo, #28:Foo,
273    #28:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo, #30:Foo, #30:Foo, #30:Foo,
274    #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo, #32:Foo, #32:Foo, #32:Foo,
275    #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo, #33:Foo, #34:Foo, #34:Foo,
276    #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo,
277    #35:Foo, #36:Foo, #36:Foo, #37:Foo, #37:Foo, #38:Foo, #38:Foo, #38:Foo,
278    #38:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #40:Foo, #40:Foo,
279    #40:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #42:Foo, #42:Foo,
280    #42:Foo, #42:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo,
281    #44:Foo, #44:Foo, #45:Foo, #45:Foo, #45:Foo, #46:Foo, #46:Foo, #46:Foo,
282    #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo, #48:Foo, #49:Foo, #49:Foo,
283    #49:Foo, #50:Foo, #50:Foo, #50:Foo, #51:Foo, #51:Foo, #51:Foo, #52:Foo,
284    #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #53:Foo, #53:Foo, #53:Foo,
285    #53:Foo, #54:Foo, #55:Foo, #55:Foo, #56:Foo, #56:Foo, #56:Foo, #57:Foo,
286    #58:Foo)))
287Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo,
288    #4:Foo, #5:Foo, #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo,
289    #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
290    #10:Foo, #10:Foo, #11:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo, #12:Foo,
291    #12:Foo, #12:Foo, #13:Foo, #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo,
292    #15:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #17:Foo,
293    #17:Foo, #17:Foo, #17:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo,
294    #19:Foo, #19:Foo, #19:Foo, #19:Foo, #20:Foo, #20:Foo, #20:Foo, #21:Foo,
295    #21:Foo, #22:Foo, #22:Foo, #23:Foo, #23:Foo, #24:Foo, #24:Foo, #24:Foo,
296    #25:Foo, #25:Foo, #26:Foo, #26:Foo, #26:Foo, #27:Foo, #27:Foo, #27:Foo,
297    #27:Foo, #28:Foo, #28:Foo, #28:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo,
298    #30:Foo, #30:Foo, #30:Foo, #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo,
299    #32:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo,
300    #33:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo,
301    #35:Foo, #35:Foo, #35:Foo, #35:Foo, #36:Foo, #36:Foo, #37:Foo, #37:Foo,
302    #38:Foo, #38:Foo, #38:Foo, #38:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo,
303    #39:Foo, #40:Foo, #40:Foo, #40:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo,
304    #41:Foo, #42:Foo, #42:Foo, #42:Foo, #42:Foo, #43:Foo, #43:Foo, #43:Foo,
305    #43:Foo, #43:Foo, #43:Foo, #44:Foo, #44:Foo, #45:Foo, #45:Foo, #45:Foo,
306    #46:Foo, #46:Foo, #46:Foo, #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo,
307    #48:Foo, #49:Foo, #49:Foo, #49:Foo, #50:Foo, #50:Foo, #50:Foo, #51:Foo,
308    #51:Foo, #51:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo,
309    #53:Foo, #53:Foo, #53:Foo, #53:Foo, #54:Foo, #55:Foo, #55:Foo, #56:Foo,
310    #56:Foo, #56:Foo, #57:Foo, #58:Foo)
311A --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo,
312    #3:Foo, #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
313    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo, #7:Foo,
314    #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo,
315    #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo, #13:Foo, #13:Foo,
316    #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #16:Foo, #16:Foo,
317    #16:Foo, #17:Foo, #17:Foo, #18:Foo, #18:Foo, #19:Foo, #20:Foo, #21:Foo,
318    #21:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo, #22:Foo, #23:Foo, #23:Foo,
319    #23:Foo, #24:Foo, #24:Foo, #24:Foo, #25:Foo, #26:Foo, #27:Foo, #29:Foo,
320    #30:Foo, #30:Foo, #30:Foo, #30:Foo, #31:Foo, #31:Foo, #32:Foo, #32:Foo,
321    #37:Foo, #37:Foo, #38:Foo, #39:Foo, #39:Foo, #40:Foo, #46:Foo, #47:Foo,
322    #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo, #50:Foo, #50:Foo, #50:Foo,
323    #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #52:Foo, #52:Foo,
324    #52:Foo, #53:Foo, #53:Foo, #54:Foo, #54:Foo, #55:Foo, #58:Foo, #59:Foo,
325    #59:Foo, #59:Foo, #60:Foo, #61:Foo, #61:Foo, h(f(#1:Foo, #2:Foo, #2:Foo,
326    #3:Foo, #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
327    #6:Foo, #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo,
328    #8:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo,
329    #11:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo,
330    #13:Foo, #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #16:Foo,
331    #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #17:Foo, #17:Foo, #17:Foo,
332    #17:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #19:Foo, #19:Foo,
333    #19:Foo, #19:Foo, #20:Foo, #20:Foo, #20:Foo, #21:Foo, #21:Foo, #22:Foo,
334    #22:Foo, #23:Foo, #23:Foo, #24:Foo, #24:Foo, #24:Foo, #25:Foo, #25:Foo,
335    #26:Foo, #26:Foo, #26:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo, #28:Foo,
336    #28:Foo, #28:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo, #30:Foo, #30:Foo,
337    #30:Foo, #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo, #32:Foo, #32:Foo,
338    #32:Foo, #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo, #33:Foo, #34:Foo,
339    #34:Foo, #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo,
340    #35:Foo, #35:Foo, #36:Foo, #36:Foo, #37:Foo, #37:Foo, #38:Foo, #38:Foo,
341    #38:Foo, #38:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #40:Foo,
342    #40:Foo, #40:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #42:Foo,
343    #42:Foo, #42:Foo, #42:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo,
344    #43:Foo, #44:Foo, #44:Foo, #45:Foo, #45:Foo, #45:Foo, #46:Foo, #46:Foo,
345    #46:Foo, #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo, #48:Foo, #49:Foo,
346    #49:Foo, #49:Foo, #50:Foo, #50:Foo, #50:Foo, #51:Foo, #51:Foo, #51:Foo,
347    #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #53:Foo, #53:Foo,
348    #53:Foo, #53:Foo, #54:Foo, #55:Foo, #55:Foo, #56:Foo, #56:Foo, #56:Foo,
349    #57:Foo, #58:Foo)))
350B --> f(#1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo,
351    #3:Foo, #3:Foo, #3:Foo, #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo,
352    #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo, #5:Foo, #5:Foo,
353    #6:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo,
354    #7:Foo, #7:Foo, #7:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo,
355    #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo, #9:Foo,
356    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo, #10:Foo,
357    #10:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo, #11:Foo,
358    #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo, #12:Foo,
359    #12:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, #14:Foo, #14:Foo, #14:Foo,
360    #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo, #15:Foo,
361    #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo,
362    #16:Foo, #16:Foo, #16:Foo, #17:Foo, #17:Foo, #17:Foo, #17:Foo, #17:Foo,
363    #17:Foo, #17:Foo, #17:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo,
364    #18:Foo, #18:Foo, #18:Foo, #18:Foo, #19:Foo, #19:Foo, #19:Foo, #19:Foo,
365    #19:Foo, #19:Foo, #19:Foo, #20:Foo, #20:Foo, #20:Foo, #20:Foo, #20:Foo,
366    #20:Foo, #21:Foo, #21:Foo, #21:Foo, #21:Foo, #22:Foo, #22:Foo, #22:Foo,
367    #22:Foo, #22:Foo, #23:Foo, #23:Foo, #23:Foo, #23:Foo, #23:Foo, #24:Foo,
368    #24:Foo, #24:Foo, #24:Foo, #24:Foo, #24:Foo, #25:Foo, #25:Foo, #25:Foo,
369    #25:Foo, #25:Foo, #26:Foo, #26:Foo, #26:Foo, #26:Foo, #26:Foo, #26:Foo,
370    #27:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo, #27:Foo, #28:Foo,
371    #28:Foo, #28:Foo, #28:Foo, #28:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo,
372    #29:Foo, #29:Foo, #29:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo, #30:Foo,
373    #30:Foo, #30:Foo, #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo,
374    #31:Foo, #31:Foo, #31:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo,
375    #32:Foo, #32:Foo, #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo, #33:Foo,
376    #33:Foo, #33:Foo, #33:Foo, #33:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo,
377    #34:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo, #35:Foo,
378    #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #35:Foo, #36:Foo,
379    #36:Foo, #36:Foo, #36:Foo, #37:Foo, #37:Foo, #37:Foo, #37:Foo, #38:Foo,
380    #38:Foo, #38:Foo, #38:Foo, #38:Foo, #38:Foo, #38:Foo, #39:Foo, #39:Foo,
381    #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo, #40:Foo,
382    #40:Foo, #40:Foo, #40:Foo, #40:Foo, #40:Foo, #41:Foo, #41:Foo, #41:Foo,
383    #41:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo, #42:Foo, #42:Foo,
384    #42:Foo, #42:Foo, #42:Foo, #42:Foo, #42:Foo, #42:Foo, #43:Foo, #43:Foo,
385    #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo, #43:Foo,
386    #44:Foo, #44:Foo, #44:Foo, #44:Foo, #45:Foo, #45:Foo, #45:Foo, #45:Foo,
387    #45:Foo, #46:Foo, #46:Foo, #46:Foo, #46:Foo, #46:Foo, #46:Foo, #47:Foo,
388    #47:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo,
389    #48:Foo, #48:Foo, #48:Foo, #48:Foo, #48:Foo, #49:Foo, #49:Foo, #49:Foo,
390    #49:Foo, #49:Foo, #49:Foo, #49:Foo, #50:Foo, #50:Foo, #50:Foo, #50:Foo,
391    #50:Foo, #50:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo, #51:Foo,
392    #51:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo,
393    #52:Foo, #52:Foo, #52:Foo, #52:Foo, #53:Foo, #53:Foo, #53:Foo, #53:Foo,
394    #53:Foo, #53:Foo, #53:Foo, #53:Foo, #54:Foo, #54:Foo, #54:Foo, #55:Foo,
395    #55:Foo, #55:Foo, #55:Foo, #55:Foo, #56:Foo, #56:Foo, #56:Foo, #56:Foo,
396    #56:Foo, #56:Foo, #56:Foo, #57:Foo, #57:Foo, #57:Foo, #58:Foo, #58:Foo,
397    #59:Foo, #60:Foo, #61:Foo, #61:Foo, #61:Foo, #61:Foo)
398C --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo,
399    #4:Foo, #5:Foo, #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #7:Foo, #7:Foo,
400    #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
401    #10:Foo, #10:Foo, #11:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo, #12:Foo,
402    #12:Foo, #12:Foo, #13:Foo, #14:Foo, #14:Foo, #15:Foo, #15:Foo, #15:Foo,
403    #15:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #16:Foo, #17:Foo,
404    #17:Foo, #17:Foo, #17:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo, #18:Foo,
405    #19:Foo, #19:Foo, #19:Foo, #19:Foo, #20:Foo, #20:Foo, #20:Foo, #21:Foo,
406    #21:Foo, #22:Foo, #22:Foo, #23:Foo, #23:Foo, #24:Foo, #24:Foo, #24:Foo,
407    #25:Foo, #25:Foo, #26:Foo, #26:Foo, #26:Foo, #27:Foo, #27:Foo, #27:Foo,
408    #27:Foo, #28:Foo, #28:Foo, #28:Foo, #29:Foo, #29:Foo, #29:Foo, #29:Foo,
409    #30:Foo, #30:Foo, #30:Foo, #30:Foo, #31:Foo, #31:Foo, #31:Foo, #31:Foo,
410    #32:Foo, #32:Foo, #32:Foo, #32:Foo, #32:Foo, #33:Foo, #33:Foo, #33:Foo,
411    #33:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #34:Foo, #35:Foo, #35:Foo,
412    #35:Foo, #35:Foo, #35:Foo, #35:Foo, #36:Foo, #36:Foo, #37:Foo, #37:Foo,
413    #38:Foo, #38:Foo, #38:Foo, #38:Foo, #39:Foo, #39:Foo, #39:Foo, #39:Foo,
414    #39:Foo, #40:Foo, #40:Foo, #40:Foo, #41:Foo, #41:Foo, #41:Foo, #41:Foo,
415    #41:Foo, #42:Foo, #42:Foo, #42:Foo, #42:Foo, #43:Foo, #43:Foo, #43:Foo,
416    #43:Foo, #43:Foo, #43:Foo, #44:Foo, #44:Foo, #45:Foo, #45:Foo, #45:Foo,
417    #46:Foo, #46:Foo, #46:Foo, #47:Foo, #47:Foo, #47:Foo, #48:Foo, #48:Foo,
418    #48:Foo, #49:Foo, #49:Foo, #49:Foo, #50:Foo, #50:Foo, #50:Foo, #51:Foo,
419    #51:Foo, #51:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo, #52:Foo,
420    #53:Foo, #53:Foo, #53:Foo, #53:Foo, #54:Foo, #55:Foo, #55:Foo, #56:Foo,
421    #56:Foo, #56:Foo, #57:Foo, #58:Foo)
422
423Solution 8
424X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
425    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
426    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
427    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
428    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
429    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
430    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
431    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
432    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
433Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo)
434Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
435    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
436    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo,
437    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
438    #14:Foo)))
439A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
440    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
441    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
442    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
443    #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
444    #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
445B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
446    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
447    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
448    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
449    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
450    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
451C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
452    #13:Foo, #13:Foo, #14:Foo)
453
454Solution 9
455X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
456    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
457    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
458    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
459    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))
460Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
461    #1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
462    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
463    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
464    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))),
465    h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
466    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
467    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo,
468    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
469    #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo,
470    #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
471    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
472    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
473    #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
474    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
475    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
476    #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
477    #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
478Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
479    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
480    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo,
481    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
482    #14:Foo)))
483A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
484    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
485    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo,
486    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
487    #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
488    #13:Foo, #13:Foo, #13:Foo, #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
489    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo,
490    #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo,
491    #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
492    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))))
493B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
494    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
495    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
496    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
497    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
498    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(
499    f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
500    #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
501    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo, #6:Foo,
502    #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)))),
503    h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
504    #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo,
505    #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(#3:Foo, #5:Foo,
506    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
507    #14:Foo)))), h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo,
508    #10:Foo, #10:Foo, #11:Foo, #12:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
509    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo)), h(f(
510    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
511    #13:Foo, #13:Foo, #14:Foo)))))
512C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
513    #13:Foo, #13:Foo, #14:Foo)
514
515Solution 10
516X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
517    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
518    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
519    #11:Foo, #11:Foo, #13:Foo, #13:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
520    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo,
521    #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo,
522    #12:Foo)))), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
523    #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
524    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))), h(f(#3:Foo,
525    #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo,
526    #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo,
527    #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))))
528Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo)
529Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
530    #10:Foo, #11:Foo, #12:Foo)
531A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
532    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
533    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo,
534    #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo,
535    #12:Foo)))), h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo,
536    #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo,
537    #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))))
538B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
539    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
540    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
541    #13:Foo, #14:Foo)
542C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
543    #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
544    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))
545
546Solution 11
547X --> f(#1:Foo, #1:Foo, #1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo,
548    #3:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo, #5:Foo,
549    #5:Foo, #6:Foo, #6:Foo, #6:Foo, #7:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo,
550    #11:Foo, #11:Foo, #13:Foo, #13:Foo)
551Y --> f(#7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #12:Foo, #14:Foo, h(f(
552    #3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
553    #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
554    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))), h(f(#3:Foo, #5:Foo,
555    #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo,
556    #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo,
557    #10:Foo, #10:Foo, #11:Foo, #12:Foo)))))
558Z --> f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo,
559    #10:Foo, #11:Foo, #12:Foo)
560A --> f(#1:Foo, #1:Foo, #2:Foo, #3:Foo, #4:Foo, #4:Foo, #4:Foo, #5:Foo, #5:Foo,
561    #6:Foo, #7:Foo, #8:Foo, #8:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo,
562    #10:Foo, #11:Foo, #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo,
563    #2:Foo, #2:Foo, #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo,
564    #12:Foo)))))
565B --> f(#1:Foo, #1:Foo, #2:Foo, #2:Foo, #2:Foo, #3:Foo, #3:Foo, #4:Foo, #5:Foo,
566    #6:Foo, #7:Foo, #8:Foo, #8:Foo, #8:Foo, #8:Foo, #9:Foo, #9:Foo, #9:Foo,
567    #9:Foo, #10:Foo, #10:Foo, #10:Foo, #11:Foo, #11:Foo, #12:Foo, #12:Foo,
568    #13:Foo, #14:Foo, h(f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo,
569    #11:Foo, #13:Foo, #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo,
570    #3:Foo, #9:Foo, #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))))
571C --> f(#3:Foo, #5:Foo, #6:Foo, #6:Foo, #10:Foo, #11:Foo, #11:Foo, #13:Foo,
572    #13:Foo, #13:Foo, #14:Foo, h(f(#1:Foo, #2:Foo, #2:Foo, #3:Foo, #9:Foo,
573    #9:Foo, #9:Foo, #10:Foo, #10:Foo, #11:Foo, #12:Foo)))
574==========================================
575unify in FOO : X =? W /\ f(X, Y) =? f(W, Z) .
576
577Solution 1
578X --> #1:Foo
579W --> #1:Foo
580Y --> #2:Foo
581Z --> #2:Foo
582==========================================
583unify in NAT' : X =? s (X * Y) .
584
585Solution 1
586X --> s 0
587Y --> 0
588==========================================
589unify in NAT' : X =? s X * Y .
590
591Solution 1
592X --> 0
593Y --> 0
594==========================================
595unify in NAT' : s X =? s X * Y .
596
597Solution 1
598X --> #1:Nat
599Y --> s 0
600==========================================
601unify in NAT' : s X =? X * Y .
602
603Solution 1
604X --> s 0
605Y --> s_^2(0)
606==========================================
607unify in COMM : X =? c(f(X, Y), Z) .
608
609Solution 1
610X --> c(a, b)
611Z --> a
612Y --> b
613
614Solution 2
615X --> c(a, b)
616Z --> b
617Y --> a
618==========================================
619unify in FOO2 : X =? f(Y, a, b) /\ Y =? g(X, c, d) .
620
621Solution 1
622X --> f(a, b)
623Y --> g(c, d)
624
625Solution 2
626X --> f(a, b)
627Y --> g(c, d)
628==========================================
629unify in FOO3 : X =? f(Y, a, b) /\ Y =? h(X) .
630
631Solution 1
632X --> f(a, b)
633Y --> h(f(a, b))
634Maude> Bye.
635