-
Notifications
You must be signed in to change notification settings - Fork 16
/
rot13.lam
225 lines (225 loc) · 40.9 KB
/
rot13.lam
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
((\x.\y.\z.\a.\b.((\c.((\d.((\e.((\f.((\g.((\h.(a ((\i.(i (d ( \j.\k.(k (\l.\m.\n.\o.(o k (j m))) k)) a) (\j.(i z (d (\k.\l.\m.\n.\o.\p.((\q.((\r.((\s.(n (\t.\u.\v.\w.v) (\t.t) (\t.\u.\v.u) (\t.\u.u) (o (\t.\u.\v.(o (k l m) p)) o) (n (\t.\u.((\v.(t (\w.\A.\B.((\C.(A (C B) (s B C))) (\C.\D.(w (D ((\E.(m (\F.\G.\H.(E (y (\I.\J.(J (\K.\L.K) I)) F) G)) (E c m))) (\E.\F.(r B E (k l F u o)))) (\E.(E (y (\F.(F(\G.\H.H))) C) (v p))) A) (D (\E.\F.\G.\H.((\I.(F (I G) (s G I))) (s H (\I.\J.(E (e I C) (q J) (v p))))))) (D (\E.\F.((\G.(f (\H.\I.I) (E (s F e C)) G G (\H.(r F)))) c)) v) (q C) (h l C (r D) v) (s D (g l C) k m u o p) (D (\E.\F.(s E (f F F) C (\G.(r E)))) v) (r D C v))))))) (k l m u o)))))) (h p))) (g p))) (\q.(h j q (\r.(r (k l m) p))))))))))) (\i.\j.(d (\k.\l.\m.\n.(l (\o.\p.\q.(m (\r.\s.\t.(k l s (\u.\v.(k v s (\w.(n (\A.(A u w)))))))) (l n))) (n l l))) i c (\k.\l.(j k)))) b) (\i.\j.j))) (d (\h.\i.\j.\k.(i (\l.\m.\n.(j (\o.\p.\q.(o (h l) (h m) p k)) (k i))) (k c)))))) (d (\g.\h.\i.\j.\k.(i (\l.\m.\n.((\o.(h (\p.\q.\r.(l (h o) (o q p))) (o (\p.\q.q) (\p.\q.q)))) (\o.(g o m j (\p.\q.(l (k (\r.(r p q))) (k (\r.(r q p))))))))) (k j)))))) (d (\f.\g.\h.\i.\j.\k.(i (\l.\m.\n.(j (\o.\p.(f g h m p (\q.\r.((\s.((\t.((\u.((\v.(t s q (v (\w.\A.w)) (v (\w.\A.A)))) (t q (q (\v.\w.w) (\v.\w.v)) (u (\v.\w.v)) (u (\v.\w.w))))) (\u.\v.(k v (\w.(w u r)))))) (\t.\u.(l (s t u) (s u t))))) (h o (o (\s.\t.t) (\s.\t.s))))))))) (k g i)))))) (d (\e.\f.\g.(f (\h.\i.\j.(g (\k.\l.((\m.(h (k m (\n.\o.\p.o)) (k (\n.\o.\p.p) m))) (e i l))))) (\h.\i.\j.h)))))) (\d.((\e.(d (e e))) (\e.(d (e e))))))) ((\c.(y c (x c (\d.\e.e)))) (\c.\d.(d (\e.\f.e) c)))))(\x.\y.(((\x.\y.(x(x y)))(((\y.(y y))(\x.\y.(x(x y))))x))y))((\x.(x x x))(\x.\y.(x(x y))))
(\f.(f((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))
(\f.(f((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))
(\f.(f((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.\y.y)))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.a)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.x)))(\x.\y.y)))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.b)(\x.(x(\b.\c.b)(\b.\c.c)))))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.b)(\x.(x(\b.\c.b)(\b.\c.c)))))))))))(\x.\y.y)))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.x)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.\y.\z.x)))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))(\x.\y.y)))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)))(\x.\y.y)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))))))))))))))))))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.a)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.x)))(\x.\y.y)))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(y(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(y(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.a)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.x)))(\x.\y.y)))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(y(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(y(y(x(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(y(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(y(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(x(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(y(y(x(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.y)(\y.\z.z)))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.z)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\y.\z.y)(\y.\z.y)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))))(\x.\y.y)))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.y)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)(\y.\z.z)))(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(y(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))))(\x.\y.y)))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(y(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)))(\x.\y.y)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))(\x.\y.y)))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.b)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\f.(f(\x.(x(\y.\z.y)(\y.\z.z)))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.\y.x)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.c)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.z)(\x.(x(\z.\a.a)(\x.(x(\a.\b.a)(\a.\b.b)))))))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.x)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.\y.\z.y)))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.d)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\f.(f(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.b)(\a.\b.b)))))))(\x.\y.x)))))(\x.\y.y)))))))))))))))))))))))))))))))))))))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.a)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(y(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.x)))(\x.\y.y)))
(\f.(f
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.x)((\x.\y.(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(\x.\y.y))))))))))))))))))))))))))(\x.\y.(y(\x.\a.x)x))(\x.\y.(y(\x.\a.a)x)))(\x.(x(\y.\z.y)(\y.\z.z)))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.e)(\x.\y.y)(\x.(x(\y.\z.y)(\y.\z.z)))(\x.(x(\y.\z.z)(\x.(x(\z.\a.z)(\x.(x(\a.\b.a)(\a.\b.b)))))))))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.x)(\x.\y.y)(\x.\y.y)(\x.\y.\z.z)))
(\f.(f(\f.(f(\x.\y.\z.\a.\b.\c.\d.\e.x)(\x.\y.y)(\x.\y.y)(\x.\y.\z.z)))(\x.\y.y)))))))))
(\x.\y.y))))))))))))))))))))))))))))))))))))))))))))))))))))