2
a(K(x),y) = x # label(constant_functions).
3
a(P1,p(x,y)) = x # label(projection_1).
4
a(P2,p(x,y)) = y # label(projection_2).
5
a(E,p(x,x)) = P1 # label(equality_1).
6
a(A,a(A,a(A,x))) = a(A,x) # label(2_1_a).
7
a(A,a(A,K(x))) = K(x) # label(2_1_b).
8
a(A,K(K(x))) = K(K(x)) # label(2_1_c).
9
K(p(x,y)) = p(K(x),K(y)) # label(2_2_b0).
10
K(a(P1,x)) = a(P1,K(x)) # label(2_2_b1).
11
K(a(P2,x)) = a(P2,K(x)) # label(2_2_b2).
12
a(a(P1,x),y) = a(P1,a(x,y)).
13
a(a(P2,x),y) = a(P2,a(x,y)).
14
a(A,P1) = K(P1) # label(2_3_b1a).
15
a(A,K(P1)) = P1 # label(2_3_b1b).
16
a(A,P2) = K(P2) # label(2_3_b2a).
17
a(A,K(P2)) = P2 # label(2_3_b2b).
18
a(A,p(P1,P2)) = p(K(P1),K(P2)).
19
a(A,p(K(P1),K(P2))) = p(P1,P2).
20
a(a(p(P1,K(P2)),K(x)),x) = x.
22
a(E,a(p(x,x),y)) = P1.
23
a(a(a(A,A),x),K(y)) = K(y).
24
a(p(K(x),K(y)),z) = p(x,y).
25
a(P1,a(p(x,y),z)) = a(x,z).
26
a(P2,a(p(x,y),z)) = a(y,z).
27
a(P2,a(A,p(x,y))) = a(A,y).
28
a(p(K(x),A),P1) = p(x,K(P1)).
29
a(p(A,K(x)),P1) = p(K(P1),x).
30
a(p(K(x),A),K(P1)) = p(x,P1).
31
a(p(A,K(x)),K(P1)) = p(P1,x).
32
a(p(K(x),A),P2) = p(x,K(P2)).
33
a(p(A,K(x)),P2) = p(K(P2),x).
34
a(p(K(x),A),K(P2)) = p(x,P2).
35
a(p(A,K(x)),K(P2)) = p(P2,x).
36
a(E,a(A,p(x,x))) = P1.
37
a(E,a(a(p(x,x),y),z)) = P1.
38
a(E,a(A,a(p(x,x),y))) = P1.
39
a(E,a(a(A,p(x,x)),y)) = P1.
40
a(E,a(A,a(A,p(x,x)))) = P1.
41
a(a(a(A,A),P1),p(P1,P2)) = P1.
42
a(a(a(A,A),P2),p(P1,P2)) = P2.
43
a(A,p(P1,P1)) = p(K(P1),K(P1)).
44
a(A,p(P1,K(P1))) = p(K(P1),P1).
45
a(A,p(P1,K(P2))) = p(K(P1),P2).
46
a(A,p(K(P1),P1)) = p(P1,K(P1)).
47
a(A,p(K(P1),K(P1))) = p(P1,P1).
48
a(A,p(K(P1),P2)) = p(P1,K(P2)).
49
a(a(a(A,A),E),p(P1,P2)) = P2.
51
a(A,p(P2,P1)) = p(K(P2),K(P1)).
52
a(A,p(P2,K(P1))) = p(K(P2),P1).
53
a(A,p(P2,P2)) = p(K(P2),K(P2)).
54
a(A,p(P2,K(P2))) = p(K(P2),P2).
55
a(A,p(K(P2),P1)) = p(P2,K(P1)).
56
a(A,p(K(P2),K(P1))) = p(P2,P1).
57
a(A,p(K(P2),P2)) = p(P2,K(P2)).
58
a(A,p(K(P2),K(P2))) = p(P2,P2).
62
a(a(A,K(E)),p(x,x)) = K(P1).
63
a(p(E,E),p(x,x)) = p(P1,P1).
64
a(p(E,E),p(P1,P2)) = p(P2,P2).
65
a(p(E,E),p(P2,P1)) = p(P2,P2).
66
a(p(E,E),f(P1,P2)) = p(P2,P2).
67
a(p(E,E),f(P2,P1)) = p(P2,P2).
68
a(P2,a(A,a(A,p(x,P1)))) = P1.
69
a(E,K(a(p(x,x),y))) = P1.
70
a(E,K(a(A,p(x,x)))) = P1.
71
a(P2,a(A,a(p(x,A),P1))) = P1.
72
a(P2,a(A,a(A,p(x,P2)))) = P2.
73
a(P2,a(A,a(p(x,A),P2))) = P2.
74
a(E,K(K(a(p(x,x),y)))) = P1.
75
a(E,K(K(a(A,p(x,x))))) = P1.
76
a(a(p(P1,A),K(P2)),P2) = P2.
77
a(p(P2,P2),p(x,x)) = p(x,x).
78
a(p(P2,E),p(P1,P2)) = p(P2,P2).
79
a(p(P2,P2),p(x,P1)) = p(P1,P1).
80
a(p(P2,P2),p(x,P2)) = p(P2,P2).
81
a(p(P1,P1),p(P1,x)) = p(P1,P1).
82
a(p(P1,P1),p(P2,x)) = p(P2,P2).
83
a(p(P1,P1),p(x,x)) = p(x,x).
84
a(P1,a(A,x)) = a(A,a(P1,x)).
85
a(A,a(P1,P1)) = a(P1,K(P1)).
86
a(A,a(P1,K(P1))) = a(P1,P1).
87
a(A,a(P1,P2)) = a(P1,K(P2)).
88
a(A,a(P1,K(P2))) = a(P1,P2).
89
a(a(A,a(A,E)),p(x,x)) = P1.
90
a(p(P1,E),p(x,x)) = p(x,P1).
91
a(p(P1,E),p(P1,P2)) = p(P1,P2).
92
a(p(P1,E),p(P2,P1)) = p(P2,P2).
93
a(p(P2,P1),p(x,y)) = p(y,x).
94
a(p(P2,E),p(P2,P1)) = p(P1,P2).
95
a(p(E,P2),p(P2,P1)) = p(P2,P1).
96
a(p(E,P1),p(x,x)) = p(P1,x).
97
a(p(E,P2),p(x,x)) = p(P1,x).
98
a(a(p(A,P2),K(P1)),P1) = P1.
99
a(A,a(P2,x)) = a(P2,a(A,x)).
100
a(E,p(p(P1,P2),p(x,x))) = P2.
101
a(E,a(p(P2,P1),f(P1,P2))) = P2.
102
a(E,a(p(P2,P1),f(P2,P1))) = P2.
103
a(E,p(p(x,x),p(P1,P2))) = P2.
104
a(E,a(p(E,P1),p(x,P2))) = P2.
105
a(E,a(p(P1,E),p(x,P2))) = P2.
106
a(p(P2,P2),p(x,E)) = p(E,E).
107
a(p(P1,P1),p(E,x)) = p(E,E).
108
a(a(A,K(x)),p(P1,P2)) = x.
109
a(p(P2,P2),p(x,A)) = p(A,A).
110
a(p(P1,P1),p(A,x)) = p(A,A).
111
a(E,p(A,p(x,x))) = P2.
112
a(E,p(p(P2,P1),p(x,x))) = P2.
113
a(E,p(f(P1,P2),p(x,x))) = P2.
114
a(E,p(f(P2,P1),p(x,x))) = P2.
115
a(E,p(p(E,P1),p(x,x))) = P2.
116
a(E,p(p(E,P2),p(x,x))) = P2.
117
a(E,p(p(P1,E),p(x,x))) = P2.
118
a(E,p(p(P2,E),p(x,x))) = P2.
119
a(E,p(p(P1,A),p(x,x))) = P2.
120
a(E,p(p(A,P1),p(x,x))) = P2.
121
a(E,p(p(P2,A),p(x,x))) = P2.
122
a(E,p(p(A,P2),p(x,x))) = P2.
123
a(E,p(P1,p(x,x))) = P2.
124
a(E,p(P2,p(x,x))) = P2.
125
a(E,a(A,p(A,p(x,x)))) = P2.
126
a(E,a(p(A,p(x,x)),A)) = P2.
127
a(E,p(E,p(x,x))) = P2.
128
a(E,p(K(P2),p(x,x))) = P2.
129
a(E,a(p(A,p(x,x)),P2)) = P2.
130
a(E,a(A,p(P2,p(x,x)))) = P2.
131
a(E,p(p(x,x),A)) = P2.
132
a(E,p(p(x,x),p(P2,A))) = P2.
133
a(E,p(p(x,x),p(A,P2))) = P2.
134
a(E,p(p(x,x),p(P1,A))) = P2.
135
a(E,p(p(x,x),P1)) = P2.
136
a(E,p(p(x,x),P2)) = P2.
137
a(E,p(p(x,x),p(A,P1))) = P2.
138
a(E,p(p(x,x),p(E,P1))) = P2.
139
a(E,p(p(x,x),p(P1,E))) = P2.
140
a(E,p(p(x,x),p(E,P2))) = P2.
141
a(E,p(p(x,x),p(P2,E))) = P2.
142
a(E,p(p(x,x),f(P1,P2))) = P2.
143
a(E,p(p(x,x),f(P2,P1))) = P2.
144
a(E,p(p(x,x),p(P2,P1))) = P2.
145
a(E,p(p(x,x),p(E,A))) = P2.
146
a(E,p(p(x,x),K(P2))) = P2.
147
a(E,p(p(x,x),E)) = P2.
148
a(E,a(p(p(x,x),A),P2)) = P2.
149
a(E,a(A,p(p(x,x),P2))) = P2.
150
a(E,p(p(A,E),p(x,x))) = P2.
151
a(E,p(p(x,x),p(A,E))) = P2.
152
a(E,p(K(K(P2)),p(x,x))) = P2.
153
a(E,p(p(x,x),K(K(P2)))) = P2.
154
a(E,p(K(E),p(x,x))) = P2.
155
a(E,p(K(P1),p(x,x))) = P2.
156
a(E,p(K(A),p(x,x))) = P2.
157
a(E,a(A,p(E,p(x,x)))) = P2.
158
a(E,a(p(A,p(x,x)),E)) = P2.
159
a(E,p(p(x,x),K(E))) = P2.
160
a(E,p(p(x,x),K(P1))) = P2.
161
a(E,p(p(x,x),K(A))) = P2.
162
a(E,a(p(A,p(x,x)),P1)) = P2.
163
a(E,a(A,p(P1,p(x,x)))) = P2.
164
a(E,a(p(p(x,x),A),E)) = P2.
165
a(E,a(A,p(p(x,x),E))) = P2.
166
a(E,a(p(p(x,x),A),P1)) = P2.
167
a(E,a(A,p(p(x,x),P1))) = P2.
168
a(E,a(p(p(x,x),A),A)) = P2.
169
a(E,a(A,p(p(x,x),A))) = P2.
170
a(E,a(p(p(x,x),P2),A)) = P2.
171
a(E,a(p(P2,p(x,x)),A)) = P2.
172
a(E,p(p(E,A),p(x,x))) = P2.
173
a(a(A,K(A)),P2) = a(P2,A).
178
a(p(E,E),p(P2,E)) = p(P2,P2).
179
a(p(P1,E),p(P2,E)) = p(P2,P2).
180
a(p(P2,E),p(P2,E)) = p(E,P2).
181
a(p(P1,E),p(E,P2)) = p(E,P2).
182
a(p(P2,E),p(E,P2)) = p(P2,P2).
183
a(p(E,E),p(P2,A)) = p(P2,P2).
184
a(p(P1,E),p(P2,A)) = p(P2,P2).
185
a(p(P2,E),p(P2,A)) = p(A,P2).
186
a(p(P1,E),p(A,P2)) = p(A,P2).
187
a(p(P2,E),p(A,P2)) = p(P2,P2).
190
a(E,p(P1,K(x))) = P2.
191
a(E,p(P2,K(x))) = P2.
192
a(E,p(K(x),P2)) = P2.
193
a(E,a(p(A,P2),K(P1))) = P2.
194
a(E,a(p(A,P1),K(P1))) = P2.
195
a(E,a(p(A,P2),K(P2))) = P2.
196
a(E,a(p(A,P1),K(P2))) = P2.
197
a(E,a(p(K(E),P1),K(x))) = P2.
198
a(E,a(p(K(E),P2),K(x))) = P2.
199
a(E,p(E,p(K(x),K(y)))) = P2.
200
a(E,a(p(K(A),P1),K(x))) = P2.
201
a(E,a(p(K(A),P2),K(x))) = P2.
202
a(E,a(p(K(P1),P1),K(x))) = P2.
205
a(E,p(K(x),P1)) = P2.
206
a(E,a(p(P2,A),K(P1))) = P2.
207
a(E,a(p(P1,A),K(P1))) = P2.
208
a(E,a(p(K(P1),P2),K(x))) = P2.
209
a(E,a(p(K(P2),P1),K(x))) = P2.
210
a(E,a(p(K(P2),P2),K(x))) = P2.
211
a(E,a(p(P1,K(P2)),K(x))) = P2.
212
a(E,a(p(P1,A),K(P2))) = P2.
213
a(E,a(p(P2,K(P2)),K(x))) = P2.
214
a(E,a(p(P2,A),K(P2))) = P2.
215
a(E,a(p(P1,K(E)),K(x))) = P2.
216
a(E,p(K(P1),K(P2))) = P2.
217
a(E,p(K(P2),K(P1))) = P2.
218
a(E,a(p(P2,K(E)),K(x))) = P2.
219
a(E,p(p(K(x),K(y)),E)) = P2.
220
a(E,a(p(P1,K(A)),K(x))) = P2.
221
a(E,a(p(P2,K(A)),K(x))) = P2.
222
a(E,a(p(P1,K(P1)),K(x))) = P2.
223
a(E,a(p(P2,K(P1)),K(x))) = P2.
224
a(E,p(K(P2),K(E))) = P2.
225
a(E,p(K(E),K(P2))) = P2.
226
a(E,p(K(A),K(P2))) = P2.
227
a(E,p(K(P2),K(A))) = P2.
230
a(p(E,E),p(A,P1)) = p(P2,P2).
231
a(p(P1,E),p(A,P1)) = p(A,P2).
232
a(p(P2,E),p(A,P1)) = p(P1,P2).
233
a(p(E,P1),p(A,P1)) = p(P2,A).
234
a(p(E,P2),p(A,P1)) = p(P2,P1).
235
a(E,p(p(P2,x),K(y))) = P2.
236
a(E,p(K(x),p(P2,y))) = P2.
239
a(p(E,E),p(P1,A)) = p(P2,P2).
240
a(p(P1,E),p(P1,A)) = p(P1,P2).
241
a(E,p(p(x,P2),K(y))) = P2.
242
a(E,p(K(x),p(y,P2))) = P2.
243
a(p(P2,E),p(P1,A)) = p(A,P2).
244
a(p(E,P1),p(P1,A)) = p(P2,P1).
245
a(p(E,P2),p(P1,A)) = p(P2,A).
246
a(p(E,E),p(E,P1)) = p(P2,P2).
247
a(p(P1,E),p(E,P1)) = p(E,P2).
248
a(p(P2,E),p(E,P1)) = p(P1,P2).
249
a(p(E,P1),p(E,P1)) = p(P2,E).
250
a(p(E,P2),p(E,P1)) = p(P2,P1).
251
a(p(E,E),p(P1,E)) = p(P2,P2).
252
a(p(P1,E),p(P1,E)) = p(P1,P2).
253
a(p(P2,E),p(P1,E)) = p(E,P2).
254
a(p(E,P1),p(P1,E)) = p(P2,P1).
255
a(p(E,P2),p(P1,E)) = p(P2,E).
256
a(E,a(A,p(K(P2),A))) = P2.
257
a(E,a(a(A,p(P2,A)),x)) = P2.
258
a(E,a(A,p(K(P2),K(E)))) = P2.
259
a(E,a(A,a(A,p(P2,E)))) = P2.
260
a(E,a(A,a(A,p(P2,A)))) = P2.
261
a(E,a(A,p(A,K(P2)))) = P2.
262
a(E,a(a(A,p(A,P2)),x)) = P2.
263
a(E,a(A,p(K(E),K(P2)))) = P2.
264
a(E,a(A,a(A,p(E,P2)))) = P2.
265
a(E,p(p(x,P2),P1)) = P2.
266
a(E,p(p(P2,x),P1)) = P2.
267
a(E,a(A,p(P2,A))) = P2.
268
a(E,a(A,p(A,P2))) = P2.
269
a(E,p(P1,p(x,P2))) = P2.
270
a(E,p(P1,p(P2,x))) = P2.
271
a(E,a(A,p(A,K(P1)))) = P2.
272
a(E,a(A,p(E,K(P1)))) = P2.
273
a(E,p(p(x,P1),P2)) = P2.
274
a(E,p(p(P1,x),P2)) = P2.
275
a(E,p(P2,p(x,P1))) = P2.
276
a(E,p(P2,p(P1,x))) = P2.
277
a(E,a(A,p(K(P1),A))) = P2.
278
a(E,a(A,p(K(P1),E))) = P2.
279
a(E,a(A,a(A,p(A,P2)))) = P2.
280
a(E,a(a(A,p(A,P1)),x)) = P2.
281
a(E,a(A,a(A,p(A,P1)))) = P2.
282
a(E,a(A,a(A,p(E,P1)))) = P2.
283
a(E,a(a(A,p(P1,A)),x)) = P2.
284
a(E,a(A,a(A,p(P1,A)))) = P2.
285
a(E,a(A,a(A,p(P1,E)))) = P2.
286
a(E,p(K(P2),p(x,K(P1)))) = P2.
287
a(E,p(p(x,K(P1)),K(P2))) = P2.
288
a(E,p(K(P2),p(K(P1),x))) = P2.
289
a(E,p(p(K(P1),x),K(P2))) = P2.
292
a(E,p(p(P1,x),E)) = P2.
293
a(E,p(p(x,P1),E)) = P2.
294
a(E,p(E,p(P1,x))) = P2.
295
a(E,p(E,p(x,P1))) = P2.
296
a(E,p(P2,p(x,E))) = P2.
297
a(E,p(p(x,E),P2)) = P2.
298
a(E,p(P1,p(x,E))) = P2.
299
a(E,p(p(x,E),P1)) = P2.
300
a(E,a(p(A,K(E)),A)) = P2.
301
a(E,a(p(K(E),A),A)) = P2.
302
a(E,p(p(P2,x),E)) = P2.
303
a(E,p(p(x,P2),E)) = P2.
304
a(E,p(E,p(P2,x))) = P2.
305
a(E,p(E,p(x,P2))) = P2.
306
a(E,p(P2,p(E,x))) = P2.
307
a(E,p(p(E,x),P2)) = P2.
308
a(E,p(P1,p(E,x))) = P2.
309
a(E,p(p(E,x),P1)) = P2.
310
a(E,p(p(K(P1),x),E)) = P2.
311
a(E,p(p(x,K(P1)),E)) = P2.
312
a(E,p(p(K(E),x),E)) = P2.
313
a(E,p(p(x,K(E)),E)) = P2.
314
a(E,p(E,p(K(P1),x))) = P2.
315
a(E,p(E,p(x,K(P1)))) = P2.
316
a(E,p(E,p(K(E),x))) = P2.
317
a(E,p(E,p(x,K(E)))) = P2.
318
a(E,a(p(A,K(E)),E)) = P2.
319
a(E,a(p(K(E),A),E)) = P2.
320
a(E,p(K(P2),p(x,K(E)))) = P2.
321
a(E,p(p(x,K(E)),K(P2))) = P2.
322
a(E,p(K(P2),p(K(E),x))) = P2.
323
a(E,p(p(K(E),x),K(P2))) = P2.
324
a(E,a(p(A,p(P1,P2)),E)) = P2.
325
a(E,a(p(p(P1,P2),A),E)) = P2.
326
a(E,p(K(P2),K(K(x)))) = P2.
327
a(E,p(K(K(x)),K(P2))) = P2.
328
a(E,a(A,p(K(x),P2))) = P2.
329
a(E,a(A,p(K(P2),K(A)))) = P2.
330
a(E,a(A,p(K(A),K(P2)))) = P2.
331
a(E,a(A,p(K(P1),K(A)))) = P2.
332
a(E,a(A,p(K(A),K(P1)))) = P2.
333
a(E,a(p(A,E),p(P2,A))) = P2.
334
a(E,a(p(A,E),p(A,P2))) = P2.
335
a(E,a(A,p(P2,K(x)))) = P2.
336
a(p(E,E),p(A,E)) = p(P2,P2).
337
a(p(P1,E),p(A,E)) = p(A,P2).
338
a(p(P2,E),p(A,E)) = p(E,P2).
339
a(p(E,P1),p(A,E)) = p(P2,A).
340
a(p(E,P2),p(A,E)) = p(P2,E).
341
a(p(E,E),p(E,A)) = p(P2,P2).
342
a(p(P1,E),p(E,A)) = p(E,P2).
343
a(p(P2,E),p(E,A)) = p(A,P2).
344
a(p(E,P1),p(E,A)) = p(P2,E).
345
a(p(E,P2),p(E,A)) = p(P2,A).
346
a(E,a(A,p(P2,p(x,P1)))) = P2.
347
a(E,a(A,p(p(x,P1),P2))) = P2.
348
a(E,a(A,p(P2,p(P1,x)))) = P2.
349
a(E,a(A,p(p(P1,x),P2))) = P2.
350
a(E,p(K(a(A,A)),K(P2))) = P2.
351
a(E,p(K(P2),K(a(A,A)))) = P2.
352
a(E,a(a(A,p(E,P1)),P2)) = P2.
353
a(E,a(a(A,p(P1,E)),P2)) = P2.
354
a(E,a(a(A,p(E,P2)),P1)) = P2.
355
a(E,a(A,p(P2,E))) = P2.
356
a(E,a(A,p(E,P2))) = P2.
357
a(E,a(a(A,p(P2,E)),P1)) = P2.
358
a(E,p(p(x,K(P2)),E)) = P2.
359
a(E,p(E,p(x,K(P2)))) = P2.
360
a(E,p(p(K(P2),x),E)) = P2.
361
a(E,p(E,p(K(P2),x))) = P2.
362
a(E,a(p(P1,A),P2)) = P2.
363
a(E,a(p(P2,A),P2)) = P2.
364
a(E,a(p(A,P1),P2)) = P2.
365
a(E,a(p(A,P2),P2)) = P2.
366
a(E,a(a(A,p(E,P1)),P1)) = P2.
367
a(E,a(a(A,p(P1,E)),P1)) = P2.
368
a(E,a(a(A,p(E,P2)),P2)) = P2.
369
a(E,a(a(A,p(P2,E)),P2)) = P2.
370
a(E,a(p(A,p(x,P1)),P2)) = P2.
371
a(E,a(p(p(x,P1),A),P2)) = P2.
372
a(E,p(p(A,x),P2)) = P2.
373
a(E,p(P2,p(A,x))) = P2.
374
a(E,a(A,p(K(E),K(P1)))) = P2.
375
a(E,p(E,p(K(A),x))) = P2.
376
a(E,p(p(K(A),x),E)) = P2.
377
a(E,p(K(P2),p(K(A),x))) = P2.
378
a(E,p(p(K(A),x),K(P2))) = P2.
379
a(E,a(p(K(A),A),A)) = P2.
380
a(E,a(p(A,K(A)),A)) = P2.
381
a(E,a(A,p(K(P1),K(E)))) = P2.
382
a(E,a(p(A,p(x,P2)),P2)) = P2.
383
a(E,a(p(p(x,P2),A),P2)) = P2.
384
a(E,a(p(A,p(P1,x)),P2)) = P2.
385
a(E,a(p(p(P1,x),A),P2)) = P2.
386
a(E,a(A,p(P2,p(A,x)))) = P2.
387
a(E,a(A,p(p(A,x),P2))) = P2.
388
a(E,a(p(A,K(A)),E)) = P2.
389
a(E,a(p(K(A),A),E)) = P2.
390
a(E,p(p(A,x),P1)) = P2.
391
a(E,p(P1,p(A,x))) = P2.
392
a(E,p(p(x,A),P1)) = P2.
393
a(E,p(P1,p(x,A))) = P2.
394
a(E,p(p(x,A),P2)) = P2.
395
a(E,p(P2,p(x,A))) = P2.
396
a(E,p(E,p(x,K(A)))) = P2.
397
a(E,p(p(x,K(A)),E)) = P2.
398
a(E,p(K(P2),p(x,K(A)))) = P2.
399
a(E,p(p(x,K(A)),K(P2))) = P2.
400
a(E,p(K(K(x)),K(E))) = P2.
401
a(E,p(K(K(x)),K(A))) = P2.
402
a(E,p(K(K(x)),K(P1))) = P2.
403
a(E,p(K(E),K(K(x)))) = P2.
404
a(E,p(K(A),K(K(x)))) = P2.
405
a(E,p(K(P1),K(K(x)))) = P2.
406
a(E,p(K(K(P2)),K(K(P1)))) = P2.
407
a(E,p(K(K(P1)),K(K(P2)))) = P2.
408
a(E,p(K(K(E)),K(K(P2)))) = P2.
409
a(E,p(K(K(P2)),K(K(E)))) = P2.
410
a(E,p(K(K(P2)),K(K(A)))) = P2.
411
a(E,p(K(K(A)),K(K(P2)))) = P2.
412
a(E,p(p(P1,x),p(P2,y))) = P2.
413
a(E,p(p(P2,x),p(P1,y))) = P2.
414
a(E,p(p(x,P1),p(y,P2))) = P2.
415
a(E,p(p(x,P2),p(y,P1))) = P2.
416
a(E,p(A,p(x,E))) = P2.
417
a(E,p(P2,p(x,P2))) = P2.
418
a(E,p(P1,p(x,P1))) = P2.
419
a(E,p(p(P1,x),P1)) = P2.
420
a(E,p(p(P2,x),P2)) = P2.
421
a(E,p(p(x,P1),P1)) = P2.
422
a(E,p(p(x,P2),P2)) = P2.
423
a(E,p(A,p(x,P1))) = P2.
424
a(E,p(p(x,P1),A)) = P2.
425
a(E,p(A,p(x,P2))) = P2.
426
a(E,p(p(x,P2),A)) = P2.
427
a(E,p(p(P1,x),A)) = P2.
428
a(E,p(A,p(P1,x))) = P2.
429
a(E,p(p(x,E),A)) = P2.
430
a(E,p(P1,p(P1,x))) = P2.
431
a(E,p(P2,p(P2,x))) = P2.
432
a(E,p(E,p(E,x))) = P2.
433
a(E,p(p(E,x),E)) = P2.
434
a(E,p(E,p(x,E))) = P2.
435
a(E,p(p(x,E),E)) = P2.
436
a(E,p(K(K(E)),p(x,x))) = P2.
437
a(E,p(K(K(P1)),p(x,x))) = P2.
438
a(E,p(K(K(A)),p(x,x))) = P2.
439
a(E,p(p(x,x),K(K(E)))) = P2.
440
a(E,p(p(A,x),A)) = P2.
441
a(E,p(p(x,A),A)) = P2.
442
a(E,p(A,p(A,x))) = P2.
443
a(E,p(A,p(x,A))) = P2.
444
a(E,p(p(x,x),K(K(P1)))) = P2.
445
a(E,p(p(x,x),K(K(A)))) = P2.
446
a(E,p(p(x,K(P2)),K(P1))) = P2.
447
a(E,p(p(K(P2),x),K(P1))) = P2.
448
a(E,p(K(P1),p(x,K(P2)))) = P2.
449
a(E,p(K(P1),p(K(P2),x))) = P2.
450
a(E,p(p(K(P1),x),K(E))) = P2.
451
a(E,p(p(x,K(P1)),K(E))) = P2.
452
a(E,p(K(E),p(K(P1),x))) = P2.
453
a(E,p(K(E),p(x,K(P1)))) = P2.
454
a(E,p(K(P1),p(x,K(E)))) = P2.
455
a(E,p(p(x,K(E)),K(P1))) = P2.
456
a(E,p(p(K(P2),x),K(E))) = P2.
457
a(E,p(p(x,K(P2)),K(E))) = P2.
458
a(E,p(K(E),p(K(P2),x))) = P2.
459
a(E,p(K(E),p(x,K(P2)))) = P2.
460
a(E,p(K(P1),p(K(E),x))) = P2.
461
a(E,p(p(K(E),x),K(P1))) = P2.
462
a(E,p(p(K(A),x),K(P1))) = P2.
463
a(E,p(K(P1),p(K(A),x))) = P2.
464
a(E,p(p(x,K(A)),K(P1))) = P2.
465
a(E,p(K(P1),p(x,K(A)))) = P2.
466
a(E,p(K(P2),p(K(P2),x))) = P2.
467
a(E,p(p(K(P2),x),K(P2))) = P2.
468
a(E,p(K(P2),p(x,K(P2)))) = P2.
469
a(E,p(p(x,K(P2)),K(P2))) = P2.
470
a(E,a(A,p(P2,p(P2,x)))) = P2.
471
a(E,a(A,p(p(P2,x),P2))) = P2.
472
a(E,a(p(A,p(A,x)),P2)) = P2.
473
a(E,a(p(p(A,x),A),P2)) = P2.
474
a(E,a(A,p(P2,p(x,P2)))) = P2.
475
a(E,a(A,p(p(x,P2),P2))) = P2.
476
a(E,a(p(A,p(x,A)),P2)) = P2.
477
a(E,a(p(p(x,A),A),P2)) = P2.
478
a(E,p(K(P1),K(A))) = P2.
479
a(E,p(K(A),K(P1))) = P2.
480
a(E,p(K(E),K(P1))) = P2.
481
a(E,p(K(P1),K(E))) = P2.
482
a(E,p(K(P1),K(a(A,A)))) = P2.
483
a(E,p(K(a(A,A)),K(P1))) = P2.
484
a(E,p(K(A),p(x,K(E)))) = P2.
485
a(E,p(p(x,K(E)),K(A))) = P2.
486
a(E,p(K(P1),p(x,K(P1)))) = P2.
487
a(E,p(p(x,K(P1)),K(P1))) = P2.
488
a(E,p(p(K(P1),x),K(P1))) = P2.
489
a(E,p(K(P1),p(K(P1),x))) = P2.
490
a(E,p(K(A),p(x,K(P1)))) = P2.
491
a(E,p(p(x,K(P1)),K(A))) = P2.
492
a(E,p(K(A),p(x,K(P2)))) = P2.
493
a(E,p(p(x,K(P2)),K(A))) = P2.
494
a(E,p(p(K(P1),x),K(A))) = P2.
495
a(E,p(K(A),p(K(P1),x))) = P2.
496
a(E,p(K(E),p(K(E),x))) = P2.
497
a(E,p(p(K(E),x),K(E))) = P2.
498
a(E,p(K(E),p(x,K(E)))) = P2.
499
a(E,p(p(x,K(E)),K(E))) = P2.
500
a(E,p(p(K(A),x),K(A))) = P2.
501
a(E,p(K(A),p(K(A),x))) = P2.
502
a(E,p(p(x,K(A)),K(A))) = P2.
503
a(E,p(K(A),p(x,K(A)))) = P2.
504
a(a(p(P1,A),K(A)),P2) = A.
505
a(E,a(p(A,P2),p(x,A))) = P2.
506
a(E,a(p(A,P1),p(A,x))) = P2.
507
a(E,a(p(P2,A),p(x,A))) = P2.
508
a(E,a(p(P1,A),p(A,x))) = P2.
509
a(E,a(A,p(E,K(K(x))))) = P2.
510
a(E,a(A,p(A,K(K(x))))) = P2.
511
a(E,a(A,p(E,P1))) = P2.
512
a(E,a(A,p(K(K(x)),E))) = P2.
513
a(E,a(A,p(K(K(x)),A))) = P2.
514
a(E,a(A,p(P1,E))) = P2.
515
a(E,a(a(A,p(E,P1)),A)) = P2.
516
a(E,a(a(A,p(P1,E)),A)) = P2.
517
a(E,a(a(A,p(E,P2)),A)) = P2.
518
a(E,a(a(A,p(P2,E)),A)) = P2.
519
a(E,a(p(A,K(E)),K(x))) = P2.
520
a(E,a(p(P1,K(E)),P1)) = P2.
521
a(E,a(p(P1,K(E)),P2)) = P2.
522
a(E,a(p(P2,K(E)),P1)) = P2.
523
a(E,a(p(P2,K(E)),P2)) = P2.
524
a(E,a(p(K(E),A),K(x))) = P2.
525
a(E,a(p(K(E),P1),P1)) = P2.
526
a(E,a(p(K(E),P1),P2)) = P2.
527
a(E,a(p(K(E),P2),P1)) = P2.
528
a(E,a(p(K(E),P2),P2)) = P2.
529
a(E,p(E,p(A,x))) = P2.
530
a(E,p(p(A,x),E)) = P2.
531
a(E,p(K(E),p(K(A),x))) = P2.
532
a(E,p(p(K(A),x),K(E))) = P2.
533
a(E,p(p(P2,x),A)) = P2.
534
a(E,p(A,p(P2,x))) = P2.
535
a(E,p(p(K(P2),x),K(A))) = P2.
536
a(E,p(K(A),p(K(P2),x))) = P2.
537
a(E,a(p(A,p(P2,x)),P2)) = P2.
538
a(E,a(p(p(P2,x),A),P2)) = P2.
539
a(E,a(A,p(p(x,P2),P1))) = P2.
540
a(E,a(A,p(p(P2,x),P1))) = P2.
541
a(E,a(A,p(P1,p(x,P2)))) = P2.
542
a(E,a(A,p(P1,p(P2,x)))) = P2.
543
a(E,a(p(A,p(x,A)),P1)) = P2.
544
a(E,a(A,p(P1,p(x,P1)))) = P2.
545
a(E,a(p(p(x,A),A),P1)) = P2.
546
a(E,a(A,p(p(x,P1),P1))) = P2.
547
a(E,a(p(p(A,x),A),P1)) = P2.
548
a(E,a(A,p(p(P1,x),P1))) = P2.
549
a(E,a(p(A,p(A,x)),P1)) = P2.
550
a(E,a(A,p(P1,p(P1,x)))) = P2.
551
a(E,p(E,p(x,A))) = P2.
552
a(E,p(p(x,A),E)) = P2.
553
a(E,p(K(E),p(x,K(A)))) = P2.
554
a(E,p(p(x,K(A)),K(E))) = P2.
555
a(E,a(A,p(P2,p(x,A)))) = P2.
556
a(E,a(A,p(p(x,A),P2))) = P2.
557
a(E,p(K(P2),K(a(A,E)))) = P2.
558
a(E,p(K(a(A,E)),K(P2))) = P2.
559
a(E,a(A,p(E,K(P2)))) = P2.
560
a(E,a(A,p(K(P2),E))) = P2.
561
a(E,p(K(E),K(A))) = P2.
562
a(E,p(K(A),K(E))) = P2.
563
a(E,p(K(K(A)),K(K(P1)))) = P2.
564
a(E,p(K(K(P1)),K(K(A)))) = P2.
565
a(E,p(K(K(P1)),K(K(E)))) = P2.
566
a(E,p(K(K(E)),K(K(P1)))) = P2.
567
a(E,p(K(K(A)),K(K(E)))) = P2.
568
a(E,p(K(K(E)),K(K(A)))) = P2.
569
a(E,p(K(a(A,E)),K(P1))) = P2.
570
a(E,p(K(P1),K(a(A,E)))) = P2.
571
a(E,p(K(E),K(a(A,A)))) = P2.
572
a(E,p(K(E),K(a(A,E)))) = P2.
573
a(E,p(K(a(A,A)),K(E))) = P2.
574
a(E,p(K(a(A,E)),K(E))) = P2.
575
a(E,a(p(K(P2),P2),A)) = P2.
576
a(E,a(p(P2,K(P2)),A)) = P2.
577
a(E,a(p(K(K(P2)),P1),A)) = P2.
578
a(E,a(p(P1,K(K(P2))),A)) = P2.
579
a(E,p(K(a(A,E)),K(A))) = P2.
580
a(E,p(K(A),K(a(A,E)))) = P2.
581
a(E,p(K(A),K(a(A,A)))) = P2.
582
a(E,p(K(a(A,A)),K(A))) = P2.
583
a(E,a(p(K(K(P2)),P2),A)) = P2.
584
a(E,a(p(P2,K(K(P2))),A)) = P2.
585
a(E,a(p(P1,K(P2)),A)) = P2.
586
a(E,a(p(K(P2),P1),A)) = P2.
587
a(E,p(A,p(E,x))) = P2.
588
a(E,p(p(E,x),A)) = P2.
589
a(E,p(K(A),p(K(E),x))) = P2.
590
a(E,p(p(K(E),x),K(A))) = P2.
591
a(E,a(p(E,A),p(P1,E))) = P2.
592
a(E,a(p(A,E),p(P1,E))) = P2.
593
a(E,a(p(A,E),p(E,P1))) = P2.
594
a(E,a(p(A,K(A)),K(x))) = P2.
595
a(E,a(p(P1,K(A)),P1)) = P2.
596
a(E,a(p(P1,K(A)),P2)) = P2.
597
a(E,a(p(P2,K(A)),P2)) = P2.
598
a(E,a(p(K(A),A),K(x))) = P2.
599
a(E,a(p(P2,K(A)),P1)) = P2.
600
a(E,a(p(K(A),P1),P1)) = P2.
601
a(E,a(p(K(A),P1),P2)) = P2.
602
a(E,a(p(K(A),P2),P2)) = P2.
603
a(E,a(p(K(A),P2),P1)) = P2.
604
a(E,p(P2,p(x,p(y,E)))) = P2.
605
a(E,p(p(x,p(y,E)),P2)) = P2.
606
a(E,p(P2,p(x,p(E,y)))) = P2.
607
a(E,p(p(x,p(E,y)),P2)) = P2.
608
a(E,p(P2,p(p(x,E),y))) = P2.
609
a(E,p(p(p(x,E),y),P2)) = P2.
610
a(E,p(P2,p(p(E,x),y))) = P2.
611
a(E,p(p(p(E,x),y),P2)) = P2.
612
a(E,a(A,p(p(x,E),P2))) = P2.
613
a(E,a(A,p(p(E,x),P2))) = P2.
614
a(E,p(E,p(x,p(y,P1)))) = P2.
615
a(E,p(p(x,p(y,P1)),E)) = P2.
616
a(E,p(P2,p(x,p(y,P1)))) = P2.
617
a(E,p(p(x,p(y,P1)),P2)) = P2.
618
a(E,p(P1,p(x,p(y,E)))) = P2.
619
a(E,p(p(x,p(y,E)),P1)) = P2.
620
a(E,p(E,p(x,p(y,P2)))) = P2.
621
a(E,p(p(x,p(y,P2)),E)) = P2.
622
a(E,p(P1,p(x,p(y,P2)))) = P2.
623
a(E,p(p(x,p(y,P2)),P1)) = P2.
624
a(E,p(E,p(x,p(P1,y)))) = P2.
625
a(E,p(p(x,p(P1,y)),E)) = P2.
626
a(E,p(P2,p(x,p(P1,y)))) = P2.
627
a(E,p(p(x,p(P1,y)),P2)) = P2.
628
a(E,p(E,p(x,p(P2,y)))) = P2.
629
a(E,p(p(x,p(P2,y)),E)) = P2.
630
a(E,p(P1,p(x,p(P2,y)))) = P2.
631
a(E,p(p(x,p(P2,y)),P1)) = P2.
632
a(E,p(E,p(p(x,P1),y))) = P2.
633
a(E,p(p(p(x,P1),y),E)) = P2.
634
a(E,p(P2,p(p(x,P1),y))) = P2.
635
a(E,p(p(p(x,P1),y),P2)) = P2.
636
a(E,p(P1,p(p(x,E),y))) = P2.
637
a(E,p(p(p(x,E),y),P1)) = P2.
638
a(E,p(E,p(p(x,P2),y))) = P2.
639
a(E,p(p(p(x,P2),y),E)) = P2.
640
a(E,p(P1,p(p(x,P2),y))) = P2.
641
a(E,p(p(p(x,P2),y),P1)) = P2.
642
a(E,p(E,p(p(P1,x),y))) = P2.
643
a(E,p(p(p(P1,x),y),E)) = P2.
644
a(E,p(P2,p(p(P1,x),y))) = P2.
645
a(E,p(p(p(P1,x),y),P2)) = P2.
646
a(E,p(P1,p(p(E,x),y))) = P2.
647
a(E,p(p(p(E,x),y),P1)) = P2.
648
a(E,p(E,p(p(P2,x),y))) = P2.
649
a(E,p(p(p(P2,x),y),E)) = P2.
650
a(E,p(P1,p(p(P2,x),y))) = P2.
651
a(E,p(p(p(P2,x),y),P1)) = P2.
652
a(E,p(P1,p(x,p(E,y)))) = P2.
653
a(E,p(p(x,p(E,y)),P1)) = P2.
654
a(E,a(A,p(A,P1))) = P2.
655
a(E,a(A,p(K(x),P1))) = P2.
656
a(E,a(p(P1,A),P1)) = P2.
657
a(E,a(p(P1,K(K(P1))),P2)) = P2.
658
a(E,a(p(P2,K(K(P1))),P2)) = P2.
659
a(E,a(p(P2,A),P1)) = P2.
660
a(E,a(A,p(A,p(P1,P2)))) = P2.
661
a(E,a(p(A,K(K(A))),E)) = P2.
662
a(E,a(p(A,K(K(E))),E)) = P2.
663
a(E,p(p(E,x),K(y))) = P2.
664
a(E,p(p(A,x),K(y))) = P2.
665
a(E,p(K(x),p(E,y))) = P2.
666
a(E,p(K(x),p(A,y))) = P2.
667
a(E,p(p(P1,x),K(y))) = P2.
668
a(E,p(K(x),p(P1,y))) = P2.
669
a(E,p(p(x,E),K(y))) = P2.
670
a(E,p(p(x,A),K(y))) = P2.
671
a(E,p(K(x),p(y,E))) = P2.
672
a(E,p(K(x),p(y,A))) = P2.
673
a(E,p(p(x,P1),K(y))) = P2.
674
a(E,p(K(x),p(y,P1))) = P2.
675
a(E,a(p(A,K(K(x))),A)) = P2.
676
a(E,a(p(P1,K(K(E))),P2)) = P2.
677
a(E,a(p(P2,K(K(E))),P2)) = P2.
678
a(E,K(f(P1,P2))) = P2.
679
a(E,K(f(P2,P1))) = P2.
680
a(a(A,K(A)),P1) = a(P1,A).
681
a(a(p(A,P2),K(A)),P1) = A.
682
a(E,a(A,p(P2,p(x,E)))) = P2.
683
a(E,a(A,p(P2,p(E,x)))) = P2.
684
a(E,a(A,p(P1,A))) = P2.
685
a(E,a(A,p(P1,K(x)))) = P2.
686
a(E,a(p(A,P1),P1)) = P2.
687
a(E,a(p(K(K(P1)),P1),P2)) = P2.
688
a(E,a(p(K(K(P1)),P2),P2)) = P2.
689
a(E,a(p(A,P2),P1)) = P2.
690
a(E,a(A,p(p(P1,P2),A))) = P2.
691
a(E,a(p(K(K(A)),A),E)) = P2.
692
a(E,a(p(K(K(E)),A),E)) = P2.
693
a(E,a(p(K(K(E)),P1),P2)) = P2.
694
a(E,a(p(K(K(E)),P2),P2)) = P2.
695
a(E,a(p(K(K(x)),A),A)) = P2.
696
a(E,p(P2,p(x,p(P2,y)))) = P2.
697
a(E,p(p(x,p(P2,y)),P2)) = P2.
698
a(E,p(P2,p(p(P2,x),y))) = P2.
699
a(E,p(p(p(P2,x),y),P2)) = P2.
700
a(E,p(P1,p(x,p(P1,y)))) = P2.
701
a(E,p(p(x,p(P1,y)),P1)) = P2.
702
a(E,p(E,p(x,p(E,y)))) = P2.
703
a(E,p(p(x,p(E,y)),E)) = P2.
704
a(E,p(p(x,p(A,y)),A)) = P2.
705
a(E,p(A,p(x,p(A,y)))) = P2.
706
a(E,p(P1,p(p(P1,x),y))) = P2.
707
a(E,p(p(p(P1,x),y),P1)) = P2.
708
a(E,p(p(p(A,x),y),A)) = P2.
709
a(E,p(A,p(p(A,x),y))) = P2.
710
a(E,p(E,p(p(E,x),y))) = P2.
711
a(E,p(p(p(E,x),y),E)) = P2.
712
a(E,p(p(E,x),p(P1,y))) = P2.
713
a(E,p(p(P1,x),p(E,y))) = P2.
714
a(E,p(P2,p(x,p(y,P2)))) = P2.
715
a(E,p(p(x,p(y,P2)),P2)) = P2.
716
a(E,p(P2,p(p(x,P2),y))) = P2.
717
a(E,p(p(p(x,P2),y),P2)) = P2.
718
a(E,p(p(x,p(y,A)),A)) = P2.
719
a(E,p(A,p(x,p(y,A)))) = P2.
720
a(E,p(p(p(x,A),y),A)) = P2.
721
a(E,p(A,p(p(x,A),y))) = P2.
722
a(E,p(E,p(p(x,E),y))) = P2.
723
a(E,p(p(p(x,E),y),E)) = P2.
724
a(E,p(P1,p(x,p(y,P1)))) = P2.
725
a(E,p(p(x,p(y,P1)),P1)) = P2.
726
a(E,p(P1,p(p(x,P1),y))) = P2.
727
a(E,p(p(p(x,P1),y),P1)) = P2.
728
a(E,a(p(A,P1),K(E))) = P2.
729
a(E,a(p(A,P2),K(E))) = P2.
730
a(E,a(p(P1,A),K(E))) = P2.
731
a(E,a(p(P2,A),K(E))) = P2.
732
a(E,a(p(K(E),P1),A)) = P2.
733
a(E,a(p(P1,K(E)),A)) = P2.
734
a(E,a(p(A,p(P1,x)),P1)) = P2.
735
a(E,a(p(p(P1,x),A),P1)) = P2.
736
a(E,a(p(K(P1),P1),A)) = P2.
737
a(E,a(p(P1,K(P1)),A)) = P2.
738
a(E,a(p(K(P1),P2),A)) = P2.
739
a(E,a(p(P2,K(P1)),A)) = P2.
740
a(E,a(p(A,p(P2,x)),P1)) = P2.
741
a(E,a(p(p(P2,x),A),P1)) = P2.
742
a(E,p(p(x,E),p(y,P1))) = P2.
743
a(E,p(p(x,P1),p(y,E))) = P2.
744
a(E,p(p(x,p(y,E)),E)) = P2.
745
a(E,p(E,p(x,p(y,E)))) = P2.
746
a(E,a(p(K(P2),P1),P1)) = P2.
747
a(E,a(p(P1,K(P2)),P1)) = P2.
748
a(E,a(p(K(P1),P1),P2)) = P2.
749
a(E,a(p(P1,K(P1)),P2)) = P2.
750
a(E,a(p(K(P2),P2),P1)) = P2.
751
a(E,a(p(P2,K(P2)),P1)) = P2.
752
a(E,a(p(K(P1),P2),P2)) = P2.
753
a(E,a(p(P2,K(P1)),P2)) = P2.
754
a(E,a(p(p(x,P1),A),P1)) = P2.
755
a(E,a(p(p(x,P2),A),P1)) = P2.
756
a(E,a(A,p(p(E,x),P1))) = P2.
757
a(E,a(A,p(p(x,E),P1))) = P2.
758
a(E,a(p(A,p(x,P1)),P1)) = P2.
759
a(E,a(p(A,p(x,P2)),P1)) = P2.
760
a(E,a(A,p(P1,p(E,x)))) = P2.
761
a(E,a(A,p(P1,p(x,E)))) = P2.
762
a(E,a(p(K(P2),P1),P2)) = P2.
763
a(E,a(p(p(P1,P2),P1),P2)) = P2.
764
a(E,a(p(P1,K(P2)),P2)) = P2.
765
a(E,a(p(P1,p(P1,P2)),P2)) = P2.
766
a(E,a(a(A,p(P2,E)),E)) = P2.
767
a(E,a(a(A,p(E,P2)),E)) = P2.
768
a(E,a(a(A,p(P1,E)),E)) = P2.
769
a(E,a(a(A,p(E,P1)),E)) = P2.
770
a(E,a(p(K(P2),P2),P2)) = P2.
771
a(E,a(p(P2,K(P2)),P2)) = P2.
772
a(E,a(p(p(P1,P2),P2),P2)) = P2.
773
a(E,a(p(P2,p(P1,P2)),P2)) = P2.
774
a(E,a(p(A,P2),A)) = P2.
775
a(E,a(p(P2,A),A)) = P2.
776
a(E,a(p(A,P1),K(K(P2)))) = P2.
777
a(E,a(p(P1,A),K(K(P2)))) = P2.
778
a(E,a(p(A,P2),K(K(P2)))) = P2.
779
a(E,a(p(P2,A),K(K(P2)))) = P2.
780
a(E,a(p(A,P1),p(E,x))) = P2.
781
a(E,a(p(P1,A),p(E,x))) = P2.
782
a(E,p(P2,p(K(x),y))) = P2.
783
a(E,p(p(K(x),y),P2)) = P2.
784
a(E,p(E,p(K(K(x)),y))) = P2.
785
a(E,p(p(K(K(x)),y),E)) = P2.
786
a(E,a(p(P1,K(A)),A)) = P2.
787
a(E,a(p(K(A),P1),A)) = P2.
788
a(E,a(p(P1,p(P1,P2)),A)) = P2.
789
a(E,a(p(p(P1,P2),P1),A)) = P2.
790
a(E,a(p(P1,A),A)) = P2.
791
a(E,a(p(A,P1),A)) = P2.
792
a(E,a(p(P2,K(E)),A)) = P2.
793
a(E,a(p(K(E),P2),A)) = P2.
794
a(E,a(p(P2,K(A)),A)) = P2.
795
a(E,a(p(K(A),P2),A)) = P2.
796
a(E,a(p(P2,p(P1,P2)),A)) = P2.
797
a(E,a(p(p(P1,P2),P2),A)) = P2.
798
a(E,p(E,p(x,K(K(y))))) = P2.
799
a(E,p(p(x,K(K(y))),E)) = P2.
800
a(E,p(P2,p(x,K(y)))) = P2.
801
a(E,p(p(x,K(y)),P2)) = P2.
802
a(E,a(A,p(p(A,x),P1))) = P2.
803
a(E,a(A,p(P1,p(A,x)))) = P2.
804
a(E,K(a(p(P1,A),A))) = P2.
805
a(E,K(a(p(A,P1),A))) = P2.
806
a(E,K(a(p(P2,A),A))) = P2.
807
a(E,K(a(p(A,P2),A))) = P2.
808
a(E,a(A,p(p(x,A),P1))) = P2.
809
a(E,a(A,p(P1,p(x,A)))) = P2.
810
a(E,a(p(P1,p(x,x)),P1)) = P2.
811
a(E,a(p(p(x,x),P1),P1)) = P2.
812
a(E,a(p(A,p(P1,x)),A)) = P2.
813
a(E,a(p(A,p(P2,x)),A)) = P2.
814
a(E,a(p(p(P1,x),A),A)) = P2.
815
a(E,a(p(p(P2,x),A),A)) = P2.
816
a(E,a(A,p(A,p(P2,x)))) = P2.
817
a(E,a(A,p(p(P2,x),A))) = P2.
818
a(E,p(P1,p(p(A,x),y))) = P2.
819
a(E,p(p(p(A,x),y),P1)) = P2.
820
a(E,p(P2,p(p(A,x),y))) = P2.
821
a(E,p(p(p(A,x),y),P2)) = P2.
822
a(E,p(P1,p(x,p(A,y)))) = P2.
823
a(E,p(p(x,p(A,y)),P1)) = P2.
824
a(E,p(P2,p(x,p(A,y)))) = P2.
825
a(E,p(p(x,p(A,y)),P2)) = P2.
826
a(E,p(P1,p(p(x,A),y))) = P2.
827
a(E,p(p(p(x,A),y),P1)) = P2.
828
a(E,p(P2,p(p(x,A),y))) = P2.
829
a(E,p(p(p(x,A),y),P2)) = P2.
830
a(E,p(P1,p(x,p(y,A)))) = P2.
831
a(E,p(p(x,p(y,A)),P1)) = P2.
832
a(E,p(P2,p(x,p(y,A)))) = P2.
833
a(E,p(p(x,p(y,A)),P2)) = P2.
834
a(E,a(p(K(K(P1)),P2),A)) = P2.
835
a(E,a(p(P2,K(K(P1))),A)) = P2.
836
a(E,a(p(K(K(A)),P1),A)) = P2.
837
a(E,a(p(K(K(A)),P2),A)) = P2.
838
a(E,a(p(P1,K(K(A))),A)) = P2.
839
a(E,a(p(P2,K(K(A))),A)) = P2.
840
a(E,a(p(K(K(P1)),P1),A)) = P2.
841
a(E,a(p(P1,K(K(P1))),A)) = P2.
842
a(E,a(p(K(K(E)),P1),A)) = P2.
843
a(E,a(p(K(K(E)),P2),A)) = P2.
844
a(E,a(p(P1,K(K(E))),A)) = P2.
845
a(E,a(p(P2,K(K(E))),A)) = P2.
846
a(E,a(p(K(K(A)),P2),P2)) = P2.
847
a(E,a(p(K(K(A)),P1),P2)) = P2.
848
a(E,a(p(P2,K(K(A))),P2)) = P2.
849
a(E,a(p(P1,K(K(A))),P2)) = P2.
850
a(E,a(p(P1,K(K(x))),P1)) = P2.
851
a(E,a(p(P2,K(K(x))),P1)) = P2.
852
a(E,a(p(P2,p(A,A)),P1)) = P2.
853
a(E,a(p(K(K(x)),P1),P1)) = P2.
854
a(E,a(p(K(K(x)),P2),P1)) = P2.
855
a(E,a(p(p(A,A),P2),P1)) = P2.
856
a(E,p(p(x,P2),p(y,A))) = P2.
857
a(E,p(p(x,A),p(y,P2))) = P2.
858
a(E,p(p(x,P2),p(y,E))) = P2.
859
a(E,p(p(x,E),p(y,P2))) = P2.
860
a(E,p(p(P2,x),p(A,y))) = P2.
861
a(E,p(p(A,x),p(P2,y))) = P2.
862
a(E,p(p(P2,x),p(E,y))) = P2.
863
a(E,p(p(E,x),p(P2,y))) = P2.
864
a(E,p(p(x,p(y,y)),A)) = P2.
865
a(E,p(A,p(x,p(y,y)))) = P2.
866
a(E,p(p(x,p(y,y)),P1)) = P2.
867
a(E,p(P1,p(x,p(y,y)))) = P2.
868
a(E,p(p(x,p(y,y)),P2)) = P2.
869
a(E,p(P2,p(x,p(y,y)))) = P2.
870
a(E,p(E,p(x,p(y,y)))) = P2.
871
a(E,p(p(x,p(y,y)),E)) = P2.
872
a(E,a(A,p(E,p(P1,P2)))) = P2.
873
a(E,a(A,p(p(P1,P2),E))) = P2.
874
a(E,a(p(P2,E),f(P2,E))) = P2.
875
a(E,a(p(E,P2),f(P2,E))) = P2.
876
a(E,a(p(P2,E),f(E,P2))) = P2.
877
a(E,a(p(E,P2),f(E,P2))) = P2.
878
a(E,a(A,p(E,p(P2,P1)))) = P2.
879
a(E,a(A,p(p(P2,P1),E))) = P2.
880
a(E,a(p(A,P2),f(P2,A))) = P2.
881
a(E,a(p(P2,A),f(P2,A))) = P2.
882
a(E,a(p(A,P2),f(A,P2))) = P2.
883
a(E,a(p(P2,A),f(A,P2))) = P2.
884
a(E,a(p(A,P2),p(x,E))) = P2.
885
a(E,a(p(P2,A),p(x,E))) = P2.
886
a(E,p(p(K(x),y),P1)) = P2.
887
a(E,p(P1,p(K(x),y))) = P2.
888
a(E,p(p(x,K(y)),P1)) = P2.
889
a(E,p(P1,p(x,K(y)))) = P2.
890
a(E,p(A,p(K(x),y))) = P2.
891
a(E,p(p(K(x),y),A)) = P2.
892
a(E,p(p(A,x),p(P1,y))) = P2.
893
a(E,p(p(P1,x),p(A,y))) = P2.
894
a(E,p(A,p(x,K(y)))) = P2.
895
a(E,p(p(x,K(y)),A)) = P2.
896
a(E,p(p(x,A),p(y,P1))) = P2.
897
a(E,p(p(x,P1),p(y,A))) = P2.
898
a(E,p(A,p(x,p(y,P1)))) = P2.
899
a(E,p(A,p(x,p(y,E)))) = P2.
900
a(E,p(A,p(x,p(E,y)))) = P2.
901
a(E,p(A,p(x,p(P1,y)))) = P2.
902
a(E,p(A,p(x,p(P2,y)))) = P2.
903
a(E,p(A,p(x,p(y,P2)))) = P2.
904
a(E,p(p(x,p(y,P1)),A)) = P2.
905
a(E,p(p(x,p(y,E)),A)) = P2.
906
a(E,p(p(x,p(E,y)),A)) = P2.
907
a(E,p(p(x,p(P1,y)),A)) = P2.
908
a(E,p(p(x,p(P2,y)),A)) = P2.
909
a(E,p(p(x,p(y,P2)),A)) = P2.
910
a(E,a(A,p(K(A),A))) = P2.
911
a(E,a(A,p(K(E),A))) = P2.
912
a(E,a(A,p(p(x,A),A))) = P2.
913
a(E,a(A,p(p(A,x),A))) = P2.
914
a(E,a(A,p(E,A))) = P2.
915
a(E,a(A,p(A,K(A)))) = P2.
916
a(E,a(A,p(A,K(E)))) = P2.
917
a(E,a(A,p(p(x,P1),A))) = P2.
918
a(E,a(p(p(x,A),A),A)) = P2.
919
a(E,a(A,p(A,p(x,A)))) = P2.
920
a(E,a(A,p(A,p(A,x)))) = P2.
921
a(E,a(A,p(A,p(x,P1)))) = P2.
922
a(E,a(A,p(A,E))) = P2.
923
a(E,a(p(p(A,x),A),A)) = P2.
924
a(E,a(p(A,p(x,A)),A)) = P2.
925
a(E,a(p(A,p(A,x)),A)) = P2.
926
a(E,a(p(p(x,P2),A),A)) = P2.
927
a(E,a(p(A,p(x,P2)),A)) = P2.
928
a(E,p(p(p(P1,x),y),A)) = P2.
929
a(E,p(p(p(x,x),y),A)) = P2.
930
a(E,p(p(p(P2,x),y),A)) = P2.
931
a(E,p(p(p(x,P2),y),A)) = P2.
932
a(E,p(p(p(x,P1),y),A)) = P2.
933
a(E,p(A,p(p(P1,x),y))) = P2.
934
a(E,p(A,p(p(x,x),y))) = P2.
935
a(E,p(A,p(p(P2,x),y))) = P2.
936
a(E,p(A,p(p(x,P2),y))) = P2.
937
a(E,p(A,p(p(x,P1),y))) = P2.
938
a(E,p(P1,p(p(x,x),y))) = P2.
939
a(E,p(p(p(x,x),y),P1)) = P2.
940
a(E,p(P2,p(p(x,x),y))) = P2.
941
a(E,p(p(p(x,x),y),P2)) = P2.
942
a(E,p(E,p(p(x,x),y))) = P2.
943
a(E,p(p(p(x,x),y),E)) = P2.
945
a(E,K(K(a(A,A)))) = P2.
946
a(E,K(a(a(A,A),x))) = P2.
947
a(p(E,E),K(A)) = p(P2,P2).
948
a(E,K(a(a(A,K(A)),A))) = P2.
949
a(E,p(p(x,A),p(y,E))) = P2.
950
a(E,p(p(x,E),p(y,A))) = P2.
951
a(E,p(p(A,x),p(E,y))) = P2.
952
a(E,p(p(E,x),p(A,y))) = P2.
953
a(p(K(x),E),K(A)) = p(x,P2).
954
a(a(p(P1,E),K(A)),A) = A.
955
a(p(E,K(x)),K(A)) = p(P2,x).
956
a(E,a(p(E,P1),K(A))) = P2.
957
a(E,a(p(E,P2),K(A))) = P2.
958
a(E,a(p(P1,E),K(A))) = P2.
959
a(E,a(p(P2,E),K(A))) = P2.
960
a(a(A,a(A,E)),a(A,A)) = P2.
961
a(E,p(p(p(E,x),y),A)) = P2.
962
a(E,p(p(p(x,E),y),A)) = P2.
963
a(E,p(A,p(p(E,x),y))) = P2.
964
a(E,p(A,p(p(x,E),y))) = P2.
966
a(p(E,E),K(E)) = p(P2,P2).
967
a(p(K(x),E),K(E)) = p(x,P2).
968
a(a(p(P1,E),K(E)),E) = E.
969
a(p(E,K(x)),K(E)) = p(P2,x).
970
a(E,a(p(E,P1),K(E))) = P2.
971
a(E,a(p(E,P2),K(E))) = P2.
972
a(E,a(p(P1,E),K(E))) = P2.
973
a(E,a(p(P2,E),K(E))) = P2.
977
a(E,K(a(A,K(A)))) = P2.
978
a(p(E,E),K(P1)) = p(P2,P2).
979
a(E,a(p(P2,E),K(P1))) = P2.
980
a(E,a(p(E,P2),K(P1))) = P2.
981
a(E,a(p(P1,E),K(P1))) = P2.
982
a(E,a(p(E,P1),K(P1))) = P2.
983
a(p(E,A),K(P1)) = p(P2,P1).
984
a(p(A,E),K(P1)) = p(P1,P2).
985
a(p(K(x),E),K(P1)) = p(x,P2).
986
a(p(E,K(x)),K(P1)) = p(P2,x).
987
a(E,p(p(x,p(y,A)),E)) = P2.
988
a(E,p(E,p(x,p(y,A)))) = P2.
989
a(E,p(p(p(A,x),y),E)) = P2.
990
a(E,p(E,p(p(A,x),y))) = P2.
991
a(E,p(p(p(x,A),y),E)) = P2.
992
a(E,p(E,p(p(x,A),y))) = P2.
993
a(E,p(p(x,p(A,y)),E)) = P2.
994
a(E,p(E,p(x,p(A,y)))) = P2.
995
a(E,a(p(K(P2),P1),E)) = P2.
996
a(E,a(p(P1,K(P2)),E)) = P2.
997
a(E,a(p(K(P2),P2),E)) = P2.
998
a(E,a(p(P2,K(P2)),E)) = P2.
1000
a(p(E,E),K(K(P2))) = p(P2,P2).
1001
a(E,a(p(E,P1),K(K(P2)))) = P2.
1002
a(E,a(p(E,P2),K(K(P2)))) = P2.
1003
a(E,a(p(P1,E),K(K(P2)))) = P2.
1004
a(E,a(p(P2,E),K(K(P2)))) = P2.
1005
a(E,K(a(a(A,E),P1))) = P2.
1006
a(E,K(a(a(A,E),P2))) = P2.
1007
a(E,a(p(P2,K(A)),E)) = P2.
1008
a(E,a(p(P1,K(K(P2))),E)) = P2.
1009
a(E,a(p(P2,K(K(P2))),E)) = P2.
1010
a(E,a(p(K(K(P2)),P1),E)) = P2.
1011
a(E,a(p(K(K(P2)),P2),E)) = P2.
1012
a(E,a(p(K(A),P2),E)) = P2.
1013
a(E,a(p(K(E),P2),E)) = P2.
1014
a(E,a(p(p(P1,P2),P2),E)) = P2.
1015
a(E,a(p(P2,K(E)),E)) = P2.
1016
a(E,a(p(P2,p(P1,P2)),E)) = P2.
1017
a(E,a(a(p(A,P1),A),P1)) = P2.
1018
a(E,a(a(p(P1,A),A),P1)) = P2.
1019
a(E,a(p(P1,K(A)),E)) = P2.
1020
a(E,a(p(K(A),P1),E)) = P2.
1021
a(E,a(p(K(E),P1),E)) = P2.
1022
a(E,a(p(p(P1,P2),P1),E)) = P2.
1023
a(E,a(p(P1,K(E)),E)) = P2.
1024
a(E,a(p(P1,p(P1,P2)),E)) = P2.