Module mathcomp.test_suite.test_ring_from_sander
From mathcomp Require Import all_boot ssralg ssrnum ssrint rat ring_tactic.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*x1^6*x2^3 -
6*x1^4*x2^5 + 6*x1^2*x2^7 - 2*x2^9 - 6*x1^6*x2^ 2*x3 +
6*x1^5*x2^3*x3 + 12*x1^4*x2^4*x3 - 12*x1^3*x2^5*x3 -
6*x1^2*x2^6*x3 + 6*x1*x2^7*x3 + 6*x1^6*x2*x3^2 -
18*x1^5*x2^2*x3^2 + 6*x1^4*x2^3*x3^2 + 24*x1^3*x2^4*x3^2 -
18*x1^2*x2^5*x3^2 - 6*x1*x2^6*x3^2 + 6*x2^7*x3^2 - 2*x1^6*x3^3
+ 18*x1^5*x2*x3^3 - 30*x1^4*x2^2*x3^3 + 2*x1^3*x2^3*x3^3 +
24*x1^2*x2^4*x3^3 - 12*x1*x2^5*x3^3 - 6*x1^5*x3^4 +
24*x1^4*x2*x3^4 - 30*x1^3*x2^2*x3^4 + 6*x1^2*x2^3*x3^4 +
12*x1*x2^4*x3^4 - 6*x2^5*x3^4 - 6*x1^4*x3^5 + 18*x1^3*x2*x3^5 -
18*x1^2*x2^2*x3^5 + 6*x1*x2^3*x3^5 - 2*x1^3*x3^6 +
6*x1^2*x2*x3^6 - 6*x1*x2^2*x3^6 + 2*x2^3*x3^6 -
3*x1^3*x2^3*y1^2 + 3*x1*x2^5*y1^2 + 9*x1^3*x2^2*x3*y1^2 -
6*x1^2*x2^3*x3*y1^2 - 6*x1*x2^4*x3*y1^2 + 3*x2^5*x3*y1^2 -
9*x1^3*x2*x3^2*y1^2 + 18*x1^2*x2^2*x3^2*y1^2 -
3*x1*x2^3*x3^2*y1^2 - 6*x2^4*x3^2*y1^2 + 3*x1^3*x3^3*y1^2 -
18*x1^2*x2*x3^3*y1^2 + 15*x1*x2^2*x3^3*y1^2 + 6*x1^2*x3^4*y1^2
- 12*x1*x2*x3^4*y1^2 + 6*x2^2*x3^4*y1^2 + 3*x1*x3^5*y1^2 -
3*x2*x3^5*y1^2 + x2^3*y1^4 - 3*x2^2*x3*y1^4 + 3*x2*x3^2*y1^4 -
x3^3*y1^4 + 8*x1^3*x2^3*y1*y2 - 2*x1^2*x2^4*y1*y2 -
8*x1*x2^5*y1*y2 + 2*x2^6*y1*y2 - 18*x1^3*x2^2*x3*y1*y2 +
14*x1^2*x2^3*x3*y1*y2 + 8*x1*x2^4*x3*y1*y2 - 4*x2^5*x3*y1*y2 +
12*x1^3*x2*x3^2*y1*y2 - 30*x1^2*x2^2*x3^2*y1*y2 +
12*x1*x2^3*x3^2*y1*y2 + 6*x2^4*x3^2*y1*y2 - 2*x1^3*x3^3*y1*y2 +
26*x1^2*x2*x3^3*y1*y2 - 22*x1*x2^2*x3^3*y1*y2 -
2*x2^3*x3^3*y1*y2 - 8*x1^2*x3^4*y1*y2 + 16*x1*x2*x3^4*y1*y2 -
8*x2^2*x3^4*y1*y2 - 6*x1*x3^5*y1*y2 + 6*x2*x3^5*y1*y2 -
6*x2^3*y1^3*y2 + 12*x2^2*x3*y1^3*y2 - 6*x2*x3^2*y1^3*y2 -
3*x1^5*x2*y2^2 + 2*x1^4*x2^2*y2^2 + 3*x1^3*x2^3*y2^2 -
4*x1^2*x2^4*y2^2 + 2*x2^6*y2^2 + 3*x1^5*x3*y2^2 -
4*x1^4*x2*x3*y2^2 + 4*x1^3*x2^2*x3*y2^2 + x1^2*x2^3*x3*y2^2 -
4*x1*x2^4*x3*y2^2 + 2*x1^4*x3^2*y2^2 - 5*x1^3*x2*x3^2*y2^2 +
6*x1^2*x2^2*x3^2*y2^2 + x1*x2^3*x3^2*y2^2 - 4*x2^4*x3^2*y2^2 -
2*x1^3*x3^3*y2^2 - 5*x1^2*x2*x3^3*y2^2 + 4*x1*x2^2*x3^3*y2^2 +
3*x2^3*x3^3*y2^2 + 2*x1^2*x3^4*y2^2 - 4*x1*x2*x3^4*y2^2 +
2*x2^2*x3^4*y2^2 + 3*x1*x3^5*y2^2 - 3*x2*x3^5*y2^2 +
3*x1^2*x2*y1^2*y2^2 - x1*x2^2*y1^2*y2^2 + 10*x2^3*y1^2*y2^2 -
3*x1^2*x3*y1^2*y2^2 + 2*x1*x2*x3*y1^2*y2^2 -
17*x2^2*x3*y1^2*y2^2 - x1*x3^2*y1^2*y2^2 + x2*x3^2*y1^2*y2^2 +
6*x3^3*y1^2*y2^2 - 2*x1^3*y1*y2^3 - 4*x1^2*x2*y1*y2^3 +
4*x1*x2^2*y1*y2^3 - 8*x2^3*y1*y2^3 + 4*x1^2*x3*y1*y2^3 +
8*x2^2*x3*y1*y2^3 + 2*x1*x3^2*y1*y2^3 + 4*x2*x3^2*y1*y2^3 -
8*x3^3*y1*y2^3 + 2*y1^3*y2^3 + 3*x1^3*y2^4 - 2*x1^2*x2*y2^4 +
2*x2^3*y2^4 - x1^2*x3*y2^4 - 2*x1*x2*x3*y2^4 - x1*x3^2*y2^4 -
2*x2*x3^2*y2^4 + 3*x3^3*y2^4 - 6*y1^2*y2^4 + 6*y1*y2^5 - 2*y2^6
- 6*x1^3*x2^3*y1*y3 + 6*x1^2*x2^4*y1*y3 + 6*x1*x2^5*y1*y3 -
6*x2^6*y1*y3 + 12*x1^3*x2^2*x3*y1*y3 - 18*x1^2*x2^3*x3*y1*y3 +
6*x2^5*x3*y1*y3 - 6*x1^3*x2*x3^2*y1*y3 +
18*x1^2*x2^2*x3^2*y1*y3 - 18*x1*x2^3*x3^2*y1*y3 +
6*x2^4*x3^2*y1*y3 - 6*x1^2*x2*x3^3*y1*y3 +
12*x1*x2^2*x3^3*y1*y3 - 6*x2^3*x3^3*y1*y3 + 4*x2^3*y1^3*y3 -
6*x2^2*x3*y1^3*y3 + 2*x3^3*y1^3*y3 + 6*x1^5*x2*y2*y3 -
8*x1^4*x2^2*y2*y3 - 2*x1^3*x2^3*y2*y3 + 6*x1^2*x2^4*y2*y3 -
4*x1*x2^5*y2*y3 + 2*x2^6*y2*y3 - 6*x1^5*x3*y2*y3 +
16*x1^4*x2*x3*y2*y3 - 22*x1^3*x2^2*x3*y2*y3 +
12*x1^2*x2^3*x3*y2*y3 + 8*x1*x2^4*x3*y2*y3 - 8*x2^5*x3*y2*y3 -
8*x1^4*x3^2*y2*y3 + 26*x1^3*x2*x3^2*y2*y3 -
30*x1^2*x2^2*x3^2*y2*y3 + 14*x1*x2^3*x3^2*y2*y3 -
2*x2^4*x3^2*y2*y3 - 2*x1^3*x3^3*y2*y3 + 12*x1^2*x2*x3^3*y2*y3 -
18*x1*x2^2*x3^3*y2*y3 + 8*x2^3*x3^3*y2*y3 -
6*x1^2*x2*y1^2*y2*y3 + 4*x1*x2^2*y1^2*y2*y3 -
10*x2^3*y1^2*y2*y3 + 6*x1^2*x3*y1^2*y2*y3 -
8*x1*x2*x3*y1^2*y2*y3 + 20*x2^2*x3*y1^2*y2*y3 +
4*x1*x3^2*y1^2*y2*y3 - 4*x2*x3^2*y1^2*y2*y3 - 6*x3^3*y1^2*y2*y3
+ 6*x1^3*y1*y2^2*y3 + 8*x1^2*x2*y1*y2^2*y3 -
18*x1*x2^2*y1*y2^2*y3 + 16*x2^3*y1*y2^2*y3 -
8*x1^2*x3*y1*y2^2*y3 + 8*x1*x2*x3*y1*y2^2*y3 -
18*x2^2*x3*y1*y2^2*y3 - 8*x1*x3^2*y1*y2^2*y3 +
8*x2*x3^2*y1*y2^2*y3 + 6*x3^3*y1*y2^2*y3 - 6*y1^3*y2^2*y3 -
8*x1^3*y2^3*y3 + 4*x1^2*x2*y2^3*y3 + 8*x1*x2^2*y2^3*y3 -
8*x2^3*y2^3*y3 + 2*x1^2*x3*y2^3*y3 + 4*x2^2*x3*y2^3*y3 +
4*x1*x3^2*y2^3*y3 - 4*x2*x3^2*y2^3*y3 - 2*x3^3*y2^3*y3 +
18*y1^2*y2^3*y3 - 18*y1*y2^4*y3 + 6*y2^5*y3 - 3*x1^5*x2*y3^2 +
6*x1^4*x2^2*y3^2 - 6*x1^2*x2^4*y3^2 + 3*x1*x2^5*y3^2 +
3*x1^5*x3*y3^2 - 12*x1^4*x2*x3*y3^2 + 15*x1^3*x2^2*x3*y3^2 -
3*x1^2*x2^3*x3*y3^2 - 6*x1*x2^4*x3*y3^2 + 3*x2^5*x3*y3^2 +
6*x1^4*x3^2*y3^2 - 18*x1^3*x2*x3^2*y3^2 +
18*x1^2*x2^2*x3^2*y3^2 - 6*x1*x2^3*x3^2*y3^2 + 3*x1^3*x3^3*y3^2
- 9*x1^2*x2*x3^3*y3^2 + 9*x1*x2^2*x3^3*y3^2 - 3*x2^3*x3^3*y3^2
+ 3*x1^2*x2*y1^2*y3^2 - 3*x1*x2^2*y1^2*y3^2 -
3*x1^2*x3*y1^2*y3^2 + 6*x1*x2*x3*y1^2*y3^2 -
3*x2^2*x3*y1^2*y3^2 - 3*x1*x3^2*y1^2*y3^2 + 3*x2*x3^2*y1^2*y3^2
- 6*x1^3*y1*y2*y3^2 - 4*x1^2*x2*y1*y2*y3^2 +
20*x1*x2^2*y1*y2*y3^2 - 10*x2^3*y1*y2*y3^2 +
4*x1^2*x3*y1*y2*y3^2 - 8*x1*x2*x3*y1*y2*y3^2 +
4*x2^2*x3*y1*y2*y3^2 + 6*x1*x3^2*y1*y2*y3^2 -
6*x2*x3^2*y1*y2*y3^2 + 6*y1^3*y2*y3^2 + 6*x1^3*y2^2*y3^2 +
x1^2*x2*y2^2*y3^2 - 17*x1*x2^2*y2^2*y3^2 + 10*x2^3*y2^2*y3^2 -
x1^2*x3*y2^2*y3^2 + 2*x1*x2*x3*y2^2*y3^2 - x2^2*x3*y2^2*y3^2 -
3*x1*x3^2*y2^2*y3^2 + 3*x2*x3^2*y2^2*y3^2 - 18*y1^2*y2^2*y3^2 +
18*y1*y2^3*y3^2 - 6*y2^4*y3^2 + 2*x1^3*y1*y3^3 -
6*x1*x2^2*y1*y3^3 + 4*x2^3*y1*y3^3 - 2*y1^3*y3^3 -
6*x1^2*x2*y2*y3^3 + 12*x1*x2^2*y2*y3^3 - 6*x2^3*y2*y3^3 +
6*y1^2*y2*y3^3 - 6*y1*y2^2*y3^3 + 2*y2^3*y3^3 - x1^3*y3^4 +
3*x1^2*x2*y3^4 - 3*x1*x2^2*y3^4 + x2^3*y3^4.
Definition f3 := 2*x1^9*x2^4 -
8*x1^7*x2^6 + 12*x1^5*x2^8 - 8*x1^3*x2^10 + 2*x1*x2^12 -
8*x1^9*x2^3*x3 + 6*x1^ 8*x2^4*x3 + 24*x1^7*x2^5*x3 -
16*x1^6*x2^6*x3 - 24*x1^5*x2^7*x3 + 12*x1^4*x2^ 8*x3 +
8*x1^3*x2^9*x3 - 2*x2^12*x3 + 12*x1^9*x2^2*x3^2 -
24*x1^ 8*x2^3*x3^2 - 12*x1^7*x2^4*x3^2 + 48*x1^6*x2^5*x3^2 -
12*x1^5*x2^6*x3^2 - 24*x1^4*x2^7*x3^2 + 12*x1^3*x2^ 8*x3^2 -
8*x1^9*x2*x3^3 + 36*x1^ 8*x2^2*x3^3 - 32*x1^7*x2^3*x3^3 -
36*x1^6*x2^4*x3^3 + 48*x1^5*x2^5*x3^3 + 4*x1^4*x2^6*x3^3 -
12*x1^2*x2^ 8*x3^3 - 8*x1*x2^9*x3^3 + 8*x2^10*x3^3 + 2*x1^9*x3^4 -
24*x1^ 8*x2*x3^4 + 48*x1^7*x2^2*x3^4 - 16*x1^6*x2^3*x3^4 -
18*x1^5*x2^4*x3^4 - 4*x1^3*x2^6*x3^4 + 24*x1^2*x2^7*x3^4 -
12*x1*x2^ 8*x3^4 + 6*x1^ 8*x3^5 - 24*x1^7*x2*x3^5 +
24*x1^6*x2^2*x3^5 + 18*x1^4*x2^4*x3^5 - 48*x1^3*x2^5*x3^5 +
12*x1^2*x2^6*x3^5 + 24*x1*x2^7*x3^5 - 12*x2^ 8*x3^5 + 4*x1^7*x3^6
- 24*x1^5*x2^2*x3^6 + 16*x1^4*x2^3*x3^6 + 36*x1^3*x2^4*x3^6 -
48*x1^2*x2^5*x3^6 + 16*x1*x2^6*x3^6 - 4*x1^6*x3^7 +
24*x1^5*x2*x3^7 - 48*x1^4*x2^2*x3^7 + 32*x1^3*x2^3*x3^7 +
12*x1^2*x2^4*x3^7 - 24*x1*x2^5*x3^7 + 8*x2^6*x3^7 - 6*x1^5*x3^8 +
24*x1^4*x2*x3^8 - 36*x1^3*x2^2*x3^8 + 24*x1^2*x2^3*x3^8 -
6*x1*x2^4*x3^8 - 2*x1^4*x3^9 + 8*x1^3*x2*x3^9 - 12*x1^2*x2^2*x3^9
+ 8*x1*x2^3*x3^9 - 2*x2^4*x3^9 - 5*x1^6*x2^4*y1^2 +
12*x1^4*x2^6*y1^2 - 9*x1^2*x2^ 8*y1^2 + 2*x2^10*y1^2 +
20*x1^6*x2^3*x3*y1^2 - 12*x1^5*x2^4*x3*y1^2 -
36*x1^4*x2^5*x3*y1^2 + 18*x1^3*x2^6*x3*y1^2 +
18*x1^2*x2^7*x3*y1^2 - 6*x1*x2^ 8*x3*y1^2 - 2*x2^9*x3*y1^2 -
30*x1^6*x2^2*x3^2*y1^2 + 48*x1^5*x2^3*x3^2*y1^2 +
18*x1^4*x2^4*x3^2*y1^2 - 54*x1^3*x2^5*x3^2*y1^2 +
9*x1^2*x2^6*x3^2*y1^2 + 12*x1*x2^7*x3^2*y1^2 - 3*x2^ 8*x3^2*y1^2 +
20*x1^6*x2*x3^3*y1^2 - 72*x1^5*x2^2*x3^3*y1^2 +
48*x1^4*x2^3*x3^3*y1^2 + 40*x1^3*x2^4*x3^3*y1^2 -
36*x1^2*x2^5*x3^3*y1^2 - 5*x1^6*x3^4*y1^2 + 48*x1^5*x2*x3^4*y1^2
- 72*x1^4*x2^2*x3^4*y1^2 + 20*x1^3*x2^3*x3^4*y1^2 +
12*x1^2*x2^4*x3^4*y1^2 - 6*x1*x2^5*x3^4*y1^2 + 3*x2^6*x3^4*y1^2 -
12*x1^5*x3^5*y1^2 + 36*x1^4*x2*x3^5*y1^2 - 30*x1^3*x2^2*x3^5*y1^2
+ 6*x1^2*x2^3*x3^5*y1^2 - 6*x1*x2^4*x3^5*y1^2 + 6*x2^5*x3^5*y1^2
- 6*x1^4*x3^6*y1^2 + 2*x1^3*x2*x3^6*y1^2 + 9*x1^2*x2^2*x3^6*y1^2
- 5*x2^4*x3^6*y1^2 + 4*x1^3*x3^7*y1^2 - 12*x1^2*x2*x3^7*y1^2 +
12*x1*x2^2*x3^7*y1^2 - 4*x2^3*x3^7*y1^2 + 3*x1^2*x3^ 8*y1^2 -
6*x1*x2*x3^ 8*y1^2 + 3*x2^2*x3^ 8*y1^2 + 4*x1^3*x2^4*y1^4 -
4*x1*x2^6*y1^4 - 16*x1^3*x2^3*x3*y1^4 + 6*x1^2*x2^4*x3*y1^4 +
12*x1*x2^5*x3*y1^4 - 2*x2^6*x3*y1^4 + 24*x1^3*x2^2*x3^2*y1^4 -
24*x1^2*x2^3*x3^2*y1^4 - 6*x1*x2^4*x3^2*y1^4 + 6*x2^5*x3^2*y1^4 -
16*x1^3*x2*x3^3*y1^4 + 36*x1^2*x2^2*x3^3*y1^4 -
16*x1*x2^3*x3^3*y1^4 - 4*x2^4*x3^3*y1^4 + 4*x1^3*x3^4*y1^4 -
24*x1^2*x2*x3^4*y1^4 + 24*x1*x2^2*x3^4*y1^4 - 4*x2^3*x3^4*y1^4 +
6*x1^2*x3^5*y1^4 - 12*x1*x2*x3^5*y1^4 + 6*x2^2*x3^5*y1^4 +
2*x1*x3^6*y1^4 - 2*x2*x3^6*y1^4 - x2^4*y1^6 + 4*x2^3*x3*y1^6 -
6*x2^2*x3^2*y1^6 + 4*x2*x3^3*y1^6 - x3^4*y1^6 + 8*x1^6*x2^4*y1*y2
- 2*x1^5*x2^5*y1*y2 - 16*x1^4*x2^6*y1*y2 + 4*x1^3*x2^7*y1*y2 +
8*x1^2*x2^ 8*y1*y2 - 2*x1*x2^9*y1*y2 - 26*x1^6*x2^3*x3*y1*y2 +
16*x1^5*x2^4*x3*y1*y2 + 34*x1^4*x2^5*x3*y1*y2 -
12*x1^3*x2^6*x3*y1*y2 - 10*x1^2*x2^7*x3*y1*y2 -
4*x1*x2^ 8*x3*y1*y2 + 2*x2^9*x3*y1*y2 + 30*x1^6*x2^2*x3^2*y1*y2 -
44*x1^5*x2^3*x3^2*y1*y2 - 8*x1^4*x2^4*x3^2*y1*y2 +
22*x1^3*x2^5*x3^2*y1*y2 + 2*x1^2*x2^6*x3^2*y1*y2 +
2*x1*x2^7*x3^2*y1*y2 - 4*x2^ 8*x3^2*y1*y2 - 14*x1^6*x2*x3^3*y1*y2
+ 56*x1^5*x2^2*x3^3*y1*y2 - 24*x1^4*x2^3*x3^3*y1*y2 -
32*x1^3*x2^4*x3^3*y1*y2 - 14*x1^2*x2^5*x3^3*y1*y2 +
24*x1*x2^6*x3^3*y1*y2 + 4*x2^7*x3^3*y1*y2 + 2*x1^6*x3^4*y1*y2 -
34*x1^5*x2*x3^4*y1*y2 + 20*x1^4*x2^2*x3^4*y1*y2 +
32*x1^3*x2^3*x3^4*y1*y2 + 4*x1^2*x2^4*x3^4*y1*y2 -
26*x1*x2^5*x3^4*y1*y2 + 2*x2^6*x3^4*y1*y2 + 8*x1^5*x3^5*y1*y2 -
10*x1^4*x2*x3^5*y1*y2 - 28*x1^3*x2^2*x3^5*y1*y2 +
40*x1^2*x2^3*x3^5*y1*y2 + 4*x1*x2^4*x3^5*y1*y2 -
14*x2^5*x3^5*y1*y2 + 4*x1^4*x3^6*y1*y2 + 22*x1^3*x2*x3^6*y1*y2 -
48*x1^2*x2^2*x3^6*y1*y2 + 14*x1*x2^3*x3^6*y1*y2 +
8*x2^4*x3^6*y1*y2 - 8*x1^3*x3^7*y1*y2 + 24*x1^2*x2*x3^7*y1*y2 -
24*x1*x2^2*x3^7*y1*y2 + 8*x2^3*x3^7*y1*y2 - 6*x1^2*x3^ 8*y1*y2 +
12*x1*x2*x3^ 8*y1*y2 - 6*x2^2*x3^ 8*y1*y2 - 14*x1^3*x2^4*y1^3*y2 +
2*x1^2*x2^5*y1^3*y2 + 14*x1*x2^6*y1^3*y2 - 2*x2^7*y1^3*y2 +
44*x1^3*x2^3*x3*y1^3*y2 - 16*x1^2*x2^4*x3*y1^3*y2 -
28*x1*x2^5*x3*y1^3*y2 - 48*x1^3*x2^2*x3^2*y1^3*y2 +
44*x1^2*x2^3*x3^2*y1^3*y2 + 2*x1*x2^4*x3^2*y1^3*y2 +
2*x2^5*x3^2*y1^3*y2 + 20*x1^3*x2*x3^3*y1^3*y2 -
56*x1^2*x2^2*x3^3*y1^3*y2 + 28*x1*x2^3*x3^3*y1^3*y2 +
8*x2^4*x3^3*y1^3*y2 - 2*x1^3*x3^4*y1^3*y2 +
34*x1^2*x2*x3^4*y1^3*y2 - 26*x1*x2^2*x3^4*y1^3*y2 -
6*x2^3*x3^4*y1^3*y2 - 8*x1^2*x3^5*y1^3*y2 + 16*x1*x2*x3^5*y1^3*y2
- 8*x2^2*x3^5*y1^3*y2 - 6*x1*x3^6*y1^3*y2 + 6*x2*x3^6*y1^3*y2 +
6*x2^4*y1^5*y2 - 18*x2^3*x3*y1^5*y2 + 18*x2^2*x3^2*y1^5*y2 -
6*x2*x3^3*y1^5*y2 - 3*x1^ 8*x2^2*y2^2 + 4*x1^7*x2^3*y2^2 +
6*x1^6*x2^4*y2^2 - 12*x1^5*x2^5*y2^2 - 3*x1^4*x2^6*y2^2 +
12*x1^3*x2^7*y2^2 - 4*x1*x2^9*y2^2 + 6*x1^ 8*x2*x3*y2^2 -
12*x1^7*x2^2*x3*y2^2 + 2*x1^6*x2^3*x3*y2^2 + 18*x1^5*x2^4*x3*y2^2
- 12*x1^4*x2^5*x3*y2^2 - 6*x1^3*x2^6*x3*y2^2 + 4*x2^9*x3*y2^2 -
3*x1^ 8*x3^2*y2^2 + 12*x1^7*x2*x3^2*y2^2 - 21*x1^6*x2^2*x3^2*y2^2
+ 6*x1^5*x2^3*x3^2*y2^2 + 18*x1^4*x2^4*x3^2*y2^2 -
12*x1^3*x2^5*x3^2*y2^2 - 4*x1^7*x3^3*y2^2 + 12*x1^6*x2*x3^3*y2^2
- 18*x1^5*x2^2*x3^3*y2^2 + 4*x1^4*x2^3*x3^3*y2^2 +
12*x1^2*x2^5*x3^3*y2^2 + 6*x1*x2^6*x3^3*y2^2 - 12*x2^7*x3^3*y2^2
+ x1^6*x3^4*y2^2 + 6*x1^5*x2*x3^4*y2^2 - 4*x1^3*x2^3*x3^4*y2^2 -
18*x1^2*x2^4*x3^4*y2^2 + 12*x1*x2^5*x3^4*y2^2 + 3*x2^6*x3^4*y2^2
- 6*x1^4*x2*x3^5*y2^2 + 18*x1^3*x2^2*x3^5*y2^2 -
6*x1^2*x2^3*x3^5*y2^2 - 18*x1*x2^4*x3^5*y2^2 + 12*x2^5*x3^5*y2^2
- x1^4*x3^6*y2^2 - 12*x1^3*x2*x3^6*y2^2 + 21*x1^2*x2^2*x3^6*y2^2
- 2*x1*x2^3*x3^6*y2^2 - 6*x2^4*x3^6*y2^2 + 4*x1^3*x3^7*y2^2 -
12*x1^2*x2*x3^7*y2^2 + 12*x1*x2^2*x3^7*y2^2 - 4*x2^3*x3^7*y2^2 +
3*x1^2*x3^ 8*y2^2 - 6*x1*x2*x3^ 8*y2^2 + 3*x2^2*x3^ 8*y2^2 +
6*x1^5*x2^2*y1^2*y2^2 - 6*x1^4*x2^3*y1^2*y2^2 +
4*x1^3*x2^4*y1^2*y2^2 + 8*x1^2*x2^5*y1^2*y2^2 -
10*x1*x2^6*y1^2*y2^2 - 2*x2^7*y1^2*y2^2 - 12*x1^5*x2*x3*y1^2*y2^2
+ 18*x1^4*x2^2*x3*y1^2*y2^2 - 28*x1^3*x2^3*x3*y1^2*y2^2 -
10*x1^2*x2^4*x3*y1^2*y2^2 + 20*x1*x2^5*x3*y1^2*y2^2 +
12*x2^6*x3*y1^2*y2^2 + 6*x1^5*x3^2*y1^2*y2^2 -
18*x1^4*x2*x3^2*y1^2*y2^2 + 36*x1^3*x2^2*x3^2*y1^2*y2^2 -
4*x1^2*x2^3*x3^2*y1^2*y2^2 - 4*x1*x2^4*x3^2*y1^2*y2^2 -
16*x2^5*x3^2*y1^2*y2^2 + 6*x1^4*x3^3*y1^2*y2^2 -
4*x1^3*x2*x3^3*y1^2*y2^2 + 4*x1^2*x2^2*x3^3*y1^2*y2^2 +
4*x1*x2^3*x3^3*y1^2*y2^2 - 10*x2^4*x3^3*y1^2*y2^2 -
8*x1^3*x3^4*y1^2*y2^2 + 4*x1^2*x2*x3^4*y1^2*y2^2 -
20*x1*x2^2*x3^4*y1^2*y2^2 + 24*x2^3*x3^4*y1^2*y2^2 -
2*x1^2*x3^5*y1^2*y2^2 + 4*x1*x2*x3^5*y1^2*y2^2 -
2*x2^2*x3^5*y1^2*y2^2 + 6*x1*x3^6*y1^2*y2^2 - 6*x2*x3^6*y1^2*y2^2
- 3*x1^2*x2^2*y1^4*y2^2 + 2*x1*x2^3*y1^4*y2^2 - 10*x2^4*y1^4*y2^2
+ 6*x1^2*x2*x3*y1^4*y2^2 - 6*x1*x2^2*x3*y1^4*y2^2 +
26*x2^3*x3*y1^4*y2^2 - 3*x1^2*x3^2*y1^4*y2^2 +
6*x1*x2*x3^2*y1^4*y2^2 - 15*x2^2*x3^2*y1^4*y2^2 -
2*x1*x3^3*y1^4*y2^2 - 8*x2*x3^3*y1^4*y2^2 + 7*x3^4*y1^4*y2^2 -
2*x1^6*x2*y1*y2^3 - 4*x1^5*x2^2*y1*y2^3 + 14*x1^4*x2^3*y1*y2^3 -
6*x1^3*x2^4*y1*y2^3 - 12*x1^2*x2^5*y1*y2^3 + 10*x1*x2^6*y1*y2^3 +
2*x1^6*x3*y1*y2^3 + 8*x1^5*x2*x3*y1*y2^3 -
22*x1^4*x2^2*x3*y1*y2^3 + 16*x1^3*x2^3*x3*y1*y2^3 +
6*x1^2*x2^4*x3*y1*y2^3 - 10*x2^6*x3*y1*y2^3 - 4*x1^5*x3^2*y1*y2^3
+ 14*x1^4*x2*x3^2*y1*y2^3 - 16*x1^3*x2^2*x3^2*y1*y2^3 -
6*x1*x2^4*x3^2*y1*y2^3 + 12*x2^5*x3^2*y1*y2^3 -
6*x1^4*x3^3*y1*y2^3 + 16*x1^2*x2^2*x3^3*y1*y2^3 -
16*x1*x2^3*x3^3*y1*y2^3 + 6*x2^4*x3^3*y1*y2^3 +
6*x1^3*x3^4*y1*y2^3 - 14*x1^2*x2*x3^4*y1*y2^3 +
22*x1*x2^2*x3^4*y1*y2^3 - 14*x2^3*x3^4*y1*y2^3 +
4*x1^2*x3^5*y1*y2^3 - 8*x1*x2*x3^5*y1*y2^3 + 4*x2^2*x3^5*y1*y2^3
- 2*x1*x3^6*y1*y2^3 + 2*x2*x3^6*y1*y2^3 + 4*x1^3*x2*y1^3*y2^3 +
4*x1^2*x2^2*y1^3*y2^3 - 12*x1*x2^3*y1^3*y2^3 + 8*x2^4*y1^3*y2^3 -
4*x1^3*x3*y1^3*y2^3 - 8*x1^2*x2*x3*y1^3*y2^3 +
16*x1*x2^2*x3*y1^3*y2^3 - 8*x2^3*x3*y1^3*y2^3 +
4*x1^2*x3^2*y1^3*y2^3 - 8*x1*x2*x3^2*y1^3*y2^3 -
8*x2^2*x3^2*y1^3*y2^3 + 4*x1*x3^3*y1^3*y2^3 +
16*x2*x3^3*y1^3*y2^3 - 8*x3^4*y1^3*y2^3 - 2*x2*y1^5*y2^3 +
2*x3*y1^5*y2^3 - 6*x1^3*x2*y1^2*y2^4 + x1^2*x2^2*y1^2*y2^4 +
16*x1*x2^3*y1^2*y2^4 - 2*x2^4*y1^2*y2^4 + 6*x1^3*x3*y1^2*y2^4 -
2*x1^2*x2*x3*y1^2*y2^4 - 14*x1*x2^2*x3*y1^2*y2^4 -
14*x2^3*x3*y1^2*y2^4 + x1^2*x3^2*y1^2*y2^4 -
2*x1*x2*x3^2*y1^2*y2^4 + 19*x2^2*x3^2*y1^2*y2^4 -
3*x3^4*y1^2*y2^4 + 6*x2*y1^4*y2^4 - 6*x3*y1^4*y2^4 -
2*x1^4*y1*y2^5 + 2*x1^3*x2*y1*y2^5 + 4*x1^2*x2^2*y1*y2^5 -
14*x1*x2^3*y1*y2^5 + 4*x1^2*x2*x3*y1*y2^5 + 4*x1*x2^2*x3*y1*y2^5
+ 14*x2^3*x3*y1*y2^5 - 2*x1^2*x3^2*y1*y2^5 + 4*x1*x2*x3^2*y1*y2^5
- 8*x2^2*x3^2*y1*y2^5 - 4*x1*x3^3*y1*y2^5 - 10*x2*x3^3*y1*y2^5 +
8*x3^4*y1*y2^5 + 2*x1*y1^3*y2^5 - 6*x2*y1^3*y2^5 + 4*x3*y1^3*y2^5
+ 3*x1^4*y2^6 - 4*x1^3*x2*y2^6 + 4*x1*x2^3*y2^6 - 2*x1^3*x3*y2^6
- 4*x2^3*x3*y2^6 + 2*x1*x3^3*y2^6 + 4*x2*x3^3*y2^6 - 3*x3^4*y2^6
- 6*x1*y1^2*y2^6 + 2*x2*y1^2*y2^6 + 4*x3*y1^2*y2^6 + 6*x1*y1*y2^7
- 6*x3*y1*y2^7 - 2*x1*y2^8 + 2*x3*y2^8 - 6*x1^6*x2^4*y1*y3 +
6*x1^5*x2^5*y1*y3 + 12*x1^4*x2^6*y1*y3 - 12*x1^3*x2^7*y1*y3 -
6*x1^2*x2^ 8*y1*y3 + 6*x1*x2^9*y1*y3 + 18*x1^6*x2^3*x3*y1*y3 -
24*x1^5*x2^4*x3*y1*y3 - 18*x1^4*x2^5*x3*y1*y3 +
24*x1^3*x2^6*x3*y1*y3 + 6*x1^2*x2^7*x3*y1*y3 - 6*x2^9*x3*y1*y3 -
18*x1^6*x2^2*x3^2*y1*y3 + 36*x1^5*x2^3*x3^2*y1*y3 -
12*x1^4*x2^4*x3^2*y1*y3 - 6*x1^3*x2^5*x3^2*y1*y3 -
6*x1*x2^7*x3^2*y1*y3 + 6*x2^ 8*x3^2*y1*y3 + 6*x1^6*x2*x3^3*y1*y3 -
24*x1^5*x2^2*x3^3*y1*y3 + 24*x1^4*x2^3*x3^3*y1*y3 +
6*x1^2*x2^5*x3^3*y1*y3 - 24*x1*x2^6*x3^3*y1*y3 +
12*x2^7*x3^3*y1*y3 + 6*x1^5*x2*x3^4*y1*y3 -
24*x1^3*x2^3*x3^4*y1*y3 + 12*x1^2*x2^4*x3^4*y1*y3 +
18*x1*x2^5*x3^4*y1*y3 - 12*x2^6*x3^4*y1*y3 - 6*x1^4*x2*x3^5*y1*y3
+ 24*x1^3*x2^2*x3^5*y1*y3 - 36*x1^2*x2^3*x3^5*y1*y3 +
24*x1*x2^4*x3^5*y1*y3 - 6*x2^5*x3^5*y1*y3 - 6*x1^3*x2*x3^6*y1*y3
+ 18*x1^2*x2^2*x3^6*y1*y3 - 18*x1*x2^3*x3^6*y1*y3 +
6*x2^4*x3^6*y1*y3 + 10*x1^3*x2^4*y1^3*y3 - 6*x1^2*x2^5*y1^3*y3 -
10*x1*x2^6*y1^3*y3 + 6*x2^7*y1^3*y3 - 28*x1^3*x2^3*x3*y1^3*y3 +
24*x1^2*x2^4*x3*y1^3*y3 + 12*x1*x2^5*x3*y1^3*y3 -
8*x2^6*x3*y1^3*y3 + 24*x1^3*x2^2*x3^2*y1^3*y3 -
36*x1^2*x2^3*x3^2*y1^3*y3 + 18*x1*x2^4*x3^2*y1^3*y3 -
6*x2^5*x3^2*y1^3*y3 - 4*x1^3*x2*x3^3*y1^3*y3 +
24*x1^2*x2^2*x3^3*y1^3*y3 - 28*x1*x2^3*x3^3*y1^3*y3 +
8*x2^4*x3^3*y1^3*y3 - 2*x1^3*x3^4*y1^3*y3 -
6*x1^2*x2*x3^4*y1^3*y3 + 6*x1*x2^2*x3^4*y1^3*y3 +
2*x2^3*x3^4*y1^3*y3 + 2*x1*x3^6*y1^3*y3 - 2*x2*x3^6*y1^3*y3 -
4*x2^4*y1^5*y3 + 10*x2^3*x3*y1^5*y3 - 6*x2^2*x3^2*y1^5*y3 -
2*x2*x3^3*y1^5*y3 + 2*x3^4*y1^5*y3 + 6*x1^ 8*x2^2*y2*y3 -
8*x1^7*x2^3*y2*y3 - 8*x1^6*x2^4*y2*y3 + 14*x1^5*x2^5*y2*y3 -
2*x1^4*x2^6*y2*y3 - 4*x1^3*x2^7*y2*y3 + 4*x1^2*x2^ 8*y2*y3 -
2*x1*x2^9*y2*y3 - 12*x1^ 8*x2*x3*y2*y3 + 24*x1^7*x2^2*x3*y2*y3 -
14*x1^6*x2^3*x3*y2*y3 - 4*x1^5*x2^4*x3*y2*y3 +
26*x1^4*x2^5*x3*y2*y3 - 24*x1^3*x2^6*x3*y2*y3 -
2*x1^2*x2^7*x3*y2*y3 + 4*x1*x2^ 8*x3*y2*y3 + 2*x2^9*x3*y2*y3 +
6*x1^ 8*x3^2*y2*y3 - 24*x1^7*x2*x3^2*y2*y3 +
48*x1^6*x2^2*x3^2*y2*y3 - 40*x1^5*x2^3*x3^2*y2*y3 -
4*x1^4*x2^4*x3^2*y2*y3 + 14*x1^3*x2^5*x3^2*y2*y3 -
2*x1^2*x2^6*x3^2*y2*y3 + 10*x1*x2^7*x3^2*y2*y3 -
8*x2^ 8*x3^2*y2*y3 + 8*x1^7*x3^3*y2*y3 - 22*x1^6*x2*x3^3*y2*y3 +
28*x1^5*x2^2*x3^3*y2*y3 - 32*x1^4*x2^3*x3^3*y2*y3 +
32*x1^3*x2^4*x3^3*y2*y3 - 22*x1^2*x2^5*x3^3*y2*y3 +
12*x1*x2^6*x3^3*y2*y3 - 4*x2^7*x3^3*y2*y3 - 4*x1^6*x3^4*y2*y3 +
10*x1^5*x2*x3^4*y2*y3 - 20*x1^4*x2^2*x3^4*y2*y3 +
24*x1^3*x2^3*x3^4*y2*y3 + 8*x1^2*x2^4*x3^4*y2*y3 -
34*x1*x2^5*x3^4*y2*y3 + 16*x2^6*x3^4*y2*y3 - 8*x1^5*x3^5*y2*y3 +
34*x1^4*x2*x3^5*y2*y3 - 56*x1^3*x2^2*x3^5*y2*y3 +
44*x1^2*x2^3*x3^5*y2*y3 - 16*x1*x2^4*x3^5*y2*y3 +
2*x2^5*x3^5*y2*y3 - 2*x1^4*x3^6*y2*y3 + 14*x1^3*x2*x3^6*y2*y3 -
30*x1^2*x2^2*x3^6*y2*y3 + 26*x1*x2^3*x3^6*y2*y3 -
8*x2^4*x3^6*y2*y3 - 12*x1^5*x2^2*y1^2*y2*y3 +
12*x1^4*x2^3*y1^2*y2*y3 - 2*x1^3*x2^4*y1^2*y2*y3 -
10*x1^2*x2^5*y1^2*y2*y3 + 14*x1*x2^6*y1^2*y2*y3 -
2*x2^7*y1^2*y2*y3 + 24*x1^5*x2*x3*y1^2*y2*y3 -
36*x1^4*x2^2*x3*y1^2*y2*y3 + 44*x1^3*x2^3*x3*y1^2*y2*y3 -
4*x1^2*x2^4*x3*y1^2*y2*y3 - 28*x1*x2^5*x3*y1^2*y2*y3 -
12*x1^5*x3^2*y1^2*y2*y3 + 36*x1^4*x2*x3^2*y1^2*y2*y3 -
72*x1^3*x2^2*x3^2*y1^2*y2*y3 + 44*x1^2*x2^3*x3^2*y1^2*y2*y3 -
10*x1*x2^4*x3^2*y1^2*y2*y3 + 14*x2^5*x3^2*y1^2*y2*y3 -
12*x1^4*x3^3*y1^2*y2*y3 + 20*x1^3*x2*x3^3*y1^2*y2*y3 -
32*x1^2*x2^2*x3^3*y1^2*y2*y3 + 28*x1*x2^3*x3^3*y1^2*y2*y3 -
4*x2^4*x3^3*y1^2*y2*y3 + 10*x1^3*x3^4*y1^2*y2*y3 -
2*x1^2*x2*x3^4*y1^2*y2*y3 + 10*x1*x2^2*x3^4*y1^2*y2*y3 -
18*x2^3*x3^4*y1^2*y2*y3 + 4*x1^2*x3^5*y1^2*y2*y3 -
8*x1*x2*x3^5*y1^2*y2*y3 + 4*x2^2*x3^5*y1^2*y2*y3 -
6*x1*x3^6*y1^2*y2*y3 + 6*x2*x3^6*y1^2*y2*y3 +
6*x1^2*x2^2*y1^4*y2*y3 - 4*x1*x2^3*y1^4*y2*y3 +
10*x2^4*y1^4*y2*y3 - 12*x1^2*x2*x3*y1^4*y2*y3 +
12*x1*x2^2*x3*y1^4*y2*y3 - 30*x2^3*x3*y1^4*y2*y3 +
6*x1^2*x3^2*y1^4*y2*y3 - 12*x1*x2*x3^2*y1^4*y2*y3 +
24*x2^2*x3^2*y1^4*y2*y3 + 4*x1*x3^3*y1^4*y2*y3 +
2*x2*x3^3*y1^4*y2*y3 - 6*x3^4*y1^4*y2*y3 + 6*x1^6*x2*y1*y2^2*y3 +
8*x1^5*x2^2*y1*y2^2*y3 - 30*x1^4*x2^3*y1*y2^2*y3 +
14*x1^3*x2^4*y1*y2^2*y3 + 24*x1^2*x2^5*y1*y2^2*y3 -
22*x1*x2^6*y1*y2^2*y3 - 6*x1^6*x3*y1*y2^2*y3 -
16*x1^5*x2*x3*y1*y2^2*y3 + 38*x1^4*x2^2*x3*y1*y2^2*y3 -
32*x1^3*x2^3*x3*y1*y2^2*y3 - 6*x1^2*x2^4*x3*y1*y2^2*y3 +
22*x2^6*x3*y1*y2^2*y3 + 8*x1^5*x3^2*y1*y2^2*y3 -
22*x1^4*x2*x3^2*y1*y2^2*y3 + 32*x1^3*x2^2*x3^2*y1*y2^2*y3 +
6*x1*x2^4*x3^2*y1*y2^2*y3 - 24*x2^5*x3^2*y1*y2^2*y3 +
14*x1^4*x3^3*y1*y2^2*y3 - 32*x1^2*x2^2*x3^3*y1*y2^2*y3 +
32*x1*x2^3*x3^3*y1*y2^2*y3 - 14*x2^4*x3^3*y1*y2^2*y3 -
14*x1^3*x3^4*y1*y2^2*y3 + 22*x1^2*x2*x3^4*y1*y2^2*y3 -
38*x1*x2^2*x3^4*y1*y2^2*y3 + 30*x2^3*x3^4*y1*y2^2*y3 -
8*x1^2*x3^5*y1*y2^2*y3 + 16*x1*x2*x3^5*y1*y2^2*y3 -
8*x2^2*x3^5*y1*y2^2*y3 + 6*x1*x3^6*y1*y2^2*y3 -
6*x2*x3^6*y1*y2^2*y3 - 12*x1^3*x2*y1^3*y2^2*y3 -
8*x1^2*x2^2*y1^3*y2^2*y3 + 28*x1*x2^3*y1^3*y2^2*y3 -
16*x2^4*y1^3*y2^2*y3 + 12*x1^3*x3*y1^3*y2^2*y3 +
16*x1^2*x2*x3*y1^3*y2^2*y3 - 32*x1*x2^2*x3*y1^3*y2^2*y3 +
24*x2^3*x3*y1^3*y2^2*y3 - 8*x1^2*x3^2*y1^3*y2^2*y3 +
16*x1*x2*x3^2*y1^3*y2^2*y3 - 20*x2^2*x3^2*y1^3*y2^2*y3 -
12*x1*x3^3*y1^3*y2^2*y3 + 8*x2*x3^3*y1^3*y2^2*y3 +
4*x3^4*y1^3*y2^2*y3 + 6*x2*y1^5*y2^2*y3 - 6*x3*y1^5*y2^2*y3 -
2*x1^6*x2*y2^3*y3 - 4*x1^5*x2^2*y2^3*y3 + 14*x1^4*x2^3*y2^3*y3 -
6*x1^3*x2^4*y2^3*y3 - 12*x1^2*x2^5*y2^3*y3 + 10*x1*x2^6*y2^3*y3 +
2*x1^6*x3*y2^3*y3 + 8*x1^5*x2*x3*y2^3*y3 -
22*x1^4*x2^2*x3*y2^3*y3 + 16*x1^3*x2^3*x3*y2^3*y3 +
6*x1^2*x2^4*x3*y2^3*y3 - 10*x2^6*x3*y2^3*y3 - 4*x1^5*x3^2*y2^3*y3
+ 14*x1^4*x2*x3^2*y2^3*y3 - 16*x1^3*x2^2*x3^2*y2^3*y3 -
6*x1*x2^4*x3^2*y2^3*y3 + 12*x2^5*x3^2*y2^3*y3 -
6*x1^4*x3^3*y2^3*y3 + 16*x1^2*x2^2*x3^3*y2^3*y3 -
16*x1*x2^3*x3^3*y2^3*y3 + 6*x2^4*x3^3*y2^3*y3 +
6*x1^3*x3^4*y2^3*y3 - 14*x1^2*x2*x3^4*y2^3*y3 +
22*x1*x2^2*x3^4*y2^3*y3 - 14*x2^3*x3^4*y2^3*y3 +
4*x1^2*x3^5*y2^3*y3 - 8*x1*x2*x3^5*y2^3*y3 + 4*x2^2*x3^5*y2^3*y3
- 2*x1*x3^6*y2^3*y3 + 2*x2*x3^6*y2^3*y3 + 20*x1^3*x2*y1^2*y2^3*y3
- 36*x1*x2^3*y1^2*y2^3*y3 + 8*x2^4*y1^2*y2^3*y3 -
20*x1^3*x3*y1^2*y2^3*y3 + 24*x1*x2^2*x3*y1^2*y2^3*y3 +
16*x2^3*x3*y1^2*y2^3*y3 - 12*x2^2*x3^2*y1^2*y2^3*y3 +
12*x1*x3^3*y1^2*y2^3*y3 - 16*x2*x3^3*y1^2*y2^3*y3 +
4*x3^4*y1^2*y2^3*y3 - 18*x2*y1^4*y2^3*y3 + 18*x3*y1^4*y2^3*y3 +
6*x1^4*y1*y2^4*y3 - 10*x1^3*x2*y1*y2^4*y3 -
18*x1^2*x2^2*y1*y2^4*y3 + 34*x1*x2^3*y1*y2^4*y3 +
4*x1^3*x3*y1*y2^4*y3 - 34*x2^3*x3*y1*y2^4*y3 +
18*x2^2*x3^2*y1*y2^4*y3 - 4*x1*x3^3*y1*y2^4*y3 +
10*x2*x3^3*y1*y2^4*y3 - 6*x3^4*y1*y2^4*y3 - 6*x1*y1^3*y2^4*y3 +
18*x2*y1^3*y2^4*y3 - 12*x3*y1^3*y2^4*y3 - 8*x1^4*y2^5*y3 +
10*x1^3*x2*y2^5*y3 + 8*x1^2*x2^2*y2^5*y3 - 14*x1*x2^3*y2^5*y3 +
4*x1^3*x3*y2^5*y3 - 4*x1^2*x2*x3*y2^5*y3 - 4*x1*x2^2*x3*y2^5*y3 +
14*x2^3*x3*y2^5*y3 + 2*x1^2*x3^2*y2^5*y3 - 4*x1*x2*x3^2*y2^5*y3 -
4*x2^2*x3^2*y2^5*y3 - 2*x2*x3^3*y2^5*y3 + 2*x3^4*y2^5*y3 +
18*x1*y1^2*y2^5*y3 - 6*x2*y1^2*y2^5*y3 - 12*x3*y1^2*y2^5*y3 -
18*x1*y1*y2^6*y3 + 18*x3*y1*y2^6*y3 + 6*x1*y2^7*y3 - 6*x3*y2^7*y3
- 3*x1^ 8*x2^2*y3^2 + 4*x1^7*x2^3*y3^2 + 5*x1^6*x2^4*y3^2 -
6*x1^5*x2^5*y3^2 - 3*x1^4*x2^6*y3^2 + 3*x1^2*x2^ 8*y3^2 +
2*x1*x2^9*y3^2 - 2*x2^10*y3^2 + 6*x1^ 8*x2*x3*y3^2 -
12*x1^7*x2^2*x3*y3^2 + 6*x1^5*x2^4*x3*y3^2 + 6*x1^4*x2^5*x3*y3^2
- 12*x1^2*x2^7*x3*y3^2 + 6*x1*x2^ 8*x3*y3^2 - 3*x1^ 8*x3^2*y3^2 +
12*x1^7*x2*x3^2*y3^2 - 9*x1^6*x2^2*x3^2*y3^2 -
6*x1^5*x2^3*x3^2*y3^2 - 12*x1^4*x2^4*x3^2*y3^2 +
36*x1^3*x2^5*x3^2*y3^2 - 9*x1^2*x2^6*x3^2*y3^2 -
18*x1*x2^7*x3^2*y3^2 + 9*x2^ 8*x3^2*y3^2 - 4*x1^7*x3^3*y3^2 -
2*x1^6*x2*x3^3*y3^2 + 30*x1^5*x2^2*x3^3*y3^2 -
20*x1^4*x2^3*x3^3*y3^2 - 40*x1^3*x2^4*x3^3*y3^2 +
54*x1^2*x2^5*x3^3*y3^2 - 18*x1*x2^6*x3^3*y3^2 + 6*x1^6*x3^4*y3^2
- 36*x1^5*x2*x3^4*y3^2 + 72*x1^4*x2^2*x3^4*y3^2 -
48*x1^3*x2^3*x3^4*y3^2 - 18*x1^2*x2^4*x3^4*y3^2 +
36*x1*x2^5*x3^4*y3^2 - 12*x2^6*x3^4*y3^2 + 12*x1^5*x3^5*y3^2 -
48*x1^4*x2*x3^5*y3^2 + 72*x1^3*x2^2*x3^5*y3^2 -
48*x1^2*x2^3*x3^5*y3^2 + 12*x1*x2^4*x3^5*y3^2 + 5*x1^4*x3^6*y3^2
- 20*x1^3*x2*x3^6*y3^2 + 30*x1^2*x2^2*x3^6*y3^2 -
20*x1*x2^3*x3^6*y3^2 + 5*x2^4*x3^6*y3^2 + 6*x1^5*x2^2*y1^2*y3^2 -
6*x1^4*x2^3*y1^2*y3^2 - 6*x1^3*x2^4*y1^2*y3^2 +
6*x1^2*x2^5*y1^2*y3^2 - 12*x1^5*x2*x3*y1^2*y3^2 +
18*x1^4*x2^2*x3*y1^2*y3^2 - 6*x1^2*x2^4*x3*y1^2*y3^2 +
6*x1^5*x3^2*y1^2*y3^2 - 18*x1^4*x2*x3^2*y1^2*y3^2 +
12*x1^3*x2^2*x3^2*y1^2*y3^2 + 6*x1*x2^4*x3^2*y1^2*y3^2 -
6*x2^5*x3^2*y1^2*y3^2 + 6*x1^4*x3^3*y1^2*y3^2 -
12*x1^2*x2^2*x3^3*y1^2*y3^2 + 6*x2^4*x3^3*y1^2*y3^2 -
6*x1^3*x3^4*y1^2*y3^2 + 18*x1^2*x2*x3^4*y1^2*y3^2 -
18*x1*x2^2*x3^4*y1^2*y3^2 + 6*x2^3*x3^4*y1^2*y3^2 -
6*x1^2*x3^5*y1^2*y3^2 + 12*x1*x2*x3^5*y1^2*y3^2 -
6*x2^2*x3^5*y1^2*y3^2 - 3*x1^2*x2^2*y1^4*y3^2 +
2*x1*x2^3*y1^4*y3^2 + x2^4*y1^4*y3^2 + 6*x1^2*x2*x3*y1^4*y3^2 -
6*x1*x2^2*x3*y1^4*y3^2 - 3*x1^2*x3^2*y1^4*y3^2 +
6*x1*x2*x3^2*y1^4*y3^2 - 3*x2^2*x3^2*y1^4*y3^2 -
2*x1*x3^3*y1^4*y3^2 + 2*x2*x3^3*y1^4*y3^2 - 6*x1^6*x2*y1*y2*y3^2
- 4*x1^5*x2^2*y1*y2*y3^2 + 18*x1^4*x2^3*y1*y2*y3^2 +
4*x1^3*x2^4*y1*y2*y3^2 - 14*x1^2*x2^5*y1*y2*y3^2 +
2*x2^7*y1*y2*y3^2 + 6*x1^6*x3*y1*y2*y3^2 +
8*x1^5*x2*x3*y1*y2*y3^2 - 10*x1^4*x2^2*x3*y1*y2*y3^2 -
28*x1^3*x2^3*x3*y1*y2*y3^2 + 10*x1^2*x2^4*x3*y1*y2*y3^2 +
28*x1*x2^5*x3*y1*y2*y3^2 - 14*x2^6*x3*y1*y2*y3^2 -
4*x1^5*x3^2*y1*y2*y3^2 + 2*x1^4*x2*x3^2*y1*y2*y3^2 +
32*x1^3*x2^2*x3^2*y1*y2*y3^2 - 44*x1^2*x2^3*x3^2*y1*y2*y3^2 +
4*x1*x2^4*x3^2*y1*y2*y3^2 + 10*x2^5*x3^2*y1*y2*y3^2 -
10*x1^4*x3^3*y1*y2*y3^2 - 20*x1^3*x2*x3^3*y1*y2*y3^2 +
72*x1^2*x2^2*x3^3*y1*y2*y3^2 - 44*x1*x2^3*x3^3*y1*y2*y3^2 +
2*x2^4*x3^3*y1*y2*y3^2 + 12*x1^3*x3^4*y1*y2*y3^2 -
36*x1^2*x2*x3^4*y1*y2*y3^2 + 36*x1*x2^2*x3^4*y1*y2*y3^2 -
12*x2^3*x3^4*y1*y2*y3^2 + 12*x1^2*x3^5*y1*y2*y3^2 -
24*x1*x2*x3^5*y1*y2*y3^2 + 12*x2^2*x3^5*y1*y2*y3^2 +
12*x1^3*x2*y1^3*y2*y3^2 + 4*x1^2*x2^2*y1^3*y2*y3^2 -
20*x1*x2^3*y1^3*y2*y3^2 + 4*x2^4*y1^3*y2*y3^2 -
12*x1^3*x3*y1^3*y2*y3^2 - 8*x1^2*x2*x3*y1^3*y2*y3^2 +
16*x1*x2^2*x3*y1^3*y2*y3^2 + 4*x2^3*x3*y1^3*y2*y3^2 +
4*x1^2*x3^2*y1^3*y2*y3^2 - 8*x1*x2*x3^2*y1^3*y2*y3^2 +
4*x2^2*x3^2*y1^3*y2*y3^2 + 12*x1*x3^3*y1^3*y2*y3^2 -
12*x2*x3^3*y1^3*y2*y3^2 - 6*x2*y1^5*y2*y3^2 + 6*x3*y1^5*y2*y3^2 +
6*x1^6*x2*y2^2*y3^2 + 2*x1^5*x2^2*y2^2*y3^2 -
24*x1^4*x2^3*y2^2*y3^2 + 10*x1^3*x2^4*y2^2*y3^2 +
16*x1^2*x2^5*y2^2*y3^2 - 12*x1*x2^6*y2^2*y3^2 + 2*x2^7*y2^2*y3^2
- 6*x1^6*x3*y2^2*y3^2 - 4*x1^5*x2*x3*y2^2*y3^2 +
20*x1^4*x2^2*x3*y2^2*y3^2 - 4*x1^3*x2^3*x3*y2^2*y3^2 +
4*x1^2*x2^4*x3*y2^2*y3^2 - 20*x1*x2^5*x3*y2^2*y3^2 +
10*x2^6*x3*y2^2*y3^2 + 2*x1^5*x3^2*y2^2*y3^2 -
4*x1^4*x2*x3^2*y2^2*y3^2 - 4*x1^3*x2^2*x3^2*y2^2*y3^2 +
4*x1^2*x2^3*x3^2*y2^2*y3^2 + 10*x1*x2^4*x3^2*y2^2*y3^2 -
8*x2^5*x3^2*y2^2*y3^2 + 8*x1^4*x3^3*y2^2*y3^2 +
4*x1^3*x2*x3^3*y2^2*y3^2 - 36*x1^2*x2^2*x3^3*y2^2*y3^2 +
28*x1*x2^3*x3^3*y2^2*y3^2 - 4*x2^4*x3^3*y2^2*y3^2 -
6*x1^3*x3^4*y2^2*y3^2 + 18*x1^2*x2*x3^4*y2^2*y3^2 -
18*x1*x2^2*x3^4*y2^2*y3^2 + 6*x2^3*x3^4*y2^2*y3^2 -
6*x1^2*x3^5*y2^2*y3^2 + 12*x1*x2*x3^5*y2^2*y3^2 -
6*x2^2*x3^5*y2^2*y3^2 - 24*x1^3*x2*y1^2*y2^2*y3^2 +
24*x1*x2^3*y1^2*y2^2*y3^2 + 24*x1^3*x3*y1^2*y2^2*y3^2 -
24*x2^3*x3*y1^2*y2^2*y3^2 - 24*x1*x3^3*y1^2*y2^2*y3^2 +
24*x2*x3^3*y1^2*y2^2*y3^2 + 18*x2*y1^4*y2^2*y3^2 -
18*x3*y1^4*y2^2*y3^2 - 4*x1^4*y1*y2^3*y3^2 +
16*x1^3*x2*y1*y2^3*y3^2 + 12*x1^2*x2^2*y1*y2^3*y3^2 -
16*x1*x2^3*y1*y2^3*y3^2 - 8*x2^4*y1*y2^3*y3^2 -
12*x1^3*x3*y1*y2^3*y3^2 - 24*x1*x2^2*x3*y1*y2^3*y3^2 +
36*x2^3*x3*y1*y2^3*y3^2 + 20*x1*x3^3*y1*y2^3*y3^2 -
20*x2*x3^3*y1*y2^3*y3^2 + 4*x1*y1^3*y2^3*y3^2 -
16*x2*y1^3*y2^3*y3^2 + 12*x3*y1^3*y2^3*y3^2 + 3*x1^4*y2^4*y3^2 -
19*x1^2*x2^2*y2^4*y3^2 + 14*x1*x2^3*y2^4*y3^2 + 2*x2^4*y2^4*y3^2
+ 2*x1^2*x2*x3*y2^4*y3^2 + 14*x1*x2^2*x3*y2^4*y3^2 -
16*x2^3*x3*y2^4*y3^2 - x1^2*x3^2*y2^4*y3^2 +
2*x1*x2*x3^2*y2^4*y3^2 - x2^2*x3^2*y2^4*y3^2 -
6*x1*x3^3*y2^4*y3^2 + 6*x2*x3^3*y2^4*y3^2 - 12*x1*y1^2*y2^4*y3^2
+ 12*x3*y1^2*y2^4*y3^2 + 12*x1*y1*y2^5*y3^2 + 6*x2*y1*y2^5*y3^2 -
18*x3*y1*y2^5*y3^2 - 4*x1*y2^6*y3^2 - 2*x2*y2^6*y3^2 +
6*x3*y2^6*y3^2 + 2*x1^6*x2*y1*y3^3 - 2*x1^4*x2^3*y1*y3^3 -
8*x1^3*x2^4*y1*y3^3 + 6*x1^2*x2^5*y1*y3^3 + 8*x1*x2^6*y1*y3^3 -
6*x2^7*y1*y3^3 - 2*x1^6*x3*y1*y3^3 - 6*x1^4*x2^2*x3*y1*y3^3 +
28*x1^3*x2^3*x3*y1*y3^3 - 18*x1^2*x2^4*x3*y1*y3^3 -
12*x1*x2^5*x3*y1*y3^3 + 10*x2^6*x3*y1*y3^3 +
6*x1^4*x2*x3^2*y1*y3^3 - 24*x1^3*x2^2*x3^2*y1*y3^3 +
36*x1^2*x2^3*x3^2*y1*y3^3 - 24*x1*x2^4*x3^2*y1*y3^3 +
6*x2^5*x3^2*y1*y3^3 + 2*x1^4*x3^3*y1*y3^3 +
4*x1^3*x2*x3^3*y1*y3^3 - 24*x1^2*x2^2*x3^3*y1*y3^3 +
28*x1*x2^3*x3^3*y1*y3^3 - 10*x2^4*x3^3*y1*y3^3 -
4*x1^3*x2*y1^3*y3^3 + 4*x1*x2^3*y1^3*y3^3 + 4*x1^3*x3*y1^3*y3^3 -
4*x2^3*x3*y1^3*y3^3 - 4*x1*x3^3*y1^3*y3^3 + 4*x2*x3^3*y1^3*y3^3 +
2*x2*y1^5*y3^3 - 2*x3*y1^5*y3^3 - 6*x1^6*x2*y2*y3^3 +
8*x1^5*x2^2*y2*y3^3 + 6*x1^4*x2^3*y2*y3^3 - 8*x1^3*x2^4*y2*y3^3 -
2*x1^2*x2^5*y2*y3^3 + 2*x2^7*y2*y3^3 + 6*x1^6*x3*y2*y3^3 -
16*x1^5*x2*x3*y2*y3^3 + 26*x1^4*x2^2*x3*y2*y3^3 -
28*x1^3*x2^3*x3*y2*y3^3 - 2*x1^2*x2^4*x3*y2*y3^3 +
28*x1*x2^5*x3*y2*y3^3 - 14*x2^6*x3*y2*y3^3 + 8*x1^5*x3^2*y2*y3^3
- 34*x1^4*x2*x3^2*y2*y3^3 + 56*x1^3*x2^2*x3^2*y2*y3^3 -
44*x1^2*x2^3*x3^2*y2*y3^3 + 16*x1*x2^4*x3^2*y2*y3^3 -
2*x2^5*x3^2*y2*y3^3 + 2*x1^4*x3^3*y2*y3^3 -
20*x1^3*x2*x3^3*y2*y3^3 + 48*x1^2*x2^2*x3^3*y2*y3^3 -
44*x1*x2^3*x3^3*y2*y3^3 + 14*x2^4*x3^3*y2*y3^3 +
12*x1^3*x2*y1^2*y2*y3^3 - 4*x1^2*x2^2*y1^2*y2*y3^3 -
4*x1*x2^3*y1^2*y2*y3^3 - 4*x2^4*y1^2*y2*y3^3 -
12*x1^3*x3*y1^2*y2*y3^3 + 8*x1^2*x2*x3*y1^2*y2*y3^3 -
16*x1*x2^2*x3*y1^2*y2*y3^3 + 20*x2^3*x3*y1^2*y2*y3^3 -
4*x1^2*x3^2*y1^2*y2*y3^3 + 8*x1*x2*x3^2*y1^2*y2*y3^3 -
4*x2^2*x3^2*y1^2*y2*y3^3 + 12*x1*x3^3*y1^2*y2*y3^3 -
12*x2*x3^3*y1^2*y2*y3^3 - 6*x2*y1^4*y2*y3^3 + 6*x3*y1^4*y2*y3^3 -
4*x1^4*y1*y2^2*y3^3 - 8*x1^3*x2*y1*y2^2*y3^3 +
20*x1^2*x2^2*y1*y2^2*y3^3 - 24*x1*x2^3*y1*y2^2*y3^3 +
16*x2^4*y1*y2^2*y3^3 + 12*x1^3*x3*y1*y2^2*y3^3 -
16*x1^2*x2*x3*y1*y2^2*y3^3 + 32*x1*x2^2*x3*y1*y2^2*y3^3 -
28*x2^3*x3*y1*y2^2*y3^3 + 8*x1^2*x3^2*y1*y2^2*y3^3 -
16*x1*x2*x3^2*y1*y2^2*y3^3 + 8*x2^2*x3^2*y1*y2^2*y3^3 -
12*x1*x3^3*y1*y2^2*y3^3 + 12*x2*x3^3*y1*y2^2*y3^3 +
4*x1*y1^3*y2^2*y3^3 - 4*x3*y1^3*y2^2*y3^3 + 8*x1^4*y2^3*y3^3 -
16*x1^3*x2*y2^3*y3^3 + 8*x1^2*x2^2*y2^3*y3^3 +
8*x1*x2^3*y2^3*y3^3 - 8*x2^4*y2^3*y3^3 - 4*x1^3*x3*y2^3*y3^3 +
8*x1^2*x2*x3*y2^3*y3^3 - 16*x1*x2^2*x3*y2^3*y3^3 +
12*x2^3*x3*y2^3*y3^3 - 4*x1^2*x3^2*y2^3*y3^3 +
8*x1*x2*x3^2*y2^3*y3^3 - 4*x2^2*x3^2*y2^3*y3^3 +
4*x1*x3^3*y2^3*y3^3 - 4*x2*x3^3*y2^3*y3^3 - 12*x1*y1^2*y2^3*y3^3
+ 16*x2*y1^2*y2^3*y3^3 - 4*x3*y1^2*y2^3*y3^3 + 12*x1*y1*y2^4*y3^3
- 18*x2*y1*y2^4*y3^3 + 6*x3*y1*y2^4*y3^3 - 4*x1*y2^5*y3^3 +
6*x2*y2^5*y3^3 - 2*x3*y2^5*y3^3 + 2*x1^6*x2*y3^4 -
6*x1^5*x2^2*y3^4 + 4*x1^4*x2^3*y3^4 + 4*x1^3*x2^4*y3^4 -
6*x1^2*x2^5*y3^4 + 2*x1*x2^6*y3^4 - 2*x1^6*x3*y3^4 +
12*x1^5*x2*x3*y3^4 - 24*x1^4*x2^2*x3*y3^4 + 16*x1^3*x2^3*x3*y3^4
+ 6*x1^2*x2^4*x3*y3^4 - 12*x1*x2^5*x3*y3^4 + 4*x2^6*x3*y3^4 -
6*x1^5*x3^2*y3^4 + 24*x1^4*x2*x3^2*y3^4 - 36*x1^3*x2^2*x3^2*y3^4
+ 24*x1^2*x2^3*x3^2*y3^4 - 6*x1*x2^4*x3^2*y3^4 - 4*x1^4*x3^3*y3^4
+ 16*x1^3*x2*x3^3*y3^4 - 24*x1^2*x2^2*x3^3*y3^4 +
16*x1*x2^3*x3^3*y3^4 - 4*x2^4*x3^3*y3^4 - 2*x1^3*x2*y1^2*y3^4 +
3*x1^2*x2^2*y1^2*y3^4 - x2^4*y1^2*y3^4 + 2*x1^3*x3*y1^2*y3^4 -
6*x1^2*x2*x3*y1^2*y3^4 + 6*x1*x2^2*x3*y1^2*y3^4 -
2*x2^3*x3*y1^2*y3^4 + 3*x1^2*x3^2*y1^2*y3^4 -
6*x1*x2*x3^2*y1^2*y3^4 + 3*x2^2*x3^2*y1^2*y3^4 +
6*x1^4*y1*y2*y3^4 - 2*x1^3*x2*y1*y2*y3^4 -
24*x1^2*x2^2*y1*y2*y3^4 + 30*x1*x2^3*y1*y2*y3^4 -
10*x2^4*y1*y2*y3^4 - 4*x1^3*x3*y1*y2*y3^4 +
12*x1^2*x2*x3*y1*y2*y3^4 - 12*x1*x2^2*x3*y1*y2*y3^4 +
4*x2^3*x3*y1*y2*y3^4 - 6*x1^2*x3^2*y1*y2*y3^4 +
12*x1*x2*x3^2*y1*y2*y3^4 - 6*x2^2*x3^2*y1*y2*y3^4 -
6*x1*y1^3*y2*y3^4 + 6*x2*y1^3*y2*y3^4 - 7*x1^4*y2^2*y3^4 +
8*x1^3*x2*y2^2*y3^4 + 15*x1^2*x2^2*y2^2*y3^4 -
26*x1*x2^3*y2^2*y3^4 + 10*x2^4*y2^2*y3^4 + 2*x1^3*x3*y2^2*y3^4 -
6*x1^2*x2*x3*y2^2*y3^4 + 6*x1*x2^2*x3*y2^2*y3^4 -
2*x2^3*x3*y2^2*y3^4 + 3*x1^2*x3^2*y2^2*y3^4 -
6*x1*x2*x3^2*y2^2*y3^4 + 3*x2^2*x3^2*y2^2*y3^4 +
18*x1*y1^2*y2^2*y3^4 - 18*x2*y1^2*y2^2*y3^4 - 18*x1*y1*y2^3*y3^4
+ 18*x2*y1*y2^3*y3^4 + 6*x1*y2^4*y3^4 - 6*x2*y2^4*y3^4 -
2*x1^4*y1*y3^5 + 2*x1^3*x2*y1*y3^5 + 6*x1^2*x2^2*y1*y3^5 -
10*x1*x2^3*y1*y3^5 + 4*x2^4*y1*y3^5 + 2*x1*y1^3*y3^5 -
2*x2*y1^3*y3^5 + 6*x1^3*x2*y2*y3^5 - 18*x1^2*x2^2*y2*y3^5 +
18*x1*x2^3*y2*y3^5 - 6*x2^4*y2*y3^5 - 6*x1*y1^2*y2*y3^5 +
6*x2*y1^2*y2*y3^5 + 6*x1*y1*y2^2*y3^5 - 6*x2*y1*y2^2*y3^5 -
2*x1*y2^3*y3^5 + 2*x2*y2^3*y3^5 + x1^4*y3^6 - 4*x1^3*x2*y3^6 +
6*x1^2*x2^2*y3^6 - 4*x1*x2^3*y3^6 + x2^4*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.
Time ring. (* 6.881 secs *)
Time Qed.
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.
Time ring. (* 6.805 secs *)
Time Qed.
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.
Time ring. (* 6.303 secs *)
Time Qed.