~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to apps.src/demods

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
% from x4.out
 
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.
 
21
a(p(P1,P2),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.
 
50
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).
 
59
a(E,p(P2,P1)) = P2.
 
60
a(E,f(P1,P2)) = P2.
 
61
a(E,f(P2,P1)) = 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).
 
174
a(E,p(P2,E)) = P2.
 
175
a(E,p(P2,A)) = P2.
 
176
a(E,p(E,P2)) = P2.
 
177
a(E,p(A,P2)) = P2.
 
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).
 
188
a(E,p(E,K(x))) = P2.
 
189
a(E,p(A,K(x))) = 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.
 
203
a(E,p(K(x),E)) = P2.
 
204
a(E,p(K(x),A)) = 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.
 
228
a(E,p(A,P1)) = P2.
 
229
a(E,p(P1,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.
 
237
a(E,p(E,P1)) = P2.
 
238
a(E,p(P1,E)) = 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.
 
290
a(E,p(A,E)) = P2.
 
291
a(E,p(E,A)) = 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.
 
944
a(E,K(A)) = 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.
 
965
a(E,K(E)) = 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.
 
974
a(E,K(P1)) = P2.
 
975
a(E,K(P2)) = P2.
 
976
a(E,K(a(A,A))) = 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.
 
999
a(E,K(K(P2))) = 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.