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
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
|
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint rat.
From mathcomp Require Import ring.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Section Polynomials.
Variables (R : unitRingType) (x1 x2 x3 y1 y2 y3 : R).
Definition f1 :=
x1^3*x2 - x1*x2^3 - x1^3*x3 + x2^3*x3 + x1*x3^3 - x2*x3^3 - x2*y1^
2 + x3*y1^2 + x1*y2^2 - x3*y2^2 - x1*y3^2 + x2*y3^2.
Definition f2 := 2%:R*x1^6%:R*x2^3 -
6%:R*x1^4%:R*x2^5 + 6%:R*x1^2*x2^7 - 2%:R*x2^9 - 6%:R*x1^6%:R*x2^ 2%:R*x3 +
6%:R*x1^5*x2^3*x3 + 12%:R*x1^4%:R*x2^4%:R*x3 - 12%:R*x1^3*x2^5*x3 -
6%:R*x1^2*x2^6%:R*x3 + 6%:R*x1*x2^7%:R*x3 + 6%:R*x1^6%:R*x2*x3^2 -
18%:R*x1^5*x2^2*x3^2 + 6%:R*x1^4%:R*x2^3*x3^2 + 24%:R*x1^3*x2^4%:R*x3^2 -
18%:R*x1^2*x2^5*x3^2 - 6%:R*x1*x2^6%:R*x3^2 + 6%:R*x2^7%:R*x3^2 - 2%:R*x1^6%:R*x3^3
+ 18%:R*x1^5*x2*x3^3 - 30%:R*x1^4%:R*x2^2*x3^3 + 2%:R*x1^3*x2^3*x3^3 +
24%:R*x1^2*x2^4%:R*x3^3 - 12%:R*x1*x2^5*x3^3 - 6%:R*x1^5*x3^4 +
24%:R*x1^4%:R*x2*x3^4 - 30%:R*x1^3*x2^2*x3^4 + 6%:R*x1^2*x2^3*x3^4 +
12%:R*x1*x2^4%:R*x3^4 - 6%:R*x2^5*x3^4 - 6%:R*x1^4%:R*x3^5 + 18%:R*x1^3*x2*x3^5 -
18%:R*x1^2*x2^2*x3^5 + 6%:R*x1*x2^3*x3^5 - 2%:R*x1^3*x3^6 +
6%:R*x1^2*x2*x3^6 - 6%:R*x1*x2^2*x3^6 + 2%:R*x2^3*x3^6 -
3%:R*x1^3*x2^3*y1^2 + 3%:R*x1*x2^5*y1^2 + 9%:R*x1^3*x2^2*x3*y1^2 -
6%:R*x1^2*x2^3*x3*y1^2 - 6%:R*x1*x2^4%:R*x3*y1^2 + 3%:R*x2^5*x3*y1^2 -
9%:R*x1^3*x2*x3^2*y1^2 + 18%:R*x1^2*x2^2*x3^2*y1^2 -
3%:R*x1*x2^3*x3^2*y1^2 - 6%:R*x2^4%:R*x3^2*y1^2 + 3%:R*x1^3*x3^3*y1^2 -
18%:R*x1^2*x2*x3^3*y1^2 + 15%:R*x1*x2^2*x3^3*y1^2 + 6%:R*x1^2*x3^4%:R*y1^2
- 12%:R*x1*x2*x3^4%:R*y1^2 + 6%:R*x2^2*x3^4%:R*y1^2 + 3%:R*x1*x3^5*y1^2 -
3%:R*x2*x3^5*y1^2 + x2^3*y1^4 - 3%:R*x2^2*x3*y1^4 + 3%:R*x2*x3^2*y1^4 -
x3^3*y1^4 + 8%:R*x1^3*x2^3*y1*y2 - 2%:R*x1^2*x2^4%:R*y1*y2 -
8%:R*x1*x2^5*y1*y2 + 2%:R*x2^6%:R*y1*y2 - 18%:R*x1^3*x2^2*x3*y1*y2 +
14%:R*x1^2*x2^3*x3*y1*y2 + 8%:R*x1*x2^4%:R*x3*y1*y2 - 4%:R*x2^5*x3*y1*y2 +
12%:R*x1^3*x2*x3^2*y1*y2 - 30%:R*x1^2*x2^2*x3^2*y1*y2 +
12%:R*x1*x2^3*x3^2*y1*y2 + 6%:R*x2^4%:R*x3^2*y1*y2 - 2%:R*x1^3*x3^3*y1*y2 +
26%:R*x1^2*x2*x3^3*y1*y2 - 22%:R*x1*x2^2*x3^3*y1*y2 -
2%:R*x2^3*x3^3*y1*y2 - 8%:R*x1^2*x3^4%:R*y1*y2 + 16%:R*x1*x2*x3^4%:R*y1*y2 -
8%:R*x2^2*x3^4%:R*y1*y2 - 6%:R*x1*x3^5*y1*y2 + 6%:R*x2*x3^5*y1*y2 -
6%:R*x2^3*y1^3*y2 + 12%:R*x2^2*x3*y1^3*y2 - 6%:R*x2*x3^2*y1^3*y2 -
3%:R*x1^5*x2*y2^2 + 2%:R*x1^4%:R*x2^2*y2^2 + 3%:R*x1^3*x2^3*y2^2 -
4%:R*x1^2*x2^4%:R*y2^2 + 2%:R*x2^6%:R*y2^2 + 3%:R*x1^5*x3*y2^2 -
4%:R*x1^4%:R*x2*x3*y2^2 + 4%:R*x1^3*x2^2*x3*y2^2 + x1^2*x2^3*x3*y2^2 -
4%:R*x1*x2^4%:R*x3*y2^2 + 2%:R*x1^4%:R*x3^2*y2^2 - 5%:R*x1^3*x2*x3^2*y2^2 +
6%:R*x1^2*x2^2*x3^2*y2^2 + x1*x2^3*x3^2*y2^2 - 4%:R*x2^4%:R*x3^2*y2^2 -
2%:R*x1^3*x3^3*y2^2 - 5%:R*x1^2*x2*x3^3*y2^2 + 4%:R*x1*x2^2*x3^3*y2^2 +
3%:R*x2^3*x3^3*y2^2 + 2%:R*x1^2*x3^4%:R*y2^2 - 4%:R*x1*x2*x3^4%:R*y2^2 +
2%:R*x2^2*x3^4%:R*y2^2 + 3%:R*x1*x3^5*y2^2 - 3%:R*x2*x3^5*y2^2 +
3%:R*x1^2*x2*y1^2*y2^2 - x1*x2^2*y1^2*y2^2 + 10%:R*x2^3*y1^2*y2^2 -
3%:R*x1^2*x3*y1^2*y2^2 + 2%:R*x1*x2*x3*y1^2*y2^2 -
17%:R*x2^2*x3*y1^2*y2^2 - x1*x3^2*y1^2*y2^2 + x2*x3^2*y1^2*y2^2 +
6%:R*x3^3*y1^2*y2^2 - 2%:R*x1^3*y1*y2^3 - 4%:R*x1^2*x2*y1*y2^3 +
4%:R*x1*x2^2*y1*y2^3 - 8%:R*x2^3*y1*y2^3 + 4%:R*x1^2*x3*y1*y2^3 +
8%:R*x2^2*x3*y1*y2^3 + 2%:R*x1*x3^2*y1*y2^3 + 4%:R*x2*x3^2*y1*y2^3 -
8%:R*x3^3*y1*y2^3 + 2%:R*y1^3*y2^3 + 3%:R*x1^3*y2^4 - 2%:R*x1^2*x2*y2^4 +
2%:R*x2^3*y2^4 - x1^2*x3*y2^4 - 2%:R*x1*x2*x3*y2^4 - x1*x3^2*y2^4 -
2%:R*x2*x3^2*y2^4 + 3%:R*x3^3*y2^4 - 6%:R*y1^2*y2^4 + 6%:R*y1*y2^5 - 2%:R*y2^6
- 6%:R*x1^3*x2^3*y1*y3 + 6%:R*x1^2*x2^4%:R*y1*y3 + 6%:R*x1*x2^5*y1*y3 -
6%:R*x2^6%:R*y1*y3 + 12%:R*x1^3*x2^2*x3*y1*y3 - 18%:R*x1^2*x2^3*x3*y1*y3 +
6%:R*x2^5*x3*y1*y3 - 6%:R*x1^3*x2*x3^2*y1*y3 +
18%:R*x1^2*x2^2*x3^2*y1*y3 - 18%:R*x1*x2^3*x3^2*y1*y3 +
6%:R*x2^4%:R*x3^2*y1*y3 - 6%:R*x1^2*x2*x3^3*y1*y3 +
12%:R*x1*x2^2*x3^3*y1*y3 - 6%:R*x2^3*x3^3*y1*y3 + 4%:R*x2^3*y1^3*y3 -
6%:R*x2^2*x3*y1^3*y3 + 2%:R*x3^3*y1^3*y3 + 6%:R*x1^5*x2*y2*y3 -
8%:R*x1^4%:R*x2^2*y2*y3 - 2%:R*x1^3*x2^3*y2*y3 + 6%:R*x1^2*x2^4%:R*y2*y3 -
4%:R*x1*x2^5*y2*y3 + 2%:R*x2^6%:R*y2*y3 - 6%:R*x1^5*x3*y2*y3 +
16%:R*x1^4%:R*x2*x3*y2*y3 - 22%:R*x1^3*x2^2*x3*y2*y3 +
12%:R*x1^2*x2^3*x3*y2*y3 + 8%:R*x1*x2^4%:R*x3*y2*y3 - 8%:R*x2^5*x3*y2*y3 -
8%:R*x1^4%:R*x3^2*y2*y3 + 26%:R*x1^3*x2*x3^2*y2*y3 -
30%:R*x1^2*x2^2*x3^2*y2*y3 + 14%:R*x1*x2^3*x3^2*y2*y3 -
2%:R*x2^4%:R*x3^2*y2*y3 - 2%:R*x1^3*x3^3*y2*y3 + 12%:R*x1^2*x2*x3^3*y2*y3 -
18%:R*x1*x2^2*x3^3*y2*y3 + 8%:R*x2^3*x3^3*y2*y3 -
6%:R*x1^2*x2*y1^2*y2*y3 + 4%:R*x1*x2^2*y1^2*y2*y3 -
10%:R*x2^3*y1^2*y2*y3 + 6%:R*x1^2*x3*y1^2*y2*y3 -
8%:R*x1*x2*x3*y1^2*y2*y3 + 20%:R*x2^2*x3*y1^2*y2*y3 +
4%:R*x1*x3^2*y1^2*y2*y3 - 4%:R*x2*x3^2*y1^2*y2*y3 - 6%:R*x3^3*y1^2*y2*y3
+ 6%:R*x1^3*y1*y2^2*y3 + 8%:R*x1^2*x2*y1*y2^2*y3 -
18%:R*x1*x2^2*y1*y2^2*y3 + 16%:R*x2^3*y1*y2^2*y3 -
8%:R*x1^2*x3*y1*y2^2*y3 + 8%:R*x1*x2*x3*y1*y2^2*y3 -
18%:R*x2^2*x3*y1*y2^2*y3 - 8%:R*x1*x3^2*y1*y2^2*y3 +
8%:R*x2*x3^2*y1*y2^2*y3 + 6%:R*x3^3*y1*y2^2*y3 - 6%:R*y1^3*y2^2*y3 -
8%:R*x1^3*y2^3*y3 + 4%:R*x1^2*x2*y2^3*y3 + 8%:R*x1*x2^2*y2^3*y3 -
8%:R*x2^3*y2^3*y3 + 2%:R*x1^2*x3*y2^3*y3 + 4%:R*x2^2*x3*y2^3*y3 +
4%:R*x1*x3^2*y2^3*y3 - 4%:R*x2*x3^2*y2^3*y3 - 2%:R*x3^3*y2^3*y3 +
18%:R*y1^2*y2^3*y3 - 18%:R*y1*y2^4%:R*y3 + 6%:R*y2^5*y3 - 3%:R*x1^5*x2*y3^2 +
6%:R*x1^4%:R*x2^2*y3^2 - 6%:R*x1^2*x2^4%:R*y3^2 + 3%:R*x1*x2^5*y3^2 +
3%:R*x1^5*x3*y3^2 - 12%:R*x1^4%:R*x2*x3*y3^2 + 15%:R*x1^3*x2^2*x3*y3^2 -
3%:R*x1^2*x2^3*x3*y3^2 - 6%:R*x1*x2^4%:R*x3*y3^2 + 3%:R*x2^5*x3*y3^2 +
6%:R*x1^4%:R*x3^2*y3^2 - 18%:R*x1^3*x2*x3^2*y3^2 +
18%:R*x1^2*x2^2*x3^2*y3^2 - 6%:R*x1*x2^3*x3^2*y3^2 + 3%:R*x1^3*x3^3*y3^2
- 9%:R*x1^2*x2*x3^3*y3^2 + 9%:R*x1*x2^2*x3^3*y3^2 - 3%:R*x2^3*x3^3*y3^2
+ 3%:R*x1^2*x2*y1^2*y3^2 - 3%:R*x1*x2^2*y1^2*y3^2 -
3%:R*x1^2*x3*y1^2*y3^2 + 6%:R*x1*x2*x3*y1^2*y3^2 -
3%:R*x2^2*x3*y1^2*y3^2 - 3%:R*x1*x3^2*y1^2*y3^2 + 3%:R*x2*x3^2*y1^2*y3^2
- 6%:R*x1^3*y1*y2*y3^2 - 4%:R*x1^2*x2*y1*y2*y3^2 +
20%:R*x1*x2^2*y1*y2*y3^2 - 10%:R*x2^3*y1*y2*y3^2 +
4%:R*x1^2*x3*y1*y2*y3^2 - 8%:R*x1*x2*x3*y1*y2*y3^2 +
4%:R*x2^2*x3*y1*y2*y3^2 + 6%:R*x1*x3^2*y1*y2*y3^2 -
6%:R*x2*x3^2*y1*y2*y3^2 + 6%:R*y1^3*y2*y3^2 + 6%:R*x1^3*y2^2*y3^2 +
x1^2*x2*y2^2*y3^2 - 17%:R*x1*x2^2*y2^2*y3^2 + 10%:R*x2^3*y2^2*y3^2 -
x1^2*x3*y2^2*y3^2 + 2%:R*x1*x2*x3*y2^2*y3^2 - x2^2*x3*y2^2*y3^2 -
3%:R*x1*x3^2*y2^2*y3^2 + 3%:R*x2*x3^2*y2^2*y3^2 - 18%:R*y1^2*y2^2*y3^2 +
18%:R*y1*y2^3*y3^2 - 6%:R*y2^4%:R*y3^2 + 2%:R*x1^3*y1*y3^3 -
6%:R*x1*x2^2*y1*y3^3 + 4%:R*x2^3*y1*y3^3 - 2%:R*y1^3*y3^3 -
6%:R*x1^2*x2*y2*y3^3 + 12%:R*x1*x2^2*y2*y3^3 - 6%:R*x2^3*y2*y3^3 +
6%:R*y1^2*y2*y3^3 - 6%:R*y1*y2^2*y3^3 + 2%:R*y2^3*y3^3 - x1^3*y3^4 +
3%:R*x1^2*x2*y3^4 - 3%:R*x1*x2^2*y3^4 + x2^3*y3^4.
Definition f3 := 2%:R*x1^9%:R*x2^4 -
8%:R*x1^7%:R*x2^6 + 12%:R*x1^5*x2^8 - 8%:R*x1^3*x2^10 + 2%:R*x1*x2^12 -
8%:R*x1^9%:R*x2^3*x3 + 6%:R*x1^ 8%:R*x2^4%:R*x3 + 24%:R*x1^7%:R*x2^5*x3 -
16%:R*x1^6%:R*x2^6%:R*x3 - 24%:R*x1^5*x2^7%:R*x3 + 12%:R*x1^4%:R*x2^ 8%:R*x3 +
8%:R*x1^3*x2^9%:R*x3 - 2%:R*x2^12%:R*x3 + 12%:R*x1^9%:R*x2^2*x3^2 -
24%:R*x1^ 8%:R*x2^3*x3^2 - 12%:R*x1^7%:R*x2^4%:R*x3^2 + 48%:R*x1^6%:R*x2^5*x3^2 -
12%:R*x1^5*x2^6%:R*x3^2 - 24%:R*x1^4%:R*x2^7%:R*x3^2 + 12%:R*x1^3*x2^ 8%:R*x3^2 -
8%:R*x1^9%:R*x2*x3^3 + 36%:R*x1^ 8%:R*x2^2*x3^3 - 32%:R*x1^7%:R*x2^3*x3^3 -
36%:R*x1^6%:R*x2^4%:R*x3^3 + 48%:R*x1^5*x2^5*x3^3 + 4%:R*x1^4%:R*x2^6%:R*x3^3 -
12%:R*x1^2*x2^ 8%:R*x3^3 - 8%:R*x1*x2^9%:R*x3^3 + 8%:R*x2^10%:R*x3^3 + 2%:R*x1^9%:R*x3^4 -
24%:R*x1^ 8%:R*x2*x3^4 + 48%:R*x1^7%:R*x2^2*x3^4 - 16%:R*x1^6%:R*x2^3*x3^4 -
18%:R*x1^5*x2^4%:R*x3^4 - 4%:R*x1^3*x2^6%:R*x3^4 + 24%:R*x1^2*x2^7%:R*x3^4 -
12%:R*x1*x2^ 8%:R*x3^4 + 6%:R*x1^ 8%:R*x3^5 - 24%:R*x1^7%:R*x2*x3^5 +
24%:R*x1^6%:R*x2^2*x3^5 + 18%:R*x1^4%:R*x2^4%:R*x3^5 - 48%:R*x1^3*x2^5*x3^5 +
12%:R*x1^2*x2^6%:R*x3^5 + 24%:R*x1*x2^7%:R*x3^5 - 12%:R*x2^ 8%:R*x3^5 + 4%:R*x1^7%:R*x3^6
- 24%:R*x1^5*x2^2*x3^6 + 16%:R*x1^4%:R*x2^3*x3^6 + 36%:R*x1^3*x2^4%:R*x3^6 -
48%:R*x1^2*x2^5*x3^6 + 16%:R*x1*x2^6%:R*x3^6 - 4%:R*x1^6%:R*x3^7 +
24%:R*x1^5*x2*x3^7 - 48%:R*x1^4%:R*x2^2*x3^7 + 32%:R*x1^3*x2^3*x3^7 +
12%:R*x1^2*x2^4%:R*x3^7 - 24%:R*x1*x2^5*x3^7 + 8%:R*x2^6%:R*x3^7 - 6%:R*x1^5*x3^8 +
24%:R*x1^4%:R*x2*x3^8 - 36%:R*x1^3*x2^2*x3^8 + 24%:R*x1^2*x2^3*x3^8 -
6%:R*x1*x2^4%:R*x3^8 - 2%:R*x1^4%:R*x3^9 + 8%:R*x1^3*x2*x3^9 - 12%:R*x1^2*x2^2*x3^9
+ 8%:R*x1*x2^3*x3^9 - 2%:R*x2^4%:R*x3^9 - 5%:R*x1^6%:R*x2^4%:R*y1^2 +
12%:R*x1^4%:R*x2^6%:R*y1^2 - 9%:R*x1^2*x2^ 8%:R*y1^2 + 2%:R*x2^10%:R*y1^2 +
20%:R*x1^6%:R*x2^3*x3*y1^2 - 12%:R*x1^5*x2^4%:R*x3*y1^2 -
36%:R*x1^4%:R*x2^5*x3*y1^2 + 18%:R*x1^3*x2^6%:R*x3*y1^2 +
18%:R*x1^2*x2^7%:R*x3*y1^2 - 6%:R*x1*x2^ 8%:R*x3*y1^2 - 2%:R*x2^9%:R*x3*y1^2 -
30%:R*x1^6%:R*x2^2*x3^2*y1^2 + 48%:R*x1^5*x2^3*x3^2*y1^2 +
18%:R*x1^4%:R*x2^4%:R*x3^2*y1^2 - 54%:R*x1^3*x2^5*x3^2*y1^2 +
9%:R*x1^2*x2^6%:R*x3^2*y1^2 + 12%:R*x1*x2^7%:R*x3^2*y1^2 - 3%:R*x2^ 8%:R*x3^2*y1^2 +
20%:R*x1^6%:R*x2*x3^3*y1^2 - 72%:R*x1^5*x2^2*x3^3*y1^2 +
48%:R*x1^4%:R*x2^3*x3^3*y1^2 + 40%:R*x1^3*x2^4%:R*x3^3*y1^2 -
36%:R*x1^2*x2^5*x3^3*y1^2 - 5%:R*x1^6%:R*x3^4%:R*y1^2 + 48%:R*x1^5*x2*x3^4%:R*y1^2
- 72%:R*x1^4%:R*x2^2*x3^4%:R*y1^2 + 20%:R*x1^3*x2^3*x3^4%:R*y1^2 +
12%:R*x1^2*x2^4%:R*x3^4%:R*y1^2 - 6%:R*x1*x2^5*x3^4%:R*y1^2 + 3%:R*x2^6%:R*x3^4%:R*y1^2 -
12%:R*x1^5*x3^5*y1^2 + 36%:R*x1^4%:R*x2*x3^5*y1^2 - 30%:R*x1^3*x2^2*x3^5*y1^2
+ 6%:R*x1^2*x2^3*x3^5*y1^2 - 6%:R*x1*x2^4%:R*x3^5*y1^2 + 6%:R*x2^5*x3^5*y1^2
- 6%:R*x1^4%:R*x3^6%:R*y1^2 + 2%:R*x1^3*x2*x3^6%:R*y1^2 + 9%:R*x1^2*x2^2*x3^6%:R*y1^2
- 5%:R*x2^4%:R*x3^6%:R*y1^2 + 4%:R*x1^3*x3^7%:R*y1^2 - 12%:R*x1^2*x2*x3^7%:R*y1^2 +
12%:R*x1*x2^2*x3^7%:R*y1^2 - 4%:R*x2^3*x3^7%:R*y1^2 + 3%:R*x1^2*x3^ 8%:R*y1^2 -
6%:R*x1*x2*x3^ 8%:R*y1^2 + 3%:R*x2^2*x3^ 8%:R*y1^2 + 4%:R*x1^3*x2^4%:R*y1^4 -
4%:R*x1*x2^6%:R*y1^4 - 16%:R*x1^3*x2^3*x3*y1^4 + 6%:R*x1^2*x2^4%:R*x3*y1^4 +
12%:R*x1*x2^5*x3*y1^4 - 2%:R*x2^6%:R*x3*y1^4 + 24%:R*x1^3*x2^2*x3^2*y1^4 -
24%:R*x1^2*x2^3*x3^2*y1^4 - 6%:R*x1*x2^4%:R*x3^2*y1^4 + 6%:R*x2^5*x3^2*y1^4 -
16%:R*x1^3*x2*x3^3*y1^4 + 36%:R*x1^2*x2^2*x3^3*y1^4 -
16%:R*x1*x2^3*x3^3*y1^4 - 4%:R*x2^4%:R*x3^3*y1^4 + 4%:R*x1^3*x3^4%:R*y1^4 -
24%:R*x1^2*x2*x3^4%:R*y1^4 + 24%:R*x1*x2^2*x3^4%:R*y1^4 - 4%:R*x2^3*x3^4%:R*y1^4 +
6%:R*x1^2*x3^5*y1^4 - 12%:R*x1*x2*x3^5*y1^4 + 6%:R*x2^2*x3^5*y1^4 +
2%:R*x1*x3^6%:R*y1^4 - 2%:R*x2*x3^6%:R*y1^4 - x2^4%:R*y1^6 + 4%:R*x2^3*x3*y1^6 -
6%:R*x2^2*x3^2*y1^6 + 4%:R*x2*x3^3*y1^6 - x3^4%:R*y1^6 + 8%:R*x1^6%:R*x2^4%:R*y1*y2
- 2%:R*x1^5*x2^5*y1*y2 - 16%:R*x1^4%:R*x2^6%:R*y1*y2 + 4%:R*x1^3*x2^7%:R*y1*y2 +
8%:R*x1^2*x2^ 8%:R*y1*y2 - 2%:R*x1*x2^9%:R*y1*y2 - 26%:R*x1^6%:R*x2^3*x3*y1*y2 +
16%:R*x1^5*x2^4%:R*x3*y1*y2 + 34%:R*x1^4%:R*x2^5*x3*y1*y2 -
12%:R*x1^3*x2^6%:R*x3*y1*y2 - 10%:R*x1^2*x2^7%:R*x3*y1*y2 -
4%:R*x1*x2^ 8%:R*x3*y1*y2 + 2%:R*x2^9%:R*x3*y1*y2 + 30%:R*x1^6%:R*x2^2*x3^2*y1*y2 -
44%:R*x1^5*x2^3*x3^2*y1*y2 - 8%:R*x1^4%:R*x2^4%:R*x3^2*y1*y2 +
22%:R*x1^3*x2^5*x3^2*y1*y2 + 2%:R*x1^2*x2^6%:R*x3^2*y1*y2 +
2%:R*x1*x2^7%:R*x3^2*y1*y2 - 4%:R*x2^ 8%:R*x3^2*y1*y2 - 14%:R*x1^6%:R*x2*x3^3*y1*y2
+ 56%:R*x1^5*x2^2*x3^3*y1*y2 - 24%:R*x1^4%:R*x2^3*x3^3*y1*y2 -
32%:R*x1^3*x2^4%:R*x3^3*y1*y2 - 14%:R*x1^2*x2^5*x3^3*y1*y2 +
24%:R*x1*x2^6%:R*x3^3*y1*y2 + 4%:R*x2^7%:R*x3^3*y1*y2 + 2%:R*x1^6%:R*x3^4%:R*y1*y2 -
34%:R*x1^5*x2*x3^4%:R*y1*y2 + 20%:R*x1^4%:R*x2^2*x3^4%:R*y1*y2 +
32%:R*x1^3*x2^3*x3^4%:R*y1*y2 + 4%:R*x1^2*x2^4%:R*x3^4%:R*y1*y2 -
26%:R*x1*x2^5*x3^4%:R*y1*y2 + 2%:R*x2^6%:R*x3^4%:R*y1*y2 + 8%:R*x1^5*x3^5*y1*y2 -
10%:R*x1^4%:R*x2*x3^5*y1*y2 - 28%:R*x1^3*x2^2*x3^5*y1*y2 +
40%:R*x1^2*x2^3*x3^5*y1*y2 + 4%:R*x1*x2^4%:R*x3^5*y1*y2 -
14%:R*x2^5*x3^5*y1*y2 + 4%:R*x1^4%:R*x3^6%:R*y1*y2 + 22%:R*x1^3*x2*x3^6%:R*y1*y2 -
48%:R*x1^2*x2^2*x3^6%:R*y1*y2 + 14%:R*x1*x2^3*x3^6%:R*y1*y2 +
8%:R*x2^4%:R*x3^6%:R*y1*y2 - 8%:R*x1^3*x3^7%:R*y1*y2 + 24%:R*x1^2*x2*x3^7%:R*y1*y2 -
24%:R*x1*x2^2*x3^7%:R*y1*y2 + 8%:R*x2^3*x3^7%:R*y1*y2 - 6%:R*x1^2*x3^ 8%:R*y1*y2 +
12%:R*x1*x2*x3^ 8%:R*y1*y2 - 6%:R*x2^2*x3^ 8%:R*y1*y2 - 14%:R*x1^3*x2^4%:R*y1^3*y2 +
2%:R*x1^2*x2^5*y1^3*y2 + 14%:R*x1*x2^6%:R*y1^3*y2 - 2%:R*x2^7%:R*y1^3*y2 +
44%:R*x1^3*x2^3*x3*y1^3*y2 - 16%:R*x1^2*x2^4%:R*x3*y1^3*y2 -
28%:R*x1*x2^5*x3*y1^3*y2 - 48%:R*x1^3*x2^2*x3^2*y1^3*y2 +
44%:R*x1^2*x2^3*x3^2*y1^3*y2 + 2%:R*x1*x2^4%:R*x3^2*y1^3*y2 +
2%:R*x2^5*x3^2*y1^3*y2 + 20%:R*x1^3*x2*x3^3*y1^3*y2 -
56%:R*x1^2*x2^2*x3^3*y1^3*y2 + 28%:R*x1*x2^3*x3^3*y1^3*y2 +
8%:R*x2^4%:R*x3^3*y1^3*y2 - 2%:R*x1^3*x3^4%:R*y1^3*y2 +
34%:R*x1^2*x2*x3^4%:R*y1^3*y2 - 26%:R*x1*x2^2*x3^4%:R*y1^3*y2 -
6%:R*x2^3*x3^4%:R*y1^3*y2 - 8%:R*x1^2*x3^5*y1^3*y2 + 16%:R*x1*x2*x3^5*y1^3*y2
- 8%:R*x2^2*x3^5*y1^3*y2 - 6%:R*x1*x3^6%:R*y1^3*y2 + 6%:R*x2*x3^6%:R*y1^3*y2 +
6%:R*x2^4%:R*y1^5*y2 - 18%:R*x2^3*x3*y1^5*y2 + 18%:R*x2^2*x3^2*y1^5*y2 -
6%:R*x2*x3^3*y1^5*y2 - 3%:R*x1^ 8%:R*x2^2*y2^2 + 4%:R*x1^7%:R*x2^3*y2^2 +
6%:R*x1^6%:R*x2^4%:R*y2^2 - 12%:R*x1^5*x2^5*y2^2 - 3%:R*x1^4%:R*x2^6%:R*y2^2 +
12%:R*x1^3*x2^7%:R*y2^2 - 4%:R*x1*x2^9%:R*y2^2 + 6%:R*x1^ 8%:R*x2*x3*y2^2 -
12%:R*x1^7%:R*x2^2*x3*y2^2 + 2%:R*x1^6%:R*x2^3*x3*y2^2 + 18%:R*x1^5*x2^4%:R*x3*y2^2
- 12%:R*x1^4%:R*x2^5*x3*y2^2 - 6%:R*x1^3*x2^6%:R*x3*y2^2 + 4%:R*x2^9%:R*x3*y2^2 -
3%:R*x1^ 8%:R*x3^2*y2^2 + 12%:R*x1^7%:R*x2*x3^2*y2^2 - 21%:R*x1^6%:R*x2^2*x3^2*y2^2
+ 6%:R*x1^5*x2^3*x3^2*y2^2 + 18%:R*x1^4%:R*x2^4%:R*x3^2*y2^2 -
12%:R*x1^3*x2^5*x3^2*y2^2 - 4%:R*x1^7%:R*x3^3*y2^2 + 12%:R*x1^6%:R*x2*x3^3*y2^2
- 18%:R*x1^5*x2^2*x3^3*y2^2 + 4%:R*x1^4%:R*x2^3*x3^3*y2^2 +
12%:R*x1^2*x2^5*x3^3*y2^2 + 6%:R*x1*x2^6%:R*x3^3*y2^2 - 12%:R*x2^7%:R*x3^3*y2^2
+ x1^6%:R*x3^4%:R*y2^2 + 6%:R*x1^5*x2*x3^4%:R*y2^2 - 4%:R*x1^3*x2^3*x3^4%:R*y2^2 -
18%:R*x1^2*x2^4%:R*x3^4%:R*y2^2 + 12%:R*x1*x2^5*x3^4%:R*y2^2 + 3%:R*x2^6%:R*x3^4%:R*y2^2
- 6%:R*x1^4%:R*x2*x3^5*y2^2 + 18%:R*x1^3*x2^2*x3^5*y2^2 -
6%:R*x1^2*x2^3*x3^5*y2^2 - 18%:R*x1*x2^4%:R*x3^5*y2^2 + 12%:R*x2^5*x3^5*y2^2
- x1^4%:R*x3^6%:R*y2^2 - 12%:R*x1^3*x2*x3^6%:R*y2^2 + 21%:R*x1^2*x2^2*x3^6%:R*y2^2
- 2%:R*x1*x2^3*x3^6%:R*y2^2 - 6%:R*x2^4%:R*x3^6%:R*y2^2 + 4%:R*x1^3*x3^7%:R*y2^2 -
12%:R*x1^2*x2*x3^7%:R*y2^2 + 12%:R*x1*x2^2*x3^7%:R*y2^2 - 4%:R*x2^3*x3^7%:R*y2^2 +
3%:R*x1^2*x3^ 8%:R*y2^2 - 6%:R*x1*x2*x3^ 8%:R*y2^2 + 3%:R*x2^2*x3^ 8%:R*y2^2 +
6%:R*x1^5*x2^2*y1^2*y2^2 - 6%:R*x1^4%:R*x2^3*y1^2*y2^2 +
4%:R*x1^3*x2^4%:R*y1^2*y2^2 + 8%:R*x1^2*x2^5*y1^2*y2^2 -
10%:R*x1*x2^6%:R*y1^2*y2^2 - 2%:R*x2^7%:R*y1^2*y2^2 - 12%:R*x1^5*x2*x3*y1^2*y2^2
+ 18%:R*x1^4%:R*x2^2*x3*y1^2*y2^2 - 28%:R*x1^3*x2^3*x3*y1^2*y2^2 -
10%:R*x1^2*x2^4%:R*x3*y1^2*y2^2 + 20%:R*x1*x2^5*x3*y1^2*y2^2 +
12%:R*x2^6%:R*x3*y1^2*y2^2 + 6%:R*x1^5*x3^2*y1^2*y2^2 -
18%:R*x1^4%:R*x2*x3^2*y1^2*y2^2 + 36%:R*x1^3*x2^2*x3^2*y1^2*y2^2 -
4%:R*x1^2*x2^3*x3^2*y1^2*y2^2 - 4%:R*x1*x2^4%:R*x3^2*y1^2*y2^2 -
16%:R*x2^5*x3^2*y1^2*y2^2 + 6%:R*x1^4%:R*x3^3*y1^2*y2^2 -
4%:R*x1^3*x2*x3^3*y1^2*y2^2 + 4%:R*x1^2*x2^2*x3^3*y1^2*y2^2 +
4%:R*x1*x2^3*x3^3*y1^2*y2^2 - 10%:R*x2^4%:R*x3^3*y1^2*y2^2 -
8%:R*x1^3*x3^4%:R*y1^2*y2^2 + 4%:R*x1^2*x2*x3^4%:R*y1^2*y2^2 -
20%:R*x1*x2^2*x3^4%:R*y1^2*y2^2 + 24%:R*x2^3*x3^4%:R*y1^2*y2^2 -
2%:R*x1^2*x3^5*y1^2*y2^2 + 4%:R*x1*x2*x3^5*y1^2*y2^2 -
2%:R*x2^2*x3^5*y1^2*y2^2 + 6%:R*x1*x3^6%:R*y1^2*y2^2 - 6%:R*x2*x3^6%:R*y1^2*y2^2
- 3%:R*x1^2*x2^2*y1^4%:R*y2^2 + 2%:R*x1*x2^3*y1^4%:R*y2^2 - 10%:R*x2^4%:R*y1^4%:R*y2^2
+ 6%:R*x1^2*x2*x3*y1^4%:R*y2^2 - 6%:R*x1*x2^2*x3*y1^4%:R*y2^2 +
26%:R*x2^3*x3*y1^4%:R*y2^2 - 3%:R*x1^2*x3^2*y1^4%:R*y2^2 +
6%:R*x1*x2*x3^2*y1^4%:R*y2^2 - 15%:R*x2^2*x3^2*y1^4%:R*y2^2 -
2%:R*x1*x3^3*y1^4%:R*y2^2 - 8%:R*x2*x3^3*y1^4%:R*y2^2 + 7%:R*x3^4%:R*y1^4%:R*y2^2 -
2%:R*x1^6%:R*x2*y1*y2^3 - 4%:R*x1^5*x2^2*y1*y2^3 + 14%:R*x1^4%:R*x2^3*y1*y2^3 -
6%:R*x1^3*x2^4%:R*y1*y2^3 - 12%:R*x1^2*x2^5*y1*y2^3 + 10%:R*x1*x2^6%:R*y1*y2^3 +
2%:R*x1^6%:R*x3*y1*y2^3 + 8%:R*x1^5*x2*x3*y1*y2^3 -
22%:R*x1^4%:R*x2^2*x3*y1*y2^3 + 16%:R*x1^3*x2^3*x3*y1*y2^3 +
6%:R*x1^2*x2^4%:R*x3*y1*y2^3 - 10%:R*x2^6%:R*x3*y1*y2^3 - 4%:R*x1^5*x3^2*y1*y2^3
+ 14%:R*x1^4%:R*x2*x3^2*y1*y2^3 - 16%:R*x1^3*x2^2*x3^2*y1*y2^3 -
6%:R*x1*x2^4%:R*x3^2*y1*y2^3 + 12%:R*x2^5*x3^2*y1*y2^3 -
6%:R*x1^4%:R*x3^3*y1*y2^3 + 16%:R*x1^2*x2^2*x3^3*y1*y2^3 -
16%:R*x1*x2^3*x3^3*y1*y2^3 + 6%:R*x2^4%:R*x3^3*y1*y2^3 +
6%:R*x1^3*x3^4%:R*y1*y2^3 - 14%:R*x1^2*x2*x3^4%:R*y1*y2^3 +
22%:R*x1*x2^2*x3^4%:R*y1*y2^3 - 14%:R*x2^3*x3^4%:R*y1*y2^3 +
4%:R*x1^2*x3^5*y1*y2^3 - 8%:R*x1*x2*x3^5*y1*y2^3 + 4%:R*x2^2*x3^5*y1*y2^3
- 2%:R*x1*x3^6%:R*y1*y2^3 + 2%:R*x2*x3^6%:R*y1*y2^3 + 4%:R*x1^3*x2*y1^3*y2^3 +
4%:R*x1^2*x2^2*y1^3*y2^3 - 12%:R*x1*x2^3*y1^3*y2^3 + 8%:R*x2^4%:R*y1^3*y2^3 -
4%:R*x1^3*x3*y1^3*y2^3 - 8%:R*x1^2*x2*x3*y1^3*y2^3 +
16%:R*x1*x2^2*x3*y1^3*y2^3 - 8%:R*x2^3*x3*y1^3*y2^3 +
4%:R*x1^2*x3^2*y1^3*y2^3 - 8%:R*x1*x2*x3^2*y1^3*y2^3 -
8%:R*x2^2*x3^2*y1^3*y2^3 + 4%:R*x1*x3^3*y1^3*y2^3 +
16%:R*x2*x3^3*y1^3*y2^3 - 8%:R*x3^4%:R*y1^3*y2^3 - 2%:R*x2*y1^5*y2^3 +
2%:R*x3*y1^5*y2^3 - 6%:R*x1^3*x2*y1^2*y2^4 + x1^2*x2^2*y1^2*y2^4 +
16%:R*x1*x2^3*y1^2*y2^4 - 2%:R*x2^4%:R*y1^2*y2^4 + 6%:R*x1^3*x3*y1^2*y2^4 -
2%:R*x1^2*x2*x3*y1^2*y2^4 - 14%:R*x1*x2^2*x3*y1^2*y2^4 -
14%:R*x2^3*x3*y1^2*y2^4 + x1^2*x3^2*y1^2*y2^4 -
2%:R*x1*x2*x3^2*y1^2*y2^4 + 19%:R*x2^2*x3^2*y1^2*y2^4 -
3%:R*x3^4%:R*y1^2*y2^4 + 6%:R*x2*y1^4%:R*y2^4 - 6%:R*x3*y1^4%:R*y2^4 -
2%:R*x1^4%:R*y1*y2^5 + 2%:R*x1^3*x2*y1*y2^5 + 4%:R*x1^2*x2^2*y1*y2^5 -
14%:R*x1*x2^3*y1*y2^5 + 4%:R*x1^2*x2*x3*y1*y2^5 + 4%:R*x1*x2^2*x3*y1*y2^5
+ 14%:R*x2^3*x3*y1*y2^5 - 2%:R*x1^2*x3^2*y1*y2^5 + 4%:R*x1*x2*x3^2*y1*y2^5
- 8%:R*x2^2*x3^2*y1*y2^5 - 4%:R*x1*x3^3*y1*y2^5 - 10%:R*x2*x3^3*y1*y2^5 +
8%:R*x3^4%:R*y1*y2^5 + 2%:R*x1*y1^3*y2^5 - 6%:R*x2*y1^3*y2^5 + 4%:R*x3*y1^3*y2^5
+ 3%:R*x1^4%:R*y2^6 - 4%:R*x1^3*x2*y2^6 + 4%:R*x1*x2^3*y2^6 - 2%:R*x1^3*x3*y2^6
- 4%:R*x2^3*x3*y2^6 + 2%:R*x1*x3^3*y2^6 + 4%:R*x2*x3^3*y2^6 - 3%:R*x3^4%:R*y2^6
- 6%:R*x1*y1^2*y2^6 + 2%:R*x2*y1^2*y2^6 + 4%:R*x3*y1^2*y2^6 + 6%:R*x1*y1*y2^7
- 6%:R*x3*y1*y2^7 - 2%:R*x1*y2^8 + 2%:R*x3*y2^8 - 6%:R*x1^6%:R*x2^4%:R*y1*y3 +
6%:R*x1^5*x2^5*y1*y3 + 12%:R*x1^4%:R*x2^6%:R*y1*y3 - 12%:R*x1^3*x2^7%:R*y1*y3 -
6%:R*x1^2*x2^ 8%:R*y1*y3 + 6%:R*x1*x2^9%:R*y1*y3 + 18%:R*x1^6%:R*x2^3*x3*y1*y3 -
24%:R*x1^5*x2^4%:R*x3*y1*y3 - 18%:R*x1^4%:R*x2^5*x3*y1*y3 +
24%:R*x1^3*x2^6%:R*x3*y1*y3 + 6%:R*x1^2*x2^7%:R*x3*y1*y3 - 6%:R*x2^9%:R*x3*y1*y3 -
18%:R*x1^6%:R*x2^2*x3^2*y1*y3 + 36%:R*x1^5*x2^3*x3^2*y1*y3 -
12%:R*x1^4%:R*x2^4%:R*x3^2*y1*y3 - 6%:R*x1^3*x2^5*x3^2*y1*y3 -
6%:R*x1*x2^7%:R*x3^2*y1*y3 + 6%:R*x2^ 8%:R*x3^2*y1*y3 + 6%:R*x1^6%:R*x2*x3^3*y1*y3 -
24%:R*x1^5*x2^2*x3^3*y1*y3 + 24%:R*x1^4%:R*x2^3*x3^3*y1*y3 +
6%:R*x1^2*x2^5*x3^3*y1*y3 - 24%:R*x1*x2^6%:R*x3^3*y1*y3 +
12%:R*x2^7%:R*x3^3*y1*y3 + 6%:R*x1^5*x2*x3^4%:R*y1*y3 -
24%:R*x1^3*x2^3*x3^4%:R*y1*y3 + 12%:R*x1^2*x2^4%:R*x3^4%:R*y1*y3 +
18%:R*x1*x2^5*x3^4%:R*y1*y3 - 12%:R*x2^6%:R*x3^4%:R*y1*y3 - 6%:R*x1^4%:R*x2*x3^5*y1*y3
+ 24%:R*x1^3*x2^2*x3^5*y1*y3 - 36%:R*x1^2*x2^3*x3^5*y1*y3 +
24%:R*x1*x2^4%:R*x3^5*y1*y3 - 6%:R*x2^5*x3^5*y1*y3 - 6%:R*x1^3*x2*x3^6%:R*y1*y3
+ 18%:R*x1^2*x2^2*x3^6%:R*y1*y3 - 18%:R*x1*x2^3*x3^6%:R*y1*y3 +
6%:R*x2^4%:R*x3^6%:R*y1*y3 + 10%:R*x1^3*x2^4%:R*y1^3*y3 - 6%:R*x1^2*x2^5*y1^3*y3 -
10%:R*x1*x2^6%:R*y1^3*y3 + 6%:R*x2^7%:R*y1^3*y3 - 28%:R*x1^3*x2^3*x3*y1^3*y3 +
24%:R*x1^2*x2^4%:R*x3*y1^3*y3 + 12%:R*x1*x2^5*x3*y1^3*y3 -
8%:R*x2^6%:R*x3*y1^3*y3 + 24%:R*x1^3*x2^2*x3^2*y1^3*y3 -
36%:R*x1^2*x2^3*x3^2*y1^3*y3 + 18%:R*x1*x2^4%:R*x3^2*y1^3*y3 -
6%:R*x2^5*x3^2*y1^3*y3 - 4%:R*x1^3*x2*x3^3*y1^3*y3 +
24%:R*x1^2*x2^2*x3^3*y1^3*y3 - 28%:R*x1*x2^3*x3^3*y1^3*y3 +
8%:R*x2^4%:R*x3^3*y1^3*y3 - 2%:R*x1^3*x3^4%:R*y1^3*y3 -
6%:R*x1^2*x2*x3^4%:R*y1^3*y3 + 6%:R*x1*x2^2*x3^4%:R*y1^3*y3 +
2%:R*x2^3*x3^4%:R*y1^3*y3 + 2%:R*x1*x3^6%:R*y1^3*y3 - 2%:R*x2*x3^6%:R*y1^3*y3 -
4%:R*x2^4%:R*y1^5*y3 + 10%:R*x2^3*x3*y1^5*y3 - 6%:R*x2^2*x3^2*y1^5*y3 -
2%:R*x2*x3^3*y1^5*y3 + 2%:R*x3^4%:R*y1^5*y3 + 6%:R*x1^ 8%:R*x2^2*y2*y3 -
8%:R*x1^7%:R*x2^3*y2*y3 - 8%:R*x1^6%:R*x2^4%:R*y2*y3 + 14%:R*x1^5*x2^5*y2*y3 -
2%:R*x1^4%:R*x2^6%:R*y2*y3 - 4%:R*x1^3*x2^7%:R*y2*y3 + 4%:R*x1^2*x2^ 8%:R*y2*y3 -
2%:R*x1*x2^9%:R*y2*y3 - 12%:R*x1^ 8%:R*x2*x3*y2*y3 + 24%:R*x1^7%:R*x2^2*x3*y2*y3 -
14%:R*x1^6%:R*x2^3*x3*y2*y3 - 4%:R*x1^5*x2^4%:R*x3*y2*y3 +
26%:R*x1^4%:R*x2^5*x3*y2*y3 - 24%:R*x1^3*x2^6%:R*x3*y2*y3 -
2%:R*x1^2*x2^7%:R*x3*y2*y3 + 4%:R*x1*x2^ 8%:R*x3*y2*y3 + 2%:R*x2^9%:R*x3*y2*y3 +
6%:R*x1^ 8%:R*x3^2*y2*y3 - 24%:R*x1^7%:R*x2*x3^2*y2*y3 +
48%:R*x1^6%:R*x2^2*x3^2*y2*y3 - 40%:R*x1^5*x2^3*x3^2*y2*y3 -
4%:R*x1^4%:R*x2^4%:R*x3^2*y2*y3 + 14%:R*x1^3*x2^5*x3^2*y2*y3 -
2%:R*x1^2*x2^6%:R*x3^2*y2*y3 + 10%:R*x1*x2^7%:R*x3^2*y2*y3 -
8%:R*x2^ 8%:R*x3^2*y2*y3 + 8%:R*x1^7%:R*x3^3*y2*y3 - 22%:R*x1^6%:R*x2*x3^3*y2*y3 +
28%:R*x1^5*x2^2*x3^3*y2*y3 - 32%:R*x1^4%:R*x2^3*x3^3*y2*y3 +
32%:R*x1^3*x2^4%:R*x3^3*y2*y3 - 22%:R*x1^2*x2^5*x3^3*y2*y3 +
12%:R*x1*x2^6%:R*x3^3*y2*y3 - 4%:R*x2^7%:R*x3^3*y2*y3 - 4%:R*x1^6%:R*x3^4%:R*y2*y3 +
10%:R*x1^5*x2*x3^4%:R*y2*y3 - 20%:R*x1^4%:R*x2^2*x3^4%:R*y2*y3 +
24%:R*x1^3*x2^3*x3^4%:R*y2*y3 + 8%:R*x1^2*x2^4%:R*x3^4%:R*y2*y3 -
34%:R*x1*x2^5*x3^4%:R*y2*y3 + 16%:R*x2^6%:R*x3^4%:R*y2*y3 - 8%:R*x1^5*x3^5*y2*y3 +
34%:R*x1^4%:R*x2*x3^5*y2*y3 - 56%:R*x1^3*x2^2*x3^5*y2*y3 +
44%:R*x1^2*x2^3*x3^5*y2*y3 - 16%:R*x1*x2^4%:R*x3^5*y2*y3 +
2%:R*x2^5*x3^5*y2*y3 - 2%:R*x1^4%:R*x3^6%:R*y2*y3 + 14%:R*x1^3*x2*x3^6%:R*y2*y3 -
30%:R*x1^2*x2^2*x3^6%:R*y2*y3 + 26%:R*x1*x2^3*x3^6%:R*y2*y3 -
8%:R*x2^4%:R*x3^6%:R*y2*y3 - 12%:R*x1^5*x2^2*y1^2*y2*y3 +
12%:R*x1^4%:R*x2^3*y1^2*y2*y3 - 2%:R*x1^3*x2^4%:R*y1^2*y2*y3 -
10%:R*x1^2*x2^5*y1^2*y2*y3 + 14%:R*x1*x2^6%:R*y1^2*y2*y3 -
2%:R*x2^7%:R*y1^2*y2*y3 + 24%:R*x1^5*x2*x3*y1^2*y2*y3 -
36%:R*x1^4%:R*x2^2*x3*y1^2*y2*y3 + 44%:R*x1^3*x2^3*x3*y1^2*y2*y3 -
4%:R*x1^2*x2^4%:R*x3*y1^2*y2*y3 - 28%:R*x1*x2^5*x3*y1^2*y2*y3 -
12%:R*x1^5*x3^2*y1^2*y2*y3 + 36%:R*x1^4%:R*x2*x3^2*y1^2*y2*y3 -
72%:R*x1^3*x2^2*x3^2*y1^2*y2*y3 + 44%:R*x1^2*x2^3*x3^2*y1^2*y2*y3 -
10%:R*x1*x2^4%:R*x3^2*y1^2*y2*y3 + 14%:R*x2^5*x3^2*y1^2*y2*y3 -
12%:R*x1^4%:R*x3^3*y1^2*y2*y3 + 20%:R*x1^3*x2*x3^3*y1^2*y2*y3 -
32%:R*x1^2*x2^2*x3^3*y1^2*y2*y3 + 28%:R*x1*x2^3*x3^3*y1^2*y2*y3 -
4%:R*x2^4%:R*x3^3*y1^2*y2*y3 + 10%:R*x1^3*x3^4%:R*y1^2*y2*y3 -
2%:R*x1^2*x2*x3^4%:R*y1^2*y2*y3 + 10%:R*x1*x2^2*x3^4%:R*y1^2*y2*y3 -
18%:R*x2^3*x3^4%:R*y1^2*y2*y3 + 4%:R*x1^2*x3^5*y1^2*y2*y3 -
8%:R*x1*x2*x3^5*y1^2*y2*y3 + 4%:R*x2^2*x3^5*y1^2*y2*y3 -
6%:R*x1*x3^6%:R*y1^2*y2*y3 + 6%:R*x2*x3^6%:R*y1^2*y2*y3 +
6%:R*x1^2*x2^2*y1^4%:R*y2*y3 - 4%:R*x1*x2^3*y1^4%:R*y2*y3 +
10%:R*x2^4%:R*y1^4%:R*y2*y3 - 12%:R*x1^2*x2*x3*y1^4%:R*y2*y3 +
12%:R*x1*x2^2*x3*y1^4%:R*y2*y3 - 30%:R*x2^3*x3*y1^4%:R*y2*y3 +
6%:R*x1^2*x3^2*y1^4%:R*y2*y3 - 12%:R*x1*x2*x3^2*y1^4%:R*y2*y3 +
24%:R*x2^2*x3^2*y1^4%:R*y2*y3 + 4%:R*x1*x3^3*y1^4%:R*y2*y3 +
2%:R*x2*x3^3*y1^4%:R*y2*y3 - 6%:R*x3^4%:R*y1^4%:R*y2*y3 + 6%:R*x1^6%:R*x2*y1*y2^2*y3 +
8%:R*x1^5*x2^2*y1*y2^2*y3 - 30%:R*x1^4%:R*x2^3*y1*y2^2*y3 +
14%:R*x1^3*x2^4%:R*y1*y2^2*y3 + 24%:R*x1^2*x2^5*y1*y2^2*y3 -
22%:R*x1*x2^6%:R*y1*y2^2*y3 - 6%:R*x1^6%:R*x3*y1*y2^2*y3 -
16%:R*x1^5*x2*x3*y1*y2^2*y3 + 38%:R*x1^4%:R*x2^2*x3*y1*y2^2*y3 -
32%:R*x1^3*x2^3*x3*y1*y2^2*y3 - 6%:R*x1^2*x2^4%:R*x3*y1*y2^2*y3 +
22%:R*x2^6%:R*x3*y1*y2^2*y3 + 8%:R*x1^5*x3^2*y1*y2^2*y3 -
22%:R*x1^4%:R*x2*x3^2*y1*y2^2*y3 + 32%:R*x1^3*x2^2*x3^2*y1*y2^2*y3 +
6%:R*x1*x2^4%:R*x3^2*y1*y2^2*y3 - 24%:R*x2^5*x3^2*y1*y2^2*y3 +
14%:R*x1^4%:R*x3^3*y1*y2^2*y3 - 32%:R*x1^2*x2^2*x3^3*y1*y2^2*y3 +
32%:R*x1*x2^3*x3^3*y1*y2^2*y3 - 14%:R*x2^4%:R*x3^3*y1*y2^2*y3 -
14%:R*x1^3*x3^4%:R*y1*y2^2*y3 + 22%:R*x1^2*x2*x3^4%:R*y1*y2^2*y3 -
38%:R*x1*x2^2*x3^4%:R*y1*y2^2*y3 + 30%:R*x2^3*x3^4%:R*y1*y2^2*y3 -
8%:R*x1^2*x3^5*y1*y2^2*y3 + 16%:R*x1*x2*x3^5*y1*y2^2*y3 -
8%:R*x2^2*x3^5*y1*y2^2*y3 + 6%:R*x1*x3^6%:R*y1*y2^2*y3 -
6%:R*x2*x3^6%:R*y1*y2^2*y3 - 12%:R*x1^3*x2*y1^3*y2^2*y3 -
8%:R*x1^2*x2^2*y1^3*y2^2*y3 + 28%:R*x1*x2^3*y1^3*y2^2*y3 -
16%:R*x2^4%:R*y1^3*y2^2*y3 + 12%:R*x1^3*x3*y1^3*y2^2*y3 +
16%:R*x1^2*x2*x3*y1^3*y2^2*y3 - 32%:R*x1*x2^2*x3*y1^3*y2^2*y3 +
24%:R*x2^3*x3*y1^3*y2^2*y3 - 8%:R*x1^2*x3^2*y1^3*y2^2*y3 +
16%:R*x1*x2*x3^2*y1^3*y2^2*y3 - 20%:R*x2^2*x3^2*y1^3*y2^2*y3 -
12%:R*x1*x3^3*y1^3*y2^2*y3 + 8%:R*x2*x3^3*y1^3*y2^2*y3 +
4%:R*x3^4%:R*y1^3*y2^2*y3 + 6%:R*x2*y1^5*y2^2*y3 - 6%:R*x3*y1^5*y2^2*y3 -
2%:R*x1^6%:R*x2*y2^3*y3 - 4%:R*x1^5*x2^2*y2^3*y3 + 14%:R*x1^4%:R*x2^3*y2^3*y3 -
6%:R*x1^3*x2^4%:R*y2^3*y3 - 12%:R*x1^2*x2^5*y2^3*y3 + 10%:R*x1*x2^6%:R*y2^3*y3 +
2%:R*x1^6%:R*x3*y2^3*y3 + 8%:R*x1^5*x2*x3*y2^3*y3 -
22%:R*x1^4%:R*x2^2*x3*y2^3*y3 + 16%:R*x1^3*x2^3*x3*y2^3*y3 +
6%:R*x1^2*x2^4%:R*x3*y2^3*y3 - 10%:R*x2^6%:R*x3*y2^3*y3 - 4%:R*x1^5*x3^2*y2^3*y3
+ 14%:R*x1^4%:R*x2*x3^2*y2^3*y3 - 16%:R*x1^3*x2^2*x3^2*y2^3*y3 -
6%:R*x1*x2^4%:R*x3^2*y2^3*y3 + 12%:R*x2^5*x3^2*y2^3*y3 -
6%:R*x1^4%:R*x3^3*y2^3*y3 + 16%:R*x1^2*x2^2*x3^3*y2^3*y3 -
16%:R*x1*x2^3*x3^3*y2^3*y3 + 6%:R*x2^4%:R*x3^3*y2^3*y3 +
6%:R*x1^3*x3^4%:R*y2^3*y3 - 14%:R*x1^2*x2*x3^4%:R*y2^3*y3 +
22%:R*x1*x2^2*x3^4%:R*y2^3*y3 - 14%:R*x2^3*x3^4%:R*y2^3*y3 +
4%:R*x1^2*x3^5*y2^3*y3 - 8%:R*x1*x2*x3^5*y2^3*y3 + 4%:R*x2^2*x3^5*y2^3*y3
- 2%:R*x1*x3^6%:R*y2^3*y3 + 2%:R*x2*x3^6%:R*y2^3*y3 + 20%:R*x1^3*x2*y1^2*y2^3*y3
- 36%:R*x1*x2^3*y1^2*y2^3*y3 + 8%:R*x2^4%:R*y1^2*y2^3*y3 -
20%:R*x1^3*x3*y1^2*y2^3*y3 + 24%:R*x1*x2^2*x3*y1^2*y2^3*y3 +
16%:R*x2^3*x3*y1^2*y2^3*y3 - 12%:R*x2^2*x3^2*y1^2*y2^3*y3 +
12%:R*x1*x3^3*y1^2*y2^3*y3 - 16%:R*x2*x3^3*y1^2*y2^3*y3 +
4%:R*x3^4%:R*y1^2*y2^3*y3 - 18%:R*x2*y1^4%:R*y2^3*y3 + 18%:R*x3*y1^4%:R*y2^3*y3 +
6%:R*x1^4%:R*y1*y2^4%:R*y3 - 10%:R*x1^3*x2*y1*y2^4%:R*y3 -
18%:R*x1^2*x2^2*y1*y2^4%:R*y3 + 34%:R*x1*x2^3*y1*y2^4%:R*y3 +
4%:R*x1^3*x3*y1*y2^4%:R*y3 - 34%:R*x2^3*x3*y1*y2^4%:R*y3 +
18%:R*x2^2*x3^2*y1*y2^4%:R*y3 - 4%:R*x1*x3^3*y1*y2^4%:R*y3 +
10%:R*x2*x3^3*y1*y2^4%:R*y3 - 6%:R*x3^4%:R*y1*y2^4%:R*y3 - 6%:R*x1*y1^3*y2^4%:R*y3 +
18%:R*x2*y1^3*y2^4%:R*y3 - 12%:R*x3*y1^3*y2^4%:R*y3 - 8%:R*x1^4%:R*y2^5*y3 +
10%:R*x1^3*x2*y2^5*y3 + 8%:R*x1^2*x2^2*y2^5*y3 - 14%:R*x1*x2^3*y2^5*y3 +
4%:R*x1^3*x3*y2^5*y3 - 4%:R*x1^2*x2*x3*y2^5*y3 - 4%:R*x1*x2^2*x3*y2^5*y3 +
14%:R*x2^3*x3*y2^5*y3 + 2%:R*x1^2*x3^2*y2^5*y3 - 4%:R*x1*x2*x3^2*y2^5*y3 -
4%:R*x2^2*x3^2*y2^5*y3 - 2%:R*x2*x3^3*y2^5*y3 + 2%:R*x3^4%:R*y2^5*y3 +
18%:R*x1*y1^2*y2^5*y3 - 6%:R*x2*y1^2*y2^5*y3 - 12%:R*x3*y1^2*y2^5*y3 -
18%:R*x1*y1*y2^6%:R*y3 + 18%:R*x3*y1*y2^6%:R*y3 + 6%:R*x1*y2^7%:R*y3 - 6%:R*x3*y2^7%:R*y3
- 3%:R*x1^ 8%:R*x2^2*y3^2 + 4%:R*x1^7%:R*x2^3*y3^2 + 5%:R*x1^6%:R*x2^4%:R*y3^2 -
6%:R*x1^5*x2^5*y3^2 - 3%:R*x1^4%:R*x2^6%:R*y3^2 + 3%:R*x1^2*x2^ 8%:R*y3^2 +
2%:R*x1*x2^9%:R*y3^2 - 2%:R*x2^10%:R*y3^2 + 6%:R*x1^ 8%:R*x2*x3*y3^2 -
12%:R*x1^7%:R*x2^2*x3*y3^2 + 6%:R*x1^5*x2^4%:R*x3*y3^2 + 6%:R*x1^4%:R*x2^5*x3*y3^2
- 12%:R*x1^2*x2^7%:R*x3*y3^2 + 6%:R*x1*x2^ 8%:R*x3*y3^2 - 3%:R*x1^ 8%:R*x3^2*y3^2 +
12%:R*x1^7%:R*x2*x3^2*y3^2 - 9%:R*x1^6%:R*x2^2*x3^2*y3^2 -
6%:R*x1^5*x2^3*x3^2*y3^2 - 12%:R*x1^4%:R*x2^4%:R*x3^2*y3^2 +
36%:R*x1^3*x2^5*x3^2*y3^2 - 9%:R*x1^2*x2^6%:R*x3^2*y3^2 -
18%:R*x1*x2^7%:R*x3^2*y3^2 + 9%:R*x2^ 8%:R*x3^2*y3^2 - 4%:R*x1^7%:R*x3^3*y3^2 -
2%:R*x1^6%:R*x2*x3^3*y3^2 + 30%:R*x1^5*x2^2*x3^3*y3^2 -
20%:R*x1^4%:R*x2^3*x3^3*y3^2 - 40%:R*x1^3*x2^4%:R*x3^3*y3^2 +
54%:R*x1^2*x2^5*x3^3*y3^2 - 18%:R*x1*x2^6%:R*x3^3*y3^2 + 6%:R*x1^6%:R*x3^4%:R*y3^2
- 36%:R*x1^5*x2*x3^4%:R*y3^2 + 72%:R*x1^4%:R*x2^2*x3^4%:R*y3^2 -
48%:R*x1^3*x2^3*x3^4%:R*y3^2 - 18%:R*x1^2*x2^4%:R*x3^4%:R*y3^2 +
36%:R*x1*x2^5*x3^4%:R*y3^2 - 12%:R*x2^6%:R*x3^4%:R*y3^2 + 12%:R*x1^5*x3^5*y3^2 -
48%:R*x1^4%:R*x2*x3^5*y3^2 + 72%:R*x1^3*x2^2*x3^5*y3^2 -
48%:R*x1^2*x2^3*x3^5*y3^2 + 12%:R*x1*x2^4%:R*x3^5*y3^2 + 5%:R*x1^4%:R*x3^6%:R*y3^2
- 20%:R*x1^3*x2*x3^6%:R*y3^2 + 30%:R*x1^2*x2^2*x3^6%:R*y3^2 -
20%:R*x1*x2^3*x3^6%:R*y3^2 + 5%:R*x2^4%:R*x3^6%:R*y3^2 + 6%:R*x1^5*x2^2*y1^2*y3^2 -
6%:R*x1^4%:R*x2^3*y1^2*y3^2 - 6%:R*x1^3*x2^4%:R*y1^2*y3^2 +
6%:R*x1^2*x2^5*y1^2*y3^2 - 12%:R*x1^5*x2*x3*y1^2*y3^2 +
18%:R*x1^4%:R*x2^2*x3*y1^2*y3^2 - 6%:R*x1^2*x2^4%:R*x3*y1^2*y3^2 +
6%:R*x1^5*x3^2*y1^2*y3^2 - 18%:R*x1^4%:R*x2*x3^2*y1^2*y3^2 +
12%:R*x1^3*x2^2*x3^2*y1^2*y3^2 + 6%:R*x1*x2^4%:R*x3^2*y1^2*y3^2 -
6%:R*x2^5*x3^2*y1^2*y3^2 + 6%:R*x1^4%:R*x3^3*y1^2*y3^2 -
12%:R*x1^2*x2^2*x3^3*y1^2*y3^2 + 6%:R*x2^4%:R*x3^3*y1^2*y3^2 -
6%:R*x1^3*x3^4%:R*y1^2*y3^2 + 18%:R*x1^2*x2*x3^4%:R*y1^2*y3^2 -
18%:R*x1*x2^2*x3^4%:R*y1^2*y3^2 + 6%:R*x2^3*x3^4%:R*y1^2*y3^2 -
6%:R*x1^2*x3^5*y1^2*y3^2 + 12%:R*x1*x2*x3^5*y1^2*y3^2 -
6%:R*x2^2*x3^5*y1^2*y3^2 - 3%:R*x1^2*x2^2*y1^4%:R*y3^2 +
2%:R*x1*x2^3*y1^4%:R*y3^2 + x2^4%:R*y1^4%:R*y3^2 + 6%:R*x1^2*x2*x3*y1^4%:R*y3^2 -
6%:R*x1*x2^2*x3*y1^4%:R*y3^2 - 3%:R*x1^2*x3^2*y1^4%:R*y3^2 +
6%:R*x1*x2*x3^2*y1^4%:R*y3^2 - 3%:R*x2^2*x3^2*y1^4%:R*y3^2 -
2%:R*x1*x3^3*y1^4%:R*y3^2 + 2%:R*x2*x3^3*y1^4%:R*y3^2 - 6%:R*x1^6%:R*x2*y1*y2*y3^2
- 4%:R*x1^5*x2^2*y1*y2*y3^2 + 18%:R*x1^4%:R*x2^3*y1*y2*y3^2 +
4%:R*x1^3*x2^4%:R*y1*y2*y3^2 - 14%:R*x1^2*x2^5*y1*y2*y3^2 +
2%:R*x2^7%:R*y1*y2*y3^2 + 6%:R*x1^6%:R*x3*y1*y2*y3^2 +
8%:R*x1^5*x2*x3*y1*y2*y3^2 - 10%:R*x1^4%:R*x2^2*x3*y1*y2*y3^2 -
28%:R*x1^3*x2^3*x3*y1*y2*y3^2 + 10%:R*x1^2*x2^4%:R*x3*y1*y2*y3^2 +
28%:R*x1*x2^5*x3*y1*y2*y3^2 - 14%:R*x2^6%:R*x3*y1*y2*y3^2 -
4%:R*x1^5*x3^2*y1*y2*y3^2 + 2%:R*x1^4%:R*x2*x3^2*y1*y2*y3^2 +
32%:R*x1^3*x2^2*x3^2*y1*y2*y3^2 - 44%:R*x1^2*x2^3*x3^2*y1*y2*y3^2 +
4%:R*x1*x2^4%:R*x3^2*y1*y2*y3^2 + 10%:R*x2^5*x3^2*y1*y2*y3^2 -
10%:R*x1^4%:R*x3^3*y1*y2*y3^2 - 20%:R*x1^3*x2*x3^3*y1*y2*y3^2 +
72%:R*x1^2*x2^2*x3^3*y1*y2*y3^2 - 44%:R*x1*x2^3*x3^3*y1*y2*y3^2 +
2%:R*x2^4%:R*x3^3*y1*y2*y3^2 + 12%:R*x1^3*x3^4%:R*y1*y2*y3^2 -
36%:R*x1^2*x2*x3^4%:R*y1*y2*y3^2 + 36%:R*x1*x2^2*x3^4%:R*y1*y2*y3^2 -
12%:R*x2^3*x3^4%:R*y1*y2*y3^2 + 12%:R*x1^2*x3^5*y1*y2*y3^2 -
24%:R*x1*x2*x3^5*y1*y2*y3^2 + 12%:R*x2^2*x3^5*y1*y2*y3^2 +
12%:R*x1^3*x2*y1^3*y2*y3^2 + 4%:R*x1^2*x2^2*y1^3*y2*y3^2 -
20%:R*x1*x2^3*y1^3*y2*y3^2 + 4%:R*x2^4%:R*y1^3*y2*y3^2 -
12%:R*x1^3*x3*y1^3*y2*y3^2 - 8%:R*x1^2*x2*x3*y1^3*y2*y3^2 +
16%:R*x1*x2^2*x3*y1^3*y2*y3^2 + 4%:R*x2^3*x3*y1^3*y2*y3^2 +
4%:R*x1^2*x3^2*y1^3*y2*y3^2 - 8%:R*x1*x2*x3^2*y1^3*y2*y3^2 +
4%:R*x2^2*x3^2*y1^3*y2*y3^2 + 12%:R*x1*x3^3*y1^3*y2*y3^2 -
12%:R*x2*x3^3*y1^3*y2*y3^2 - 6%:R*x2*y1^5*y2*y3^2 + 6%:R*x3*y1^5*y2*y3^2 +
6%:R*x1^6%:R*x2*y2^2*y3^2 + 2%:R*x1^5*x2^2*y2^2*y3^2 -
24%:R*x1^4%:R*x2^3*y2^2*y3^2 + 10%:R*x1^3*x2^4%:R*y2^2*y3^2 +
16%:R*x1^2*x2^5*y2^2*y3^2 - 12%:R*x1*x2^6%:R*y2^2*y3^2 + 2%:R*x2^7%:R*y2^2*y3^2
- 6%:R*x1^6%:R*x3*y2^2*y3^2 - 4%:R*x1^5*x2*x3*y2^2*y3^2 +
20%:R*x1^4%:R*x2^2*x3*y2^2*y3^2 - 4%:R*x1^3*x2^3*x3*y2^2*y3^2 +
4%:R*x1^2*x2^4%:R*x3*y2^2*y3^2 - 20%:R*x1*x2^5*x3*y2^2*y3^2 +
10%:R*x2^6%:R*x3*y2^2*y3^2 + 2%:R*x1^5*x3^2*y2^2*y3^2 -
4%:R*x1^4%:R*x2*x3^2*y2^2*y3^2 - 4%:R*x1^3*x2^2*x3^2*y2^2*y3^2 +
4%:R*x1^2*x2^3*x3^2*y2^2*y3^2 + 10%:R*x1*x2^4%:R*x3^2*y2^2*y3^2 -
8%:R*x2^5*x3^2*y2^2*y3^2 + 8%:R*x1^4%:R*x3^3*y2^2*y3^2 +
4%:R*x1^3*x2*x3^3*y2^2*y3^2 - 36%:R*x1^2*x2^2*x3^3*y2^2*y3^2 +
28%:R*x1*x2^3*x3^3*y2^2*y3^2 - 4%:R*x2^4%:R*x3^3*y2^2*y3^2 -
6%:R*x1^3*x3^4%:R*y2^2*y3^2 + 18%:R*x1^2*x2*x3^4%:R*y2^2*y3^2 -
18%:R*x1*x2^2*x3^4%:R*y2^2*y3^2 + 6%:R*x2^3*x3^4%:R*y2^2*y3^2 -
6%:R*x1^2*x3^5*y2^2*y3^2 + 12%:R*x1*x2*x3^5*y2^2*y3^2 -
6%:R*x2^2*x3^5*y2^2*y3^2 - 24%:R*x1^3*x2*y1^2*y2^2*y3^2 +
24%:R*x1*x2^3*y1^2*y2^2*y3^2 + 24%:R*x1^3*x3*y1^2*y2^2*y3^2 -
24%:R*x2^3*x3*y1^2*y2^2*y3^2 - 24%:R*x1*x3^3*y1^2*y2^2*y3^2 +
24%:R*x2*x3^3*y1^2*y2^2*y3^2 + 18%:R*x2*y1^4%:R*y2^2*y3^2 -
18%:R*x3*y1^4%:R*y2^2*y3^2 - 4%:R*x1^4%:R*y1*y2^3*y3^2 +
16%:R*x1^3*x2*y1*y2^3*y3^2 + 12%:R*x1^2*x2^2*y1*y2^3*y3^2 -
16%:R*x1*x2^3*y1*y2^3*y3^2 - 8%:R*x2^4%:R*y1*y2^3*y3^2 -
12%:R*x1^3*x3*y1*y2^3*y3^2 - 24%:R*x1*x2^2*x3*y1*y2^3*y3^2 +
36%:R*x2^3*x3*y1*y2^3*y3^2 + 20%:R*x1*x3^3*y1*y2^3*y3^2 -
20%:R*x2*x3^3*y1*y2^3*y3^2 + 4%:R*x1*y1^3*y2^3*y3^2 -
16%:R*x2*y1^3*y2^3*y3^2 + 12%:R*x3*y1^3*y2^3*y3^2 + 3%:R*x1^4%:R*y2^4%:R*y3^2 -
19%:R*x1^2*x2^2*y2^4%:R*y3^2 + 14%:R*x1*x2^3*y2^4%:R*y3^2 + 2%:R*x2^4%:R*y2^4%:R*y3^2
+ 2%:R*x1^2*x2*x3*y2^4%:R*y3^2 + 14%:R*x1*x2^2*x3*y2^4%:R*y3^2 -
16%:R*x2^3*x3*y2^4%:R*y3^2 - x1^2*x3^2*y2^4%:R*y3^2 +
2%:R*x1*x2*x3^2*y2^4%:R*y3^2 - x2^2*x3^2*y2^4%:R*y3^2 -
6%:R*x1*x3^3*y2^4%:R*y3^2 + 6%:R*x2*x3^3*y2^4%:R*y3^2 - 12%:R*x1*y1^2*y2^4%:R*y3^2
+ 12%:R*x3*y1^2*y2^4%:R*y3^2 + 12%:R*x1*y1*y2^5*y3^2 + 6%:R*x2*y1*y2^5*y3^2 -
18%:R*x3*y1*y2^5*y3^2 - 4%:R*x1*y2^6%:R*y3^2 - 2%:R*x2*y2^6%:R*y3^2 +
6%:R*x3*y2^6%:R*y3^2 + 2%:R*x1^6%:R*x2*y1*y3^3 - 2%:R*x1^4%:R*x2^3*y1*y3^3 -
8%:R*x1^3*x2^4%:R*y1*y3^3 + 6%:R*x1^2*x2^5*y1*y3^3 + 8%:R*x1*x2^6%:R*y1*y3^3 -
6%:R*x2^7%:R*y1*y3^3 - 2%:R*x1^6%:R*x3*y1*y3^3 - 6%:R*x1^4%:R*x2^2*x3*y1*y3^3 +
28%:R*x1^3*x2^3*x3*y1*y3^3 - 18%:R*x1^2*x2^4%:R*x3*y1*y3^3 -
12%:R*x1*x2^5*x3*y1*y3^3 + 10%:R*x2^6%:R*x3*y1*y3^3 +
6%:R*x1^4%:R*x2*x3^2*y1*y3^3 - 24%:R*x1^3*x2^2*x3^2*y1*y3^3 +
36%:R*x1^2*x2^3*x3^2*y1*y3^3 - 24%:R*x1*x2^4%:R*x3^2*y1*y3^3 +
6%:R*x2^5*x3^2*y1*y3^3 + 2%:R*x1^4%:R*x3^3*y1*y3^3 +
4%:R*x1^3*x2*x3^3*y1*y3^3 - 24%:R*x1^2*x2^2*x3^3*y1*y3^3 +
28%:R*x1*x2^3*x3^3*y1*y3^3 - 10%:R*x2^4%:R*x3^3*y1*y3^3 -
4%:R*x1^3*x2*y1^3*y3^3 + 4%:R*x1*x2^3*y1^3*y3^3 + 4%:R*x1^3*x3*y1^3*y3^3 -
4%:R*x2^3*x3*y1^3*y3^3 - 4%:R*x1*x3^3*y1^3*y3^3 + 4%:R*x2*x3^3*y1^3*y3^3 +
2%:R*x2*y1^5*y3^3 - 2%:R*x3*y1^5*y3^3 - 6%:R*x1^6%:R*x2*y2*y3^3 +
8%:R*x1^5*x2^2*y2*y3^3 + 6%:R*x1^4%:R*x2^3*y2*y3^3 - 8%:R*x1^3*x2^4%:R*y2*y3^3 -
2%:R*x1^2*x2^5*y2*y3^3 + 2%:R*x2^7%:R*y2*y3^3 + 6%:R*x1^6%:R*x3*y2*y3^3 -
16%:R*x1^5*x2*x3*y2*y3^3 + 26%:R*x1^4%:R*x2^2*x3*y2*y3^3 -
28%:R*x1^3*x2^3*x3*y2*y3^3 - 2%:R*x1^2*x2^4%:R*x3*y2*y3^3 +
28%:R*x1*x2^5*x3*y2*y3^3 - 14%:R*x2^6%:R*x3*y2*y3^3 + 8%:R*x1^5*x3^2*y2*y3^3
- 34%:R*x1^4%:R*x2*x3^2*y2*y3^3 + 56%:R*x1^3*x2^2*x3^2*y2*y3^3 -
44%:R*x1^2*x2^3*x3^2*y2*y3^3 + 16%:R*x1*x2^4%:R*x3^2*y2*y3^3 -
2%:R*x2^5*x3^2*y2*y3^3 + 2%:R*x1^4%:R*x3^3*y2*y3^3 -
20%:R*x1^3*x2*x3^3*y2*y3^3 + 48%:R*x1^2*x2^2*x3^3*y2*y3^3 -
44%:R*x1*x2^3*x3^3*y2*y3^3 + 14%:R*x2^4%:R*x3^3*y2*y3^3 +
12%:R*x1^3*x2*y1^2*y2*y3^3 - 4%:R*x1^2*x2^2*y1^2*y2*y3^3 -
4%:R*x1*x2^3*y1^2*y2*y3^3 - 4%:R*x2^4%:R*y1^2*y2*y3^3 -
12%:R*x1^3*x3*y1^2*y2*y3^3 + 8%:R*x1^2*x2*x3*y1^2*y2*y3^3 -
16%:R*x1*x2^2*x3*y1^2*y2*y3^3 + 20%:R*x2^3*x3*y1^2*y2*y3^3 -
4%:R*x1^2*x3^2*y1^2*y2*y3^3 + 8%:R*x1*x2*x3^2*y1^2*y2*y3^3 -
4%:R*x2^2*x3^2*y1^2*y2*y3^3 + 12%:R*x1*x3^3*y1^2*y2*y3^3 -
12%:R*x2*x3^3*y1^2*y2*y3^3 - 6%:R*x2*y1^4%:R*y2*y3^3 + 6%:R*x3*y1^4%:R*y2*y3^3 -
4%:R*x1^4%:R*y1*y2^2*y3^3 - 8%:R*x1^3*x2*y1*y2^2*y3^3 +
20%:R*x1^2*x2^2*y1*y2^2*y3^3 - 24%:R*x1*x2^3*y1*y2^2*y3^3 +
16%:R*x2^4%:R*y1*y2^2*y3^3 + 12%:R*x1^3*x3*y1*y2^2*y3^3 -
16%:R*x1^2*x2*x3*y1*y2^2*y3^3 + 32%:R*x1*x2^2*x3*y1*y2^2*y3^3 -
28%:R*x2^3*x3*y1*y2^2*y3^3 + 8%:R*x1^2*x3^2*y1*y2^2*y3^3 -
16%:R*x1*x2*x3^2*y1*y2^2*y3^3 + 8%:R*x2^2*x3^2*y1*y2^2*y3^3 -
12%:R*x1*x3^3*y1*y2^2*y3^3 + 12%:R*x2*x3^3*y1*y2^2*y3^3 +
4%:R*x1*y1^3*y2^2*y3^3 - 4%:R*x3*y1^3*y2^2*y3^3 + 8%:R*x1^4%:R*y2^3*y3^3 -
16%:R*x1^3*x2*y2^3*y3^3 + 8%:R*x1^2*x2^2*y2^3*y3^3 +
8%:R*x1*x2^3*y2^3*y3^3 - 8%:R*x2^4%:R*y2^3*y3^3 - 4%:R*x1^3*x3*y2^3*y3^3 +
8%:R*x1^2*x2*x3*y2^3*y3^3 - 16%:R*x1*x2^2*x3*y2^3*y3^3 +
12%:R*x2^3*x3*y2^3*y3^3 - 4%:R*x1^2*x3^2*y2^3*y3^3 +
8%:R*x1*x2*x3^2*y2^3*y3^3 - 4%:R*x2^2*x3^2*y2^3*y3^3 +
4%:R*x1*x3^3*y2^3*y3^3 - 4%:R*x2*x3^3*y2^3*y3^3 - 12%:R*x1*y1^2*y2^3*y3^3
+ 16%:R*x2*y1^2*y2^3*y3^3 - 4%:R*x3*y1^2*y2^3*y3^3 + 12%:R*x1*y1*y2^4%:R*y3^3
- 18%:R*x2*y1*y2^4%:R*y3^3 + 6%:R*x3*y1*y2^4%:R*y3^3 - 4%:R*x1*y2^5*y3^3 +
6%:R*x2*y2^5*y3^3 - 2%:R*x3*y2^5*y3^3 + 2%:R*x1^6%:R*x2*y3^4 -
6%:R*x1^5*x2^2*y3^4 + 4%:R*x1^4%:R*x2^3*y3^4 + 4%:R*x1^3*x2^4%:R*y3^4 -
6%:R*x1^2*x2^5*y3^4 + 2%:R*x1*x2^6%:R*y3^4 - 2%:R*x1^6%:R*x3*y3^4 +
12%:R*x1^5*x2*x3*y3^4 - 24%:R*x1^4%:R*x2^2*x3*y3^4 + 16%:R*x1^3*x2^3*x3*y3^4
+ 6%:R*x1^2*x2^4%:R*x3*y3^4 - 12%:R*x1*x2^5*x3*y3^4 + 4%:R*x2^6%:R*x3*y3^4 -
6%:R*x1^5*x3^2*y3^4 + 24%:R*x1^4%:R*x2*x3^2*y3^4 - 36%:R*x1^3*x2^2*x3^2*y3^4
+ 24%:R*x1^2*x2^3*x3^2*y3^4 - 6%:R*x1*x2^4%:R*x3^2*y3^4 - 4%:R*x1^4%:R*x3^3*y3^4
+ 16%:R*x1^3*x2*x3^3*y3^4 - 24%:R*x1^2*x2^2*x3^3*y3^4 +
16%:R*x1*x2^3*x3^3*y3^4 - 4%:R*x2^4%:R*x3^3*y3^4 - 2%:R*x1^3*x2*y1^2*y3^4 +
3%:R*x1^2*x2^2*y1^2*y3^4 - x2^4%:R*y1^2*y3^4 + 2%:R*x1^3*x3*y1^2*y3^4 -
6%:R*x1^2*x2*x3*y1^2*y3^4 + 6%:R*x1*x2^2*x3*y1^2*y3^4 -
2%:R*x2^3*x3*y1^2*y3^4 + 3%:R*x1^2*x3^2*y1^2*y3^4 -
6%:R*x1*x2*x3^2*y1^2*y3^4 + 3%:R*x2^2*x3^2*y1^2*y3^4 +
6%:R*x1^4%:R*y1*y2*y3^4 - 2%:R*x1^3*x2*y1*y2*y3^4 -
24%:R*x1^2*x2^2*y1*y2*y3^4 + 30%:R*x1*x2^3*y1*y2*y3^4 -
10%:R*x2^4%:R*y1*y2*y3^4 - 4%:R*x1^3*x3*y1*y2*y3^4 +
12%:R*x1^2*x2*x3*y1*y2*y3^4 - 12%:R*x1*x2^2*x3*y1*y2*y3^4 +
4%:R*x2^3*x3*y1*y2*y3^4 - 6%:R*x1^2*x3^2*y1*y2*y3^4 +
12%:R*x1*x2*x3^2*y1*y2*y3^4 - 6%:R*x2^2*x3^2*y1*y2*y3^4 -
6%:R*x1*y1^3*y2*y3^4 + 6%:R*x2*y1^3*y2*y3^4 - 7%:R*x1^4%:R*y2^2*y3^4 +
8%:R*x1^3*x2*y2^2*y3^4 + 15%:R*x1^2*x2^2*y2^2*y3^4 -
26%:R*x1*x2^3*y2^2*y3^4 + 10%:R*x2^4%:R*y2^2*y3^4 + 2%:R*x1^3*x3*y2^2*y3^4 -
6%:R*x1^2*x2*x3*y2^2*y3^4 + 6%:R*x1*x2^2*x3*y2^2*y3^4 -
2%:R*x2^3*x3*y2^2*y3^4 + 3%:R*x1^2*x3^2*y2^2*y3^4 -
6%:R*x1*x2*x3^2*y2^2*y3^4 + 3%:R*x2^2*x3^2*y2^2*y3^4 +
18%:R*x1*y1^2*y2^2*y3^4 - 18%:R*x2*y1^2*y2^2*y3^4 - 18%:R*x1*y1*y2^3*y3^4
+ 18%:R*x2*y1*y2^3*y3^4 + 6%:R*x1*y2^4%:R*y3^4 - 6%:R*x2*y2^4%:R*y3^4 -
2%:R*x1^4%:R*y1*y3^5 + 2%:R*x1^3*x2*y1*y3^5 + 6%:R*x1^2*x2^2*y1*y3^5 -
10%:R*x1*x2^3*y1*y3^5 + 4%:R*x2^4%:R*y1*y3^5 + 2%:R*x1*y1^3*y3^5 -
2%:R*x2*y1^3*y3^5 + 6%:R*x1^3*x2*y2*y3^5 - 18%:R*x1^2*x2^2*y2*y3^5 +
18%:R*x1*x2^3*y2*y3^5 - 6%:R*x2^4%:R*y2*y3^5 - 6%:R*x1*y1^2*y2*y3^5 +
6%:R*x2*y1^2*y2*y3^5 + 6%:R*x1*y1*y2^2*y3^5 - 6%:R*x2*y1*y2^2*y3^5 -
2%:R*x1*y2^3*y3^5 + 2%:R*x2*y2^3*y3^5 + x1^4%:R*y3^6 - 4%:R*x1^3*x2*y3^6 +
6%:R*x1^2*x2^2*y3^6 - 4%:R*x1*x2^3*y3^6 + x2^4%:R*y3^6.
End Polynomials.
Lemma from_sander_int (x1 x2 x3 y1 y2 y3 : int) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 6.881 secs *)
Time Qed. (* 0.95 secs *)
Lemma from_sander_rat (x1 x2 x3 y1 y2 y3 : rat) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 6.805 secs *)
Time Qed. (* 0.94 secs *)
Lemma from_sander_abstract (R : comUnitRingType) (x1 x2 x3 y1 y2 y3 : R) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 6.303 secs *)
Time Qed. (* 0.913 secs *)
Ltac ring_reflection ::= ring_reflection_no_check.
Lemma from_sander_int_no_check (x1 x2 x3 y1 y2 y3 : int) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 4.93 secs *)
Time Qed. (* 0.903 secs *)
Lemma from_sander_rat_no_check (x1 x2 x3 y1 y2 y3 : rat) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 4.772 secs *)
Time Qed. (* 0.838 secs *)
Lemma from_sander_abstract_no_check
(R : comUnitRingType) (x1 x2 x3 y1 y2 y3 : R) :
f1 x1 x2 x3 y1 y2 y3 * f2 x1 x2 x3 y1 y2 y3 = f3 x1 x2 x3 y1 y2 y3.
Proof.
rewrite /f1 /f2 /f3.
Time ring. (* 5.023 secs *)
Time Qed. (* 1.005 secs *)
|
