|
(* Test parsing/interpretation/pretyping on a large example *)
(* Expected time < 1.50s *)
Require Import Reals.
Require Import Ring_tac.
Open Scope R_scope.
Timeout 5 Time Goal forall x1 x2 x3 y1 y2 y3 e1 e2 e3 e4 e5 e6 e7: R,
(e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1) *
((- (y1 - y2) * (e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x1) -
e2 * y1 - e2 * y3) *
((- (y1 - y2) * (e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x1) -
e2 * y1 - e2 * y3) * 1)) * e3 -
(e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) * 1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1)) *
(e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1) * e3 -
(e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) * 1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1)) * x3 * e1 * e3 -
(- (y2 - y3) * (e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x2) -
e4 * y2 - e4 * y1) *
((- (y2 - y3) * (e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x2) -
e4 * y2 - e4 * y1) * 1) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) * 1)) * e1 +
(e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) * 1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1)) *
(e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3) * e1 +
(e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) *
((e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x3) * 1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1)) * x1 * e1 * e3 =
3 * e1 * e6 ^ 4 * e7 + e1 * e6 ^ 2 * e7 ^ 3 + e3 * e6 ^ 4 * y1 ^ 2 +
3 * e1 * e6 ^ 3 * e7 ^ 2 - 2 * e6 ^ 4 * x2 * e1 ^ 2 + 2 * e1 * e6 ^ 4 * e5 -
2 * e3 * e6 ^ 4 * e7 - 2 * e6 ^ 4 * x1 * e1 ^ 2 + e1 ^ 3 * x3 ^ 2 * e6 ^ 3 -
2 * e6 ^ 4 * e1 ^ 2 * x3 + x2 ^ 4 * e3 ^ 3 * y1 ^ 2 * e1 ^ 2 +
x2 ^ 4 * e3 ^ 3 * y2 ^ 2 * e1 ^ 2 + x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 ^ 2 +
x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 ^ 2 + 4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 4 * y2 ^ 2 +
x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 ^ 2 + x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 ^ 2 +
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 4 * y2 ^ 2 + 4 * e3 ^ 3 * x1 ^ 4 * y1 ^ 2 * e1 ^ 2 +
4 * e3 ^ 3 * x1 ^ 4 * y2 ^ 2 * e1 ^ 2 + e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 ^ 2 +
e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e6 ^ 2 + 4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 4 * y2 ^ 2 +
x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 ^ 2 + x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * e6 ^ 2 +
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 ^ 4 + x2 ^ 2 * e3 ^ 3 * e2 ^ 2 * y1 ^ 2 +
x2 ^ 2 * e3 ^ 3 * e2 ^ 2 * y3 ^ 2 + x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 ^ 2 +
x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e6 ^ 2 + 4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 ^ 4 +
x3 ^ 2 * e3 ^ 3 * e2 ^ 2 * y1 ^ 2 + x3 ^ 2 * e3 ^ 3 * e2 ^ 2 * y3 ^ 2 +
e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e5 ^ 2 + e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e6 ^ 2 +
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * y2 ^ 4 + e3 ^ 3 * x1 ^ 2 * e2 ^ 2 * y1 ^ 2 +
e3 ^ 3 * x1 ^ 2 * e2 ^ 2 * y3 ^ 2 - 2 * e6 ^ 3 * x2 * e3 ^ 2 * y1 ^ 2 -
2 * e6 ^ 3 * x3 * e3 ^ 2 * y1 ^ 2 - 2 * e6 ^ 3 * e3 ^ 2 * x1 * y1 ^ 2 -
2 * e6 ^ 3 * x2 * e3 ^ 2 * y2 ^ 2 - 2 * e6 ^ 3 * x3 * e3 ^ 2 * y2 ^ 2 -
2 * e6 ^ 3 * e3 ^ 2 * x1 * y2 ^ 2 + 2 * e3 * e6 ^ 3 * y1 ^ 2 * e5 -
4 * e3 * e6 ^ 3 * y1 ^ 3 * y2 + 4 * e3 * e6 ^ 4 * y1 * y2 -
4 * e3 * e6 ^ 3 * y1 ^ 2 * y2 ^ 2 + 2 * e3 * e6 ^ 3 * y1 ^ 2 * e2 +
2 * e3 * e6 ^ 3 * y2 ^ 2 * e5 - 4 * e3 * e6 ^ 3 * y2 ^ 3 * y1 +
e3 * e6 ^ 2 * y1 ^ 2 * e5 ^ 2 + 4 * e3 * e6 ^ 2 * y1 ^ 4 * y2 ^ 2 +
2 * e3 * e6 ^ 3 * e7 * y1 ^ 2 + e3 * e7 ^ 2 * y1 ^ 2 * e5 ^ 2 +
e3 * e7 ^ 2 * y1 ^ 2 * e6 ^ 2 + 4 * e3 * e7 ^ 2 * y1 ^ 4 * y2 ^ 2 +
16 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 4 + e3 * e6 ^ 2 * y2 ^ 2 * e5 ^ 2 +
4 * e3 * e6 ^ 2 * y1 ^ 2 * y2 ^ 4 + e3 * e6 ^ 2 * e2 ^ 2 * y1 ^ 2 +
e3 * e6 ^ 2 * e2 ^ 2 * y3 ^ 2 + 2 * e3 * e6 ^ 3 * e7 * y2 ^ 2 +
e3 * e7 ^ 2 * y2 ^ 2 * e5 ^ 2 + e3 * e7 ^ 2 * y2 ^ 2 * e6 ^ 2 +
x1 ^ 2 * e1 ^ 3 * e6 ^ 3 + x2 ^ 2 * e1 ^ 3 * e6 ^ 3 + e1 * e5 ^ 2 * e7 ^ 3 +
e3 * e6 ^ 4 * y2 ^ 2 - 24 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 -
8 * y2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e5 * e1 +
32 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 * e5 * e6 +
8 * y2 * y3 ^ 2 * x2 * e3 ^ 2 * y1 * e5 * e2 -
24 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e6 * x1 * e1 -
8 * y2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e6 * e1 +
16 * y2 ^ 2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 ^ 3 * e1 +
8 * y2 * y3 ^ 2 * x2 * e3 ^ 2 * y1 * e6 * e2 +
48 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 ^ 3 * x1 * e1 -
16 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * x1 * e1 +
24 * y2 ^ 3 * y3 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e1 -
16 * y2 ^ 2 * y3 ^ 2 * x2 * e3 ^ 2 * y1 ^ 2 * e2 +
8 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * e6 -
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 ^ 3 * e5 +
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 * e5 ^ 2 -
16 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e5 +
8 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * e2 -
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 ^ 3 * e6 +
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 * e6 ^ 2 -
16 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e6 +
16 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e6 * e2 -
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 ^ 3 * e2 +
32 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * y2 * y3 * x2 ^ 3 * e3 ^ 2 * y1 ^ 2 * e1 ^ 2 +
8 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * e5 * e6 -
16 * y2 ^ 4 * y3 * x2 * e3 ^ 2 * e5 * y1 -
16 * y2 ^ 4 * y3 * x2 * e3 ^ 2 * e6 * y1 +
16 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e2 +
32 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * y2 ^ 3 * y3 * x2 ^ 3 * e3 ^ 2 * e1 ^ 2 +
8 * y2 * y3 ^ 2 * x2 * e3 ^ 2 * e2 ^ 2 * y1 +
4 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 +
4 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * e6 ^ 2 +
16 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * y1 ^ 4 -
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 -
8 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x2 * e1 +
32 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e5 * e6 +
8 * y2 * y3 ^ 2 * x3 * e3 ^ 2 * y1 * e5 * e2 -
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * x1 * e1 -
8 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * x2 * e1 +
8 * y2 * y3 ^ 2 * x3 * e3 ^ 2 * y1 * e6 * e2 +
32 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 ^ 3 * x1 * e1 +
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 ^ 3 * x2 * e1 -
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 +
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x2 * e1 -
16 * y2 ^ 2 * y3 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * e2 +
8 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * e6 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 ^ 3 * e5 +
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e5 ^ 2 -
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 +
8 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * e2 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 ^ 3 * e6 +
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e6 ^ 2 -
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e6 +
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * e2 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 ^ 3 * e2 +
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
8 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e5 * e6 -
16 * y2 ^ 4 * y3 * x3 * e3 ^ 2 * e5 * y1 -
16 * y2 ^ 4 * y3 * x3 * e3 ^ 2 * e6 * y1 +
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e2 +
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * x2 ^ 2 * e1 ^ 2 +
8 * y2 * y3 ^ 2 * x3 * e3 ^ 2 * e2 ^ 2 * y1 +
4 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 +
4 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * e6 ^ 2 +
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * y1 ^ 4 -
16 * y2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e5 * e1 +
32 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 * e5 * e6 +
8 * y2 * y3 ^ 2 * e3 ^ 2 * x1 * y1 * e5 * e2 -
16 * y2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e6 * e1 +
8 * y2 * y3 ^ 2 * e3 ^ 2 * x1 * y1 * e6 * e2 +
32 * y2 ^ 2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 ^ 3 * e1 -
8 * y2 ^ 3 * y3 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e1 -
16 * y2 ^ 2 * y3 ^ 2 * e3 ^ 2 * x1 * y1 ^ 2 * e2 +
8 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * e6 -
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 ^ 3 * e5 +
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 * e5 ^ 2 -
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e5 +
8 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * e2 -
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 ^ 3 * e6 +
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 * e6 ^ 2 -
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e6 +
16 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e6 * e2 -
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * y1 ^ 3 * e2 +
16 * y2 * y3 * e3 ^ 2 * x1 ^ 3 * y1 ^ 2 * e1 ^ 2 +
20 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
8 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * e5 * e6 -
16 * y2 ^ 4 * y3 * e3 ^ 2 * x1 * e5 * y1 -
16 * y2 ^ 4 * y3 * e3 ^ 2 * x1 * e6 * y1 +
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e2 +
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 ^ 3 * e1 ^ 2 +
20 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * x2 ^ 2 * e1 ^ 2 +
8 * y2 * y3 ^ 2 * e3 ^ 2 * x1 * e2 ^ 2 * y1 +
4 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e5 ^ 2 +
4 * y2 * y3 * e3 ^ 2 * x1 * y1 ^ 2 * e6 ^ 2 +
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * y1 ^ 4 -
8 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * x1 * e1 -
2 * x2 ^ 3 * e3 ^ 3 * y1 ^ 2 * e5 * e1 +
8 * x2 ^ 2 * e3 ^ 3 * y1 * e5 * y2 * e6 +
2 * x2 ^ 2 * e3 ^ 3 * y1 * e5 * e2 * y3 -
8 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * x1 * e1 -
2 * x2 ^ 3 * e3 ^ 3 * y1 ^ 2 * e6 * e1 +
2 * x2 ^ 2 * e3 ^ 3 * y1 * e6 * e2 * y3 +
16 * x2 ^ 2 * e3 ^ 3 * y1 ^ 3 * y2 * x1 * e1 +
4 * x2 ^ 3 * e3 ^ 3 * y1 ^ 3 * y2 * e1 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 * e2 * y3 +
2 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * e6 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 3 * e5 * y2 +
4 * x2 ^ 2 * e3 ^ 3 * y1 * e5 ^ 2 * y2 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * y2 ^ 2 +
2 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * e2 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 3 * e6 * y2 +
4 * x2 ^ 2 * e3 ^ 3 * y1 * e6 ^ 2 * y2 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * y2 ^ 2 +
2 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * e2 -
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 3 * y2 * e2 +
13 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
2 * x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 * e6 -
4 * x2 ^ 2 * e3 ^ 3 * y2 ^ 3 * e5 * y1 -
4 * x2 ^ 2 * e3 ^ 3 * y2 ^ 3 * e6 * y1 +
4 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 ^ 2 * e2 +
13 * x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
2 * x2 ^ 2 * e3 ^ 3 * e2 ^ 2 * y1 * y3 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * x1 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * x2 * e1 +
8 * x3 ^ 2 * e3 ^ 3 * y1 * e5 * y2 * e6 +
2 * x3 ^ 2 * e3 ^ 3 * y1 * e5 * e2 * y3 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * x1 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * x2 * e1 +
2 * x3 ^ 2 * e3 ^ 3 * y1 * e6 * e2 * y3 +
8 * x3 ^ 2 * e3 ^ 3 * y1 ^ 3 * y2 * x1 * e1 +
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 3 * y2 * x2 * e1 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 * e2 * y3 +
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * e6 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 3 * e5 * y2 +
4 * x3 ^ 2 * e3 ^ 3 * y1 * e5 ^ 2 * y2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * y2 ^ 2 +
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e5 * e2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 3 * e6 * y2 +
4 * x3 ^ 2 * e3 ^ 3 * y1 * e6 ^ 2 * y2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * y2 ^ 2 +
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * e6 * e2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 3 * y2 * e2 +
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
2 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 * e6 -
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 3 * e5 * y1 -
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 3 * e6 * y1 +
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * y2 ^ 2 * e2 +
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 +
2 * x3 ^ 2 * e3 ^ 3 * e2 ^ 2 * y1 * y3 -
4 * e3 ^ 3 * x1 ^ 3 * y1 ^ 2 * e5 * e1 -
10 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 * x2 * e1 +
8 * e3 ^ 3 * x1 ^ 2 * y1 * e5 * y2 * e6 +
2 * e3 ^ 3 * x1 ^ 2 * y1 * e5 * e2 * y3 -
4 * e3 ^ 3 * x1 ^ 3 * y1 ^ 2 * e6 * e1 -
10 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e6 * x2 * e1 +
2 * e3 ^ 3 * x1 ^ 2 * y1 * e6 * e2 * y3 +
8 * e3 ^ 3 * x1 ^ 3 * y1 ^ 3 * y2 * e1 +
20 * e3 ^ 3 * x1 ^ 2 * y1 ^ 3 * y2 * x2 * e1 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * y2 * e2 * y3 +
2 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 * e6 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 3 * e5 * y2 +
4 * e3 ^ 3 * x1 ^ 2 * y1 * e5 ^ 2 * y2 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 +
2 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 * e2 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 3 * e6 * y2 +
4 * e3 ^ 3 * x1 ^ 2 * y1 * e6 ^ 2 * y2 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e6 * y2 ^ 2 +
2 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e6 * e2 -
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 3 * y2 * e2 +
2 * e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e5 * e6 -
4 * e3 ^ 3 * x1 ^ 2 * y2 ^ 3 * e5 * y1 -
4 * e3 ^ 3 * x1 ^ 2 * y2 ^ 3 * e6 * y1 +
4 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 +
2 * e3 ^ 3 * x1 ^ 2 * e2 ^ 2 * y1 * y3 +
4 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * e5 ^ 2 +
4 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * e6 ^ 2 +
16 * y2 ^ 5 * y3 * x2 * e3 ^ 2 * y1 ^ 2 +
4 * y2 * y3 * x2 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 +
4 * y2 * y3 ^ 3 * x2 * e3 ^ 2 * e2 ^ 2 -
32 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 * e5 * x1 * e1 -
40 * y2 ^ 2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 * e5 * e1 -
32 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * y1 * e6 * x1 * e1 -
40 * y2 ^ 2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 * e6 * e1 -
24 * y2 * y3 * x2 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
24 * y2 ^ 2 * y3 * x2 ^ 3 * e3 ^ 2 * y1 * e1 ^ 2 -
8 * y2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e1 * e2 -
24 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * e5 * x1 * e1 -
8 * y2 ^ 3 * y3 * x2 ^ 2 * e3 ^ 2 * e5 * e1 -
8 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * e5 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * x2 * e3 ^ 2 * e5 * e2 -
24 * y2 ^ 3 * y3 * x2 * e3 ^ 2 * e6 * x1 * e1 -
8 * y2 ^ 3 * y3 * x2 ^ 2 * e3 ^ 2 * e6 * e1 -
16 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * e6 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * x2 * e3 ^ 2 * e6 * e2 +
48 * y2 ^ 4 * y3 * x2 * e3 ^ 2 * y1 * x1 * e1 +
16 * y2 ^ 4 * y3 * x2 ^ 2 * e3 ^ 2 * y1 * e1 +
16 * y2 ^ 3 * y3 ^ 2 * x2 * e3 ^ 2 * y1 * e2 +
24 * y2 ^ 2 * y3 * x2 ^ 2 * e3 ^ 2 * y1 * x1 * e1 ^ 2 -
24 * y2 * y3 ^ 2 * x2 * e3 ^ 2 * y1 * x1 * e1 * e2 -
8 * y2 * y3 ^ 2 * x2 ^ 2 * e3 ^ 2 * y1 * e1 * e2 +
24 * y2 ^ 2 * y3 * x2 * e3 ^ 2 * x1 * e1 * e2 * y1 +
24 * y2 ^ 2 * y3 ^ 2 * x2 * e3 ^ 2 * x1 * e1 * e2 +
8 * y2 ^ 2 * y3 * x2 ^ 2 * e3 ^ 2 * e1 * e2 * y1 +
8 * y2 ^ 2 * y3 ^ 2 * x2 ^ 2 * e3 ^ 2 * e1 * e2 +
4 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e5 ^ 2 +
4 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e6 ^ 2 +
16 * y2 ^ 5 * y3 * x3 * e3 ^ 2 * y1 ^ 2 +
4 * y2 * y3 * x3 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 +
4 * y2 * y3 ^ 3 * x3 * e3 ^ 2 * e2 ^ 2 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e5 * x1 * e1 -
32 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e5 * x2 * e1 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e6 * x1 * e1 -
32 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * e6 * x2 * e1 +
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 -
16 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
24 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 -
8 * y2 * y3 * x3 * e3 ^ 2 * y1 ^ 2 * x2 * e1 * e2 -
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e5 * x1 * e1 -
8 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e5 * x2 * e1 -
8 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * e5 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * x3 * e3 ^ 2 * e5 * e2 -
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e6 * x1 * e1 -
8 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * e6 * x2 * e1 -
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * e6 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * x3 * e3 ^ 2 * e6 * e2 +
32 * y2 ^ 4 * y3 * x3 * e3 ^ 2 * y1 * x1 * e1 +
16 * y2 ^ 4 * y3 * x3 * e3 ^ 2 * y1 * x2 * e1 +
16 * y2 ^ 3 * y3 ^ 2 * x3 * e3 ^ 2 * y1 * e2 +
16 * y2 ^ 3 * y3 * x3 * e3 ^ 2 * x1 * e1 ^ 2 * x2 -
16 * y2 * y3 ^ 2 * x3 * e3 ^ 2 * y1 * x1 * e1 * e2 -
8 * y2 * y3 ^ 2 * x3 * e3 ^ 2 * y1 * x2 * e1 * e2 +
16 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * x1 * e1 * e2 * y1 +
16 * y2 ^ 2 * y3 ^ 2 * x3 * e3 ^ 2 * x1 * e1 * e2 +
8 * y2 ^ 2 * y3 * x3 * e3 ^ 2 * x2 * e1 * e2 * y1 +
8 * y2 ^ 2 * y3 ^ 2 * x3 * e3 ^ 2 * x2 * e1 * e2 +
4 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * e5 ^ 2 +
4 * y2 ^ 3 * y3 * e3 ^ 2 * x1 * e6 ^ 2 +
16 * y2 ^ 5 * y3 * e3 ^ 2 * x1 * y1 ^ 2 +
4 * y2 * y3 * e3 ^ 2 * x1 * e2 ^ 2 * y1 ^ 2 +
4 * y2 * y3 ^ 3 * e3 ^ 2 * x1 * e2 ^ 2 -
24 * y2 ^ 2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 * e5 * e1 -
24 * y2 ^ 2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 * e6 * e1 -
16 * y2 * y3 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e1 * e2 -
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 ^ 2 * e5 * e1 -
8 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * e5 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * e3 ^ 2 * x1 * e5 * e2 -
16 * y2 ^ 3 * y3 * e3 ^ 2 * x1 ^ 2 * e6 * e1 -
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 * e6 * e2 * y1 -
8 * y2 ^ 2 * y3 ^ 2 * e3 ^ 2 * x1 * e6 * e2 +
32 * y2 ^ 4 * y3 * e3 ^ 2 * x1 ^ 2 * y1 * e1 +
16 * y2 ^ 3 * y3 ^ 2 * e3 ^ 2 * x1 * y1 * e2 -
16 * y2 * y3 ^ 2 * e3 ^ 2 * x1 ^ 2 * y1 * e1 * e2 +
16 * y2 ^ 2 * y3 * e3 ^ 2 * x1 ^ 2 * e1 * e2 * y1 +
16 * y2 ^ 2 * y3 ^ 2 * e3 ^ 2 * x1 ^ 2 * e1 * e2 -
16 * x2 ^ 2 * e3 ^ 3 * y1 * e5 * y2 * x1 * e1 -
4 * x2 ^ 3 * e3 ^ 3 * y1 * e5 * y2 * e1 -
16 * x2 ^ 2 * e3 ^ 3 * y1 * e6 * y2 * x1 * e1 -
4 * x2 ^ 3 * e3 ^ 3 * y1 * e6 * y2 * e1 +
6 * x2 ^ 3 * e3 ^ 3 * y1 ^ 2 * x1 * e1 ^ 2 +
10 * x2 ^ 2 * e3 ^ 3 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
8 * x2 ^ 2 * e3 ^ 3 * y1 ^ 2 * x1 * e1 * e2 -
2 * x2 ^ 3 * e3 ^ 3 * y1 ^ 2 * e1 * e2 -
8 * x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 * x1 * e1 -
2 * x2 ^ 3 * e3 ^ 3 * y2 ^ 2 * e5 * e1 -
2 * x2 ^ 2 * e3 ^ 3 * y2 * e5 * e2 * y1 -
2 * x2 ^ 2 * e3 ^ 3 * y2 * e5 * e2 * y3 -
8 * x2 ^ 2 * e3 ^ 3 * y2 ^ 2 * e6 * x1 * e1 -
2 * x2 ^ 3 * e3 ^ 3 * y2 ^ 2 * e6 * e1 -
2 * x2 ^ 2 * e3 ^ 3 * y2 * e6 * e2 * y1 -
2 * x2 ^ 2 * e3 ^ 3 * y2 * e6 * e2 * y3 +
16 * x2 ^ 2 * e3 ^ 3 * y1 * y2 ^ 3 * x1 * e1 +
4 * x2 ^ 3 * e3 ^ 3 * y1 * y2 ^ 3 * e1 +
4 * x2 ^ 2 * e3 ^ 3 * y1 * y2 ^ 2 * e2 * y3 +
6 * x2 ^ 3 * e3 ^ 3 * y2 ^ 2 * x1 * e1 ^ 2 +
4 * x2 ^ 3 * e3 ^ 3 * y1 * x1 * e1 ^ 2 * y2 -
8 * x2 ^ 2 * e3 ^ 3 * y1 * x1 * e1 * e2 * y3 -
2 * x2 ^ 3 * e3 ^ 3 * y1 * e1 * e2 * y3 +
8 * x2 ^ 2 * e3 ^ 3 * y2 * x1 * e1 * e2 * y1 +
8 * x2 ^ 2 * e3 ^ 3 * y2 * x1 * e1 * e2 * y3 +
2 * x2 ^ 3 * e3 ^ 3 * y2 * e1 * e2 * y1 +
2 * x2 ^ 3 * e3 ^ 3 * y2 * e1 * e2 * y3 -
8 * x3 ^ 2 * e3 ^ 3 * y1 * e5 * y2 * x1 * e1 -
4 * x3 ^ 2 * e3 ^ 3 * y1 * e5 * y2 * x2 * e1 -
8 * x3 ^ 2 * e3 ^ 3 * y1 * e6 * y2 * x1 * e1 -
4 * x3 ^ 2 * e3 ^ 3 * y1 * e6 * y2 * x2 * e1 +
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * x1 * e1 ^ 2 * x2 +
4 * x3 ^ 2 * e3 ^ 3 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * x1 * e1 * e2 -
14 * x3 ^ 2 * e3 ^ 3 * y1 * x2 ^ 2 * e1 ^ 2 * y2 -
2 * x3 ^ 2 * e3 ^ 3 * y1 ^ 2 * x2 * e1 * e2 -
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 * x1 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e5 * x2 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 * e5 * e2 * y1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 * e5 * e2 * y3 -
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e6 * x1 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * e6 * x2 * e1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 * e6 * e2 * y1 -
2 * x3 ^ 2 * e3 ^ 3 * y2 * e6 * e2 * y3 +
8 * x3 ^ 2 * e3 ^ 3 * y1 * y2 ^ 3 * x1 * e1 +
4 * x3 ^ 2 * e3 ^ 3 * y1 * y2 ^ 3 * x2 * e1 +
4 * x3 ^ 2 * e3 ^ 3 * y1 * y2 ^ 2 * e2 * y3 +
4 * x3 ^ 2 * e3 ^ 3 * y2 ^ 2 * x1 * e1 ^ 2 * x2 -
8 * x3 ^ 2 * e3 ^ 3 * y1 * x1 * e1 ^ 2 * y2 * x2 -
4 * x3 ^ 2 * e3 ^ 3 * y1 * x1 * e1 * e2 * y3 -
2 * x3 ^ 2 * e3 ^ 3 * y1 * x2 * e1 * e2 * y3 +
4 * x3 ^ 2 * e3 ^ 3 * y2 * x1 * e1 * e2 * y1 +
4 * x3 ^ 2 * e3 ^ 3 * y2 * x1 * e1 * e2 * y3 +
2 * x3 ^ 2 * e3 ^ 3 * y2 * x2 * e1 * e2 * y1 +
2 * x3 ^ 2 * e3 ^ 3 * y2 * x2 * e1 * e2 * y3 -
8 * e3 ^ 3 * x1 ^ 3 * y1 * e5 * y2 * e1 -
20 * e3 ^ 3 * x1 ^ 2 * y1 * e5 * y2 * x2 * e1 -
8 * e3 ^ 3 * x1 ^ 3 * y1 * e6 * y2 * e1 -
20 * e3 ^ 3 * x1 ^ 2 * y1 * e6 * y2 * x2 * e1 +
12 * e3 ^ 3 * x1 ^ 3 * y1 ^ 2 * e1 ^ 2 * x2 +
2 * e3 ^ 3 * x1 ^ 4 * y1 * e1 ^ 2 * y2 -
4 * e3 ^ 3 * x1 ^ 3 * y1 ^ 2 * e1 * e2 -
10 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * x2 * e1 * e2 -
4 * e3 ^ 3 * x1 ^ 3 * y2 ^ 2 * e5 * e1 -
10 * e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e5 * x2 * e1 -
2 * e3 ^ 3 * x1 ^ 2 * y2 * e5 * e2 * y1 -
2 * e3 ^ 3 * x1 ^ 2 * y2 * e5 * e2 * y3 -
4 * e3 ^ 3 * x1 ^ 3 * y2 ^ 2 * e6 * e1 -
10 * e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e6 * x2 * e1 -
2 * e3 ^ 3 * x1 ^ 2 * y2 * e6 * e2 * y1 -
2 * e3 ^ 3 * x1 ^ 2 * y2 * e6 * e2 * y3 +
8 * e3 ^ 3 * x1 ^ 3 * y1 * y2 ^ 3 * e1 +
20 * e3 ^ 3 * x1 ^ 2 * y1 * y2 ^ 3 * x2 * e1 +
4 * e3 ^ 3 * x1 ^ 2 * y1 * y2 ^ 2 * e2 * y3 +
12 * e3 ^ 3 * x1 ^ 3 * y2 ^ 2 * e1 ^ 2 * x2 +
8 * e3 ^ 3 * x1 ^ 3 * y1 * e1 ^ 2 * y2 * x2 -
4 * e3 ^ 3 * x1 ^ 3 * y1 * e1 * e2 * y3 -
10 * e3 ^ 3 * x1 ^ 2 * y1 * x2 * e1 * e2 * y3 +
4 * e3 ^ 3 * x1 ^ 3 * y2 * e1 * e2 * y1 +
4 * e3 ^ 3 * x1 ^ 3 * y2 * e1 * e2 * y3 +
10 * e3 ^ 3 * x1 ^ 2 * y2 * x2 * e1 * e2 * y1 +
10 * e3 ^ 3 * x1 ^ 2 * y2 * x2 * e1 * e2 * y3 +
2 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * e5 ^ 2 -
12 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 * x1 * e1 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 * e1 +
16 * x2 * e3 ^ 3 * x3 * y1 * e5 * y2 * e6 +
4 * x2 * e3 ^ 3 * x3 * y1 * e5 * e2 * y3 -
12 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e6 * x1 * e1 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y1 ^ 2 * e6 * e1 +
4 * x2 * e3 ^ 3 * x3 * y1 * e6 * e2 * y3 +
24 * x2 * e3 ^ 3 * x3 * y1 ^ 3 * y2 * x1 * e1 +
8 * x2 ^ 2 * e3 ^ 3 * x3 * y1 ^ 3 * y2 * e1 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * y2 * e2 * y3 +
4 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 * e6 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 3 * e5 * y2 +
8 * x2 * e3 ^ 3 * x3 * y1 * e5 ^ 2 * y2 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 * y2 ^ 2 +
4 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 * e2 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 3 * e6 * y2 +
8 * x2 * e3 ^ 3 * x3 * y1 * e6 ^ 2 * y2 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e6 * y2 ^ 2 +
4 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e6 * e2 -
8 * x2 * e3 ^ 3 * x3 * y1 ^ 3 * y2 * e2 +
16 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
2 * x2 ^ 3 * e3 ^ 3 * x3 * y1 ^ 2 * e1 ^ 2 +
4 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * e5 * e6 -
8 * x2 * e3 ^ 3 * x3 * y2 ^ 3 * e5 * y1 -
8 * x2 * e3 ^ 3 * x3 * y2 ^ 3 * e6 * y1 +
8 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * y2 ^ 2 * e2 +
16 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
2 * x2 ^ 3 * e3 ^ 3 * x3 * y2 ^ 2 * e1 ^ 2 +
4 * x2 * e3 ^ 3 * x3 * e2 ^ 2 * y1 * y3 +
2 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e5 ^ 2 +
2 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * e6 ^ 2 +
8 * x2 * e3 ^ 3 * x3 * y1 ^ 4 * y2 ^ 2 +
16 * x2 * e3 ^ 3 * x1 * y1 * e5 * y2 * e6 +
4 * x2 * e3 ^ 3 * x1 * y1 * e5 * e2 * y3 +
4 * x2 * e3 ^ 3 * x1 * y1 * e6 * e2 * y3 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * y2 * e2 * y3 +
4 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * e6 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 3 * e5 * y2 +
8 * x2 * e3 ^ 3 * x1 * y1 * e5 ^ 2 * y2 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * y2 ^ 2 +
4 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * e2 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 3 * e6 * y2 +
8 * x2 * e3 ^ 3 * x1 * y1 * e6 ^ 2 * y2 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e6 * y2 ^ 2 +
4 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e6 * e2 -
8 * x2 * e3 ^ 3 * x1 * y1 ^ 3 * y2 * e2 +
4 * x2 * e3 ^ 3 * x1 * y2 ^ 2 * e5 * e6 -
8 * x2 * e3 ^ 3 * x1 * y2 ^ 3 * e5 * y1 -
8 * x2 * e3 ^ 3 * x1 * y2 ^ 3 * e6 * y1 +
8 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * y2 ^ 2 * e2 +
4 * x2 * e3 ^ 3 * x1 * e2 ^ 2 * y1 * y3 +
2 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e5 ^ 2 +
2 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * e6 ^ 2 +
8 * x2 * e3 ^ 3 * x1 * y1 ^ 4 * y2 ^ 2 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e5 * e1 +
16 * x3 * e3 ^ 3 * x1 * y1 * e5 * y2 * e6 +
4 * x3 * e3 ^ 3 * x1 * y1 * e5 * e2 * y3 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e6 * e1 +
4 * x3 * e3 ^ 3 * x1 * y1 * e6 * e2 * y3 +
16 * x3 * e3 ^ 3 * x1 ^ 2 * y1 ^ 3 * y2 * e1 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * y2 * e2 * y3 +
4 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * e6 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 3 * e5 * y2 +
8 * x3 * e3 ^ 3 * x1 * y1 * e5 ^ 2 * y2 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * y2 ^ 2 +
4 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e5 * e2 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 3 * e6 * y2 +
8 * x3 * e3 ^ 3 * x1 * y1 * e6 ^ 2 * y2 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e6 * y2 ^ 2 +
4 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e6 * e2 -
8 * x3 * e3 ^ 3 * x1 * y1 ^ 3 * y2 * e2 +
8 * x3 * e3 ^ 3 * x1 ^ 3 * y1 ^ 2 * e1 ^ 2 +
10 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
4 * x3 * e3 ^ 3 * x1 * y2 ^ 2 * e5 * e6 -
8 * x3 * e3 ^ 3 * x1 * y2 ^ 3 * e5 * y1 -
8 * x3 * e3 ^ 3 * x1 * y2 ^ 3 * e6 * y1 +
8 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * y2 ^ 2 * e2 +
8 * x3 * e3 ^ 3 * x1 ^ 3 * y2 ^ 2 * e1 ^ 2 +
10 * x3 * e3 ^ 3 * x1 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 +
4 * x3 * e3 ^ 3 * x1 * e2 ^ 2 * y1 * y3 +
2 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e5 ^ 2 +
2 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * e6 ^ 2 +
8 * x3 * e3 ^ 3 * x1 * y1 ^ 4 * y2 ^ 2 +
12 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e5 * e1 -
16 * e6 ^ 2 * x2 * e3 ^ 2 * y1 * e5 * y2 -
4 * e6 * x2 * e3 ^ 2 * y1 * e5 * e2 * y3 +
12 * e6 ^ 2 * x2 * e3 ^ 2 * y1 ^ 2 * x1 * e1 +
4 * e6 ^ 2 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e1 -
4 * e6 ^ 2 * x2 * e3 ^ 2 * y1 * e2 * y3 -
24 * e6 * x2 * e3 ^ 2 * y1 ^ 3 * y2 * x1 * e1 -
8 * e6 * x2 ^ 2 * e3 ^ 2 * y1 ^ 3 * y2 * e1 +
8 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e1 -
4 * e6 ^ 2 * x2 * e3 ^ 2 * y1 ^ 2 * e5 +
8 * e6 * x2 * e3 ^ 2 * y1 ^ 3 * e5 * y2 -
8 * e6 * x2 * e3 ^ 2 * y1 * e5 ^ 2 * y2 +
8 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * e2 +
8 * e6 ^ 2 * x2 * e3 ^ 2 * y1 ^ 3 * y2 - 8 * e6 ^ 3 * x2 * e3 ^ 2 * y1 * y2 +
8 * e6 ^ 2 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 -
4 * e6 ^ 2 * x2 * e3 ^ 2 * y1 ^ 2 * e2 +
8 * e6 * x2 * e3 ^ 2 * y1 ^ 3 * y2 * e2 -
16 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e6 * x2 ^ 3 * e3 ^ 2 * y1 ^ 2 * e1 ^ 2 -
4 * e6 ^ 2 * x2 * e3 ^ 2 * y2 ^ 2 * e5 +
8 * e6 * x2 * e3 ^ 2 * y2 ^ 3 * e5 * y1 +
8 * e6 ^ 2 * x2 * e3 ^ 2 * y2 ^ 3 * y1 -
8 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 -
16 * e6 * x2 * e3 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
6 * e6 * x2 ^ 3 * e3 ^ 2 * y2 ^ 2 * e1 ^ 2 -
4 * e6 * x2 * e3 ^ 2 * e2 ^ 2 * y1 * y3 -
2 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 -
8 * e6 * x2 * e3 ^ 2 * y1 ^ 4 * y2 ^ 2 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 +
4 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x2 * e1 -
16 * e6 ^ 2 * x3 * e3 ^ 2 * y1 * e5 * y2 -
4 * e6 * x3 * e3 ^ 2 * y1 * e5 * e2 * y3 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 +
4 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * x2 * e1 -
4 * e6 ^ 2 * x3 * e3 ^ 2 * y1 * e2 * y3 -
16 * e6 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * x1 * e1 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * x2 * e1 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x2 * e1 -
4 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * e5 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 3 * e5 * y2 -
8 * e6 * x3 * e3 ^ 2 * y1 * e5 ^ 2 * y2 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * e2 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 3 * y2 - 8 * e6 ^ 3 * x3 * e3 ^ 2 * y1 * y2 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 -
4 * e6 ^ 2 * x3 * e3 ^ 2 * y1 ^ 2 * e2 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * e2 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e6 ^ 2 * x3 * e3 ^ 2 * y2 ^ 2 * e5 +
8 * e6 * x3 * e3 ^ 2 * y2 ^ 3 * e5 * y1 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y2 ^ 3 * y1 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 -
8 * e6 * x3 * e3 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
14 * e6 * x3 * e3 ^ 2 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e6 * x3 * e3 ^ 2 * e2 ^ 2 * y1 * y3 -
2 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 4 * y2 ^ 2 +
8 * e6 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e5 * e1 -
16 * e6 ^ 2 * e3 ^ 2 * x1 * y1 * e5 * y2 -
4 * e6 * e3 ^ 2 * x1 * y1 * e5 * e2 * y3 +
8 * e6 ^ 2 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e1 -
4 * e6 ^ 2 * e3 ^ 2 * x1 * y1 * e2 * y3 -
16 * e6 * e3 ^ 2 * x1 ^ 2 * y1 ^ 3 * y2 * e1 +
4 * e6 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * y2 ^ 2 * e1 -
4 * e6 ^ 2 * e3 ^ 2 * x1 * y1 ^ 2 * e5 +
8 * e6 * e3 ^ 2 * x1 * y1 ^ 3 * e5 * y2 -
8 * e6 * e3 ^ 2 * x1 * y1 * e5 ^ 2 * y2 +
8 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * e2 +
8 * e6 ^ 2 * e3 ^ 2 * x1 * y1 ^ 3 * y2 - 8 * e6 ^ 3 * e3 ^ 2 * x1 * y1 * y2 +
8 * e6 ^ 2 * e3 ^ 2 * x1 * y1 ^ 2 * y2 ^ 2 -
4 * e6 ^ 2 * e3 ^ 2 * x1 * y1 ^ 2 * e2 +
8 * e6 * e3 ^ 2 * x1 * y1 ^ 3 * y2 * e2 -
8 * e6 * e3 ^ 2 * x1 ^ 3 * y1 ^ 2 * e1 ^ 2 -
10 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e6 ^ 2 * e3 ^ 2 * x1 * y2 ^ 2 * e5 +
8 * e6 * e3 ^ 2 * x1 * y2 ^ 3 * e5 * y1 +
8 * e6 ^ 2 * e3 ^ 2 * x1 * y2 ^ 3 * y1 -
8 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * y2 ^ 2 * e2 -
8 * e6 * e3 ^ 2 * x1 ^ 3 * y2 ^ 2 * e1 ^ 2 -
2 * e6 * e3 ^ 2 * x1 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e6 * e3 ^ 2 * x1 * e2 ^ 2 * y1 * y3 -
2 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * e5 ^ 2 -
8 * e6 * e3 ^ 2 * x1 * y1 ^ 4 * y2 ^ 2 +
12 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e5 * e1 -
16 * e7 * x2 * e3 ^ 2 * y1 * e5 * y2 * e6 -
4 * e7 * x2 * e3 ^ 2 * y1 * e5 * e2 * y3 +
12 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e6 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e6 * e1 -
4 * e7 * x2 * e3 ^ 2 * y1 * e6 * e2 * y3 -
24 * e7 * x2 * e3 ^ 2 * y1 ^ 3 * y2 * x1 * e1 -
8 * e7 * x2 ^ 2 * e3 ^ 2 * y1 ^ 3 * y2 * e1 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e1 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * y2 * e2 * y3 -
4 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * e6 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 3 * e5 * y2 -
8 * e7 * x2 * e3 ^ 2 * y1 * e5 ^ 2 * y2 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e5 * e2 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 3 * e6 * y2 -
8 * e7 * x2 * e3 ^ 2 * y1 * e6 ^ 2 * y2 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e6 * y2 ^ 2 -
4 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e6 * e2 +
8 * e7 * x2 * e3 ^ 2 * y1 ^ 3 * y2 * e2 -
16 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e7 * x2 ^ 3 * e3 ^ 2 * y1 ^ 2 * e1 ^ 2 -
4 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * e5 * e6 +
8 * e7 * x2 * e3 ^ 2 * y2 ^ 3 * e5 * y1 +
8 * e7 * x2 * e3 ^ 2 * y2 ^ 3 * e6 * y1 -
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 -
16 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e7 * x2 ^ 3 * e3 ^ 2 * y2 ^ 2 * e1 ^ 2 -
4 * e7 * x2 * e3 ^ 2 * e2 ^ 2 * y1 * y3 -
2 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 -
2 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * e6 ^ 2 -
8 * e7 * x2 * e3 ^ 2 * y1 ^ 4 * y2 ^ 2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 +
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * x2 * e1 -
16 * e7 * x3 * e3 ^ 2 * y1 * e5 * y2 * e6 -
4 * e7 * x3 * e3 ^ 2 * y1 * e5 * e2 * y3 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * x1 * e1 +
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * x2 * e1 -
4 * e7 * x3 * e3 ^ 2 * y1 * e6 * e2 * y3 -
16 * e7 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * x1 * e1 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * x2 * e1 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * x2 * e1 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * y2 * e2 * y3 -
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * e6 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 3 * e5 * y2 -
8 * e7 * x3 * e3 ^ 2 * y1 * e5 ^ 2 * y2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 * e2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 3 * e6 * y2 -
8 * e7 * x3 * e3 ^ 2 * y1 * e6 ^ 2 * y2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * y2 ^ 2 -
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e6 * e2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 3 * y2 * e2 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e5 * e6 +
8 * e7 * x3 * e3 ^ 2 * y2 ^ 3 * e5 * y1 +
8 * e7 * x3 * e3 ^ 2 * y2 ^ 3 * e6 * y1 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 -
8 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 -
2 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e7 * x3 * e3 ^ 2 * e2 ^ 2 * y1 * y3 -
2 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e5 ^ 2 -
2 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * e6 ^ 2 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 4 * y2 ^ 2 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e5 * e1 -
16 * e7 * e3 ^ 2 * x1 * y1 * e5 * y2 * e6 -
4 * e7 * e3 ^ 2 * x1 * y1 * e5 * e2 * y3 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e6 * e1 -
4 * e7 * e3 ^ 2 * x1 * y1 * e6 * e2 * y3 -
16 * e7 * e3 ^ 2 * x1 ^ 2 * y1 ^ 3 * y2 * e1 +
4 * e7 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * y2 ^ 2 * e1 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * y2 * e2 * y3 -
4 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * e6 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 3 * e5 * y2 -
8 * e7 * e3 ^ 2 * x1 * y1 * e5 ^ 2 * y2 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * y2 ^ 2 -
4 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e5 * e2 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 3 * e6 * y2 -
8 * e7 * e3 ^ 2 * x1 * y1 * e6 ^ 2 * y2 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e6 * y2 ^ 2 -
4 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e6 * e2 +
8 * e7 * e3 ^ 2 * x1 * y1 ^ 3 * y2 * e2 -
8 * e7 * e3 ^ 2 * x1 ^ 3 * y1 ^ 2 * e1 ^ 2 -
10 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e7 * e3 ^ 2 * x1 * y2 ^ 2 * e5 * e6 +
8 * e7 * e3 ^ 2 * x1 * y2 ^ 3 * e5 * y1 +
8 * e7 * e3 ^ 2 * x1 * y2 ^ 3 * e6 * y1 -
8 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * y2 ^ 2 * e2 -
8 * e7 * e3 ^ 2 * x1 ^ 3 * y2 ^ 2 * e1 ^ 2 -
10 * e7 * e3 ^ 2 * x1 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 -
4 * e7 * e3 ^ 2 * x1 * e2 ^ 2 * y1 * y3 -
2 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e5 ^ 2 -
2 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * e6 ^ 2 -
8 * e7 * e3 ^ 2 * x1 * y1 ^ 4 * y2 ^ 2 +
2 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * e6 ^ 2 +
8 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * y2 ^ 4 +
2 * x2 * e3 ^ 3 * x3 * e2 ^ 2 * y1 ^ 2 +
2 * x2 * e3 ^ 3 * x3 * e2 ^ 2 * y3 ^ 2 -
24 * x2 * e3 ^ 3 * x3 * y1 * e5 * y2 * x1 * e1 -
8 * x2 ^ 2 * e3 ^ 3 * x3 * y1 * e5 * y2 * e1 -
24 * x2 * e3 ^ 3 * x3 * y1 * e6 * y2 * x1 * e1 -
8 * x2 ^ 2 * e3 ^ 3 * x3 * y1 * e6 * y2 * e1 +
16 * x2 * e3 ^ 3 * x3 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
12 * x2 * e3 ^ 3 * x3 * y1 ^ 2 * x1 * e1 * e2 -
4 * x2 ^ 3 * e3 ^ 3 * x3 * y1 * e1 ^ 2 * y2 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y1 ^ 2 * e1 * e2 -
12 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * e5 * x1 * e1 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y2 ^ 2 * e5 * e1 -
4 * x2 * e3 ^ 3 * x3 * y2 * e5 * e2 * y1 -
4 * x2 * e3 ^ 3 * x3 * y2 * e5 * e2 * y3 -
12 * x2 * e3 ^ 3 * x3 * y2 ^ 2 * e6 * x1 * e1 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y2 ^ 2 * e6 * e1 -
4 * x2 * e3 ^ 3 * x3 * y2 * e6 * e2 * y1 -
4 * x2 * e3 ^ 3 * x3 * y2 * e6 * e2 * y3 +
24 * x2 * e3 ^ 3 * x3 * y1 * y2 ^ 3 * x1 * e1 +
8 * x2 ^ 2 * e3 ^ 3 * x3 * y1 * y2 ^ 3 * e1 +
8 * x2 * e3 ^ 3 * x3 * y1 * y2 ^ 2 * e2 * y3 +
4 * x2 ^ 2 * e3 ^ 3 * x3 * y1 * x1 * e1 ^ 2 * y2 -
12 * x2 * e3 ^ 3 * x3 * y1 * x1 * e1 * e2 * y3 -
4 * x2 ^ 2 * e3 ^ 3 * x3 * y1 * e1 * e2 * y3 +
12 * x2 * e3 ^ 3 * x3 * y2 * x1 * e1 * e2 * y1 +
12 * x2 * e3 ^ 3 * x3 * y2 * x1 * e1 * e2 * y3 +
4 * x2 ^ 2 * e3 ^ 3 * x3 * y2 * e1 * e2 * y1 +
4 * x2 ^ 2 * e3 ^ 3 * x3 * y2 * e1 * e2 * y3 +
2 * x2 * e3 ^ 3 * x1 * y2 ^ 2 * e5 ^ 2 +
2 * x2 * e3 ^ 3 * x1 * y2 ^ 2 * e6 ^ 2 +
8 * x2 * e3 ^ 3 * x1 * y1 ^ 2 * y2 ^ 4 +
2 * x2 * e3 ^ 3 * x1 * e2 ^ 2 * y1 ^ 2 +
2 * x2 * e3 ^ 3 * x1 * e2 ^ 2 * y3 ^ 2 -
4 * x2 * e3 ^ 3 * x1 * y2 * e5 * e2 * y1 -
4 * x2 * e3 ^ 3 * x1 * y2 * e5 * e2 * y3 -
4 * x2 * e3 ^ 3 * x1 * y2 * e6 * e2 * y1 -
4 * x2 * e3 ^ 3 * x1 * y2 * e6 * e2 * y3 +
8 * x2 * e3 ^ 3 * x1 * y1 * y2 ^ 2 * e2 * y3 +
2 * x3 * e3 ^ 3 * x1 * y2 ^ 2 * e5 ^ 2 +
2 * x3 * e3 ^ 3 * x1 * y2 ^ 2 * e6 ^ 2 +
8 * x3 * e3 ^ 3 * x1 * y1 ^ 2 * y2 ^ 4 +
2 * x3 * e3 ^ 3 * x1 * e2 ^ 2 * y1 ^ 2 +
2 * x3 * e3 ^ 3 * x1 * e2 ^ 2 * y3 ^ 2 -
16 * x3 * e3 ^ 3 * x1 ^ 2 * y1 * e5 * y2 * e1 -
16 * x3 * e3 ^ 3 * x1 ^ 2 * y1 * e6 * y2 * e1 +
8 * x3 * e3 ^ 3 * x1 ^ 3 * y1 * e1 ^ 2 * y2 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y1 ^ 2 * e1 * e2 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e5 * e1 -
4 * x3 * e3 ^ 3 * x1 * y2 * e5 * e2 * y1 -
4 * x3 * e3 ^ 3 * x1 * y2 * e5 * e2 * y3 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y2 ^ 2 * e6 * e1 -
4 * x3 * e3 ^ 3 * x1 * y2 * e6 * e2 * y1 -
4 * x3 * e3 ^ 3 * x1 * y2 * e6 * e2 * y3 +
16 * x3 * e3 ^ 3 * x1 ^ 2 * y1 * y2 ^ 3 * e1 +
8 * x3 * e3 ^ 3 * x1 * y1 * y2 ^ 2 * e2 * y3 -
8 * x3 * e3 ^ 3 * x1 ^ 2 * y1 * e1 * e2 * y3 +
8 * x3 * e3 ^ 3 * x1 ^ 2 * y2 * e1 * e2 * y1 +
8 * x3 * e3 ^ 3 * x1 ^ 2 * y2 * e1 * e2 * y3 -
2 * e6 * x2 * e3 ^ 2 * y2 ^ 2 * e5 ^ 2 -
8 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 4 -
2 * e6 * x2 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 -
2 * e6 * x2 * e3 ^ 2 * e2 ^ 2 * y3 ^ 2 +
16 * e6 * x2 * e3 ^ 2 * y1 * e5 * y2 * x1 * e1 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 * e5 * y2 * e1 +
16 * e6 ^ 2 * x2 * e3 ^ 2 * y1 * y2 * x1 * e1 +
4 * e6 ^ 2 * x2 ^ 2 * e3 ^ 2 * y1 * y2 * e1 +
12 * e6 * x2 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
4 * e6 * x2 ^ 3 * e3 ^ 2 * y1 * e1 ^ 2 * y2 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e1 * e2 +
12 * e6 * x2 * e3 ^ 2 * y2 ^ 2 * e5 * x1 * e1 -
4 * e6 * x2 ^ 2 * e3 ^ 2 * y2 ^ 2 * e5 * e1 +
4 * e6 * x2 * e3 ^ 2 * y2 * e5 * e2 * y1 +
4 * e6 * x2 * e3 ^ 2 * y2 * e5 * e2 * y3 +
12 * e6 ^ 2 * x2 * e3 ^ 2 * y2 ^ 2 * x1 * e1 +
4 * e6 ^ 2 * x2 * e3 ^ 2 * y2 * e2 * y1 +
4 * e6 ^ 2 * x2 * e3 ^ 2 * y2 * e2 * y3 -
24 * e6 * x2 * e3 ^ 2 * y1 * y2 ^ 3 * x1 * e1 +
8 * e6 * x2 ^ 2 * e3 ^ 2 * y1 * y2 ^ 3 * e1 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 * x1 * e1 ^ 2 * y2 +
12 * e6 * x2 * e3 ^ 2 * y1 * x1 * e1 * e2 * y3 +
4 * e6 * x2 ^ 2 * e3 ^ 2 * y1 * e1 * e2 * y3 -
12 * e6 * x2 * e3 ^ 2 * y2 * x1 * e1 * e2 * y1 -
12 * e6 * x2 * e3 ^ 2 * y2 * x1 * e1 * e2 * y3 -
4 * e6 * x2 ^ 2 * e3 ^ 2 * y2 * e1 * e2 * y1 -
4 * e6 * x2 ^ 2 * e3 ^ 2 * y2 * e1 * e2 * y3 -
2 * e6 * x3 * e3 ^ 2 * y2 ^ 2 * e5 ^ 2 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 4 -
2 * e6 * x3 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 -
2 * e6 * x3 * e3 ^ 2 * e2 ^ 2 * y3 ^ 2 +
8 * e6 * x3 * e3 ^ 2 * y1 * e5 * y2 * x1 * e1 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y1 * y2 * x1 * e1 -
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 +
8 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
20 * e6 * x3 * e3 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 * y2 +
4 * e6 * x3 * e3 ^ 2 * y1 ^ 2 * x2 * e1 * e2 +
8 * e6 * x3 * e3 ^ 2 * y2 ^ 2 * e5 * x1 * e1 -
4 * e6 * x3 * e3 ^ 2 * y2 ^ 2 * e5 * x2 * e1 +
4 * e6 * x3 * e3 ^ 2 * y2 * e5 * e2 * y1 +
4 * e6 * x3 * e3 ^ 2 * y2 * e5 * e2 * y3 +
8 * e6 ^ 2 * x3 * e3 ^ 2 * y2 ^ 2 * x1 * e1 +
4 * e6 ^ 2 * x3 * e3 ^ 2 * y2 * e2 * y1 +
4 * e6 ^ 2 * x3 * e3 ^ 2 * y2 * e2 * y3 -
16 * e6 * x3 * e3 ^ 2 * y1 * y2 ^ 3 * x1 * e1 +
8 * e6 * x3 * e3 ^ 2 * y1 * y2 ^ 3 * x2 * e1 +
16 * e6 * x3 * e3 ^ 2 * y1 * x1 * e1 ^ 2 * y2 * x2 +
8 * e6 * x3 * e3 ^ 2 * y1 * x1 * e1 * e2 * y3 +
4 * e6 * x3 * e3 ^ 2 * y1 * x2 * e1 * e2 * y3 -
8 * e6 * x3 * e3 ^ 2 * y2 * x1 * e1 * e2 * y1 -
8 * e6 * x3 * e3 ^ 2 * y2 * x1 * e1 * e2 * y3 -
4 * e6 * x3 * e3 ^ 2 * y2 * x2 * e1 * e2 * y1 -
4 * e6 * x3 * e3 ^ 2 * y2 * x2 * e1 * e2 * y3 -
2 * e6 * e3 ^ 2 * x1 * y2 ^ 2 * e5 ^ 2 -
8 * e6 * e3 ^ 2 * x1 * y1 ^ 2 * y2 ^ 4 -
2 * e6 * e3 ^ 2 * x1 * e2 ^ 2 * y1 ^ 2 -
2 * e6 * e3 ^ 2 * x1 * e2 ^ 2 * y3 ^ 2 +
12 * e6 * e3 ^ 2 * x1 ^ 2 * y1 * e5 * y2 * e1 +
12 * e6 ^ 2 * e3 ^ 2 * x1 ^ 2 * y1 * y2 * e1 +
8 * e6 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e1 * e2 +
8 * e6 * e3 ^ 2 * x1 ^ 2 * y2 ^ 2 * e5 * e1 +
4 * e6 * e3 ^ 2 * x1 * y2 * e5 * e2 * y1 +
4 * e6 * e3 ^ 2 * x1 * y2 * e5 * e2 * y3 +
8 * e6 ^ 2 * e3 ^ 2 * x1 ^ 2 * y2 ^ 2 * e1 +
4 * e6 ^ 2 * e3 ^ 2 * x1 * y2 * e2 * y1 +
4 * e6 ^ 2 * e3 ^ 2 * x1 * y2 * e2 * y3 -
16 * e6 * e3 ^ 2 * x1 ^ 2 * y1 * y2 ^ 3 * e1 +
8 * e6 * e3 ^ 2 * x1 ^ 2 * y1 * e1 * e2 * y3 -
8 * e6 * e3 ^ 2 * x1 ^ 2 * y2 * e1 * e2 * y1 -
8 * e6 * e3 ^ 2 * x1 ^ 2 * y2 * e1 * e2 * y3 -
2 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * e5 ^ 2 -
2 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * e6 ^ 2 -
8 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * y2 ^ 4 -
2 * e7 * x2 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 -
2 * e7 * x2 * e3 ^ 2 * e2 ^ 2 * y3 ^ 2 +
16 * e7 * x2 * e3 ^ 2 * y1 * e5 * y2 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 * e5 * y2 * e1 +
16 * e7 * x2 * e3 ^ 2 * y1 * e6 * y2 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 * e6 * y2 * e1 +
12 * e7 * x2 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
4 * e7 * x2 ^ 3 * e3 ^ 2 * y1 * e1 ^ 2 * y2 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 ^ 2 * e1 * e2 +
12 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * e5 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y2 ^ 2 * e5 * e1 +
4 * e7 * x2 * e3 ^ 2 * y2 * e5 * e2 * y1 +
4 * e7 * x2 * e3 ^ 2 * y2 * e5 * e2 * y3 +
12 * e7 * x2 * e3 ^ 2 * y2 ^ 2 * e6 * x1 * e1 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y2 ^ 2 * e6 * e1 +
4 * e7 * x2 * e3 ^ 2 * y2 * e6 * e2 * y1 +
4 * e7 * x2 * e3 ^ 2 * y2 * e6 * e2 * y3 -
24 * e7 * x2 * e3 ^ 2 * y1 * y2 ^ 3 * x1 * e1 -
8 * e7 * x2 ^ 2 * e3 ^ 2 * y1 * y2 ^ 3 * e1 -
8 * e7 * x2 * e3 ^ 2 * y1 * y2 ^ 2 * e2 * y3 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 * x1 * e1 ^ 2 * y2 +
12 * e7 * x2 * e3 ^ 2 * y1 * x1 * e1 * e2 * y3 +
4 * e7 * x2 ^ 2 * e3 ^ 2 * y1 * e1 * e2 * y3 -
12 * e7 * x2 * e3 ^ 2 * y2 * x1 * e1 * e2 * y1 -
12 * e7 * x2 * e3 ^ 2 * y2 * x1 * e1 * e2 * y3 -
4 * e7 * x2 ^ 2 * e3 ^ 2 * y2 * e1 * e2 * y1 -
4 * e7 * x2 ^ 2 * e3 ^ 2 * y2 * e1 * e2 * y3 -
2 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e5 ^ 2 -
2 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e6 ^ 2 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * y2 ^ 4 -
2 * e7 * x3 * e3 ^ 2 * e2 ^ 2 * y1 ^ 2 -
2 * e7 * x3 * e3 ^ 2 * e2 ^ 2 * y3 ^ 2 +
8 * e7 * x3 * e3 ^ 2 * y1 * e5 * y2 * x1 * e1 +
8 * e7 * x3 * e3 ^ 2 * y1 * e6 * y2 * x1 * e1 -
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 +
8 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
20 * e7 * x3 * e3 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 * y2 +
4 * e7 * x3 * e3 ^ 2 * y1 ^ 2 * x2 * e1 * e2 +
8 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e5 * x1 * e1 +
4 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e5 * x2 * e1 +
4 * e7 * x3 * e3 ^ 2 * y2 * e5 * e2 * y1 +
4 * e7 * x3 * e3 ^ 2 * y2 * e5 * e2 * y3 +
8 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e6 * x1 * e1 +
4 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * e6 * x2 * e1 +
4 * e7 * x3 * e3 ^ 2 * y2 * e6 * e2 * y1 +
4 * e7 * x3 * e3 ^ 2 * y2 * e6 * e2 * y3 -
16 * e7 * x3 * e3 ^ 2 * y1 * y2 ^ 3 * x1 * e1 -
8 * e7 * x3 * e3 ^ 2 * y1 * y2 ^ 3 * x2 * e1 -
8 * e7 * x3 * e3 ^ 2 * y1 * y2 ^ 2 * e2 * y3 -
8 * e7 * x3 * e3 ^ 2 * y2 ^ 2 * x1 * e1 ^ 2 * x2 +
16 * e7 * x3 * e3 ^ 2 * y1 * x1 * e1 ^ 2 * y2 * x2 +
8 * e7 * x3 * e3 ^ 2 * y1 * x1 * e1 * e2 * y3 +
4 * e7 * x3 * e3 ^ 2 * y1 * x2 * e1 * e2 * y3 -
8 * e7 * x3 * e3 ^ 2 * y2 * x1 * e1 * e2 * y1 -
8 * e7 * x3 * e3 ^ 2 * y2 * x1 * e1 * e2 * y3 -
4 * e7 * x3 * e3 ^ 2 * y2 * x2 * e1 * e2 * y1 -
4 * e7 * x3 * e3 ^ 2 * y2 * x2 * e1 * e2 * y3 -
2 * e7 * e3 ^ 2 * x1 * y2 ^ 2 * e5 ^ 2 -
2 * e7 * e3 ^ 2 * x1 * y2 ^ 2 * e6 ^ 2 -
8 * e7 * e3 ^ 2 * x1 * y1 ^ 2 * y2 ^ 4 -
2 * e7 * e3 ^ 2 * x1 * e2 ^ 2 * y1 ^ 2 -
2 * e7 * e3 ^ 2 * x1 * e2 ^ 2 * y3 ^ 2 +
12 * e7 * e3 ^ 2 * x1 ^ 2 * y1 * e5 * y2 * e1 +
12 * e7 * e3 ^ 2 * x1 ^ 2 * y1 * e6 * y2 * e1 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y1 ^ 2 * e1 * e2 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y2 ^ 2 * e5 * e1 +
4 * e7 * e3 ^ 2 * x1 * y2 * e5 * e2 * y1 +
4 * e7 * e3 ^ 2 * x1 * y2 * e5 * e2 * y3 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y2 ^ 2 * e6 * e1 +
4 * e7 * e3 ^ 2 * x1 * y2 * e6 * e2 * y1 +
4 * e7 * e3 ^ 2 * x1 * y2 * e6 * e2 * y3 -
16 * e7 * e3 ^ 2 * x1 ^ 2 * y1 * y2 ^ 3 * e1 -
8 * e7 * e3 ^ 2 * x1 * y1 * y2 ^ 2 * e2 * y3 +
8 * e7 * e3 ^ 2 * x1 ^ 2 * y1 * e1 * e2 * y3 -
8 * e7 * e3 ^ 2 * x1 ^ 2 * y2 * e1 * e2 * y1 -
8 * e7 * e3 ^ 2 * x1 ^ 2 * y2 * e1 * e2 * y3 + 8 * e3 * e6 ^ 3 * y1 * e5 * y2 -
4 * e3 * e6 ^ 3 * y1 ^ 2 * x1 * e1 - 2 * e3 * e6 ^ 3 * y1 ^ 2 * x2 * e1 +
2 * e3 * e6 ^ 3 * y1 * e2 * y3 - 4 * e3 * e6 ^ 2 * y1 ^ 3 * e5 * y2 +
x1 ^ 2 * e1 ^ 3 * e7 ^ 3 + 4 * e3 * e6 ^ 2 * y1 * e5 ^ 2 * y2 -
4 * e3 * e6 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 + 2 * e3 * e6 ^ 2 * y1 ^ 2 * e5 * e2 -
4 * e3 * e6 ^ 2 * y1 ^ 3 * y2 * e2 +
4 * e3 * e6 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
e3 * e6 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 - 4 * e3 * e6 ^ 2 * y2 ^ 3 * e5 * y1 +
4 * e3 * e6 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 +
4 * e3 * e6 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 -
7 * e3 * e6 ^ 2 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 +
2 * e3 * e6 ^ 2 * e2 ^ 2 * y1 * y3 + 4 * e3 * e6 ^ 2 * e7 * y1 ^ 2 * e5 -
8 * e3 * e6 ^ 2 * e7 * y1 ^ 3 * y2 + 8 * e3 * e6 ^ 3 * e7 * y1 * y2 -
8 * e3 * e6 ^ 2 * e7 * y1 ^ 2 * y2 ^ 2 + 4 * e3 * e6 ^ 2 * e7 * y1 ^ 2 * e2 +
4 * e3 * e6 ^ 2 * e7 * y2 ^ 2 * e5 - 8 * e3 * e6 ^ 2 * e7 * y2 ^ 3 * y1 +
2 * e3 * e6 * e7 * y1 ^ 2 * e5 ^ 2 + 8 * e3 * e6 * e7 * y1 ^ 4 * y2 ^ 2 +
2 * e3 * e7 ^ 2 * y1 ^ 2 * e5 * e6 - 4 * e3 * e7 ^ 2 * y1 ^ 3 * e5 * y2 +
4 * e3 * e7 ^ 2 * y1 * e5 ^ 2 * y2 - 4 * e3 * e6 ^ 2 * y1 ^ 2 * e5 * x1 * e1 -
2 * e3 * e6 ^ 2 * y1 ^ 2 * e5 * x2 * e1 + 2 * e3 * e6 ^ 2 * y1 * e5 * e2 * y3 +
8 * e3 * e6 ^ 2 * y1 ^ 3 * y2 * x1 * e1 +
4 * e3 * e6 ^ 2 * y1 ^ 3 * y2 * x2 * e1 -
8 * e3 * e6 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 -
8 * e3 * e6 ^ 2 * y1 ^ 2 * y2 ^ 2 * x2 * e1 -
12 * e3 * e6 ^ 2 * y1 ^ 2 * y2 * e2 * y3 + e1 * e5 ^ 2 * e6 ^ 3 -
8 * e3 * e6 * e7 * y1 ^ 2 * e5 * x1 * e1 -
4 * e3 * e6 * e7 * y1 ^ 2 * e5 * x2 * e1 +
16 * e3 * e6 ^ 2 * e7 * y1 * e5 * y2 + 4 * e3 * e6 * e7 * y1 * e5 * e2 * y3 -
8 * e3 * e6 ^ 2 * e7 * y1 ^ 2 * x1 * e1 -
4 * e3 * e6 ^ 2 * e7 * y1 ^ 2 * x2 * e1 + 4 * e3 * e6 ^ 2 * e7 * y1 * e2 * y3 +
16 * e3 * e6 * e7 * y1 ^ 3 * y2 * x1 * e1 +
8 * e3 * e6 * e7 * y1 ^ 3 * y2 * x2 * e1 -
16 * e3 * e6 * e7 * y1 ^ 2 * y2 ^ 2 * x1 * e1 -
16 * e3 * e6 * e7 * y1 ^ 2 * y2 ^ 2 * x2 * e1 -
16 * e3 * e6 * e7 * y1 ^ 2 * y2 * e2 * y3 -
8 * e3 * e6 * e7 * y1 ^ 3 * e5 * y2 + 8 * e3 * e6 * e7 * y1 * e5 ^ 2 * y2 -
8 * e3 * e6 * e7 * y1 ^ 2 * e5 * y2 ^ 2 + 4 * e3 * e6 * e7 * y1 ^ 2 * e5 * e2 -
8 * e3 * e6 * e7 * y1 ^ 3 * y2 * e2 +
8 * e3 * e6 * e7 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
2 * e3 * e6 * e7 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
8 * e3 * e6 * e7 * y2 ^ 3 * e5 * y1 + 8 * e3 * e6 * e7 * y1 ^ 2 * y2 ^ 2 * e2 +
8 * e3 * e6 * e7 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 -
6 * e3 * e6 * e7 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 +
4 * e3 * e6 * e7 * e2 ^ 2 * y1 * y3 - 4 * e3 * e7 ^ 2 * y1 ^ 2 * e5 * x1 * e1 -
2 * e3 * e7 ^ 2 * y1 ^ 2 * e5 * x2 * e1 + 8 * e3 * e7 ^ 2 * y1 * e5 * y2 * e6 +
2 * e3 * e7 ^ 2 * y1 * e5 * e2 * y3 - 4 * e3 * e7 ^ 2 * y1 ^ 2 * e6 * x1 * e1 -
2 * e3 * e7 ^ 2 * y1 ^ 2 * e6 * x2 * e1 + 2 * e3 * e7 ^ 2 * y1 * e6 * e2 * y3 +
8 * e3 * e7 ^ 2 * y1 ^ 3 * y2 * x1 * e1 +
4 * e3 * e7 ^ 2 * y1 ^ 3 * y2 * x2 * e1 -
8 * e3 * e7 ^ 2 * y1 ^ 2 * y2 ^ 2 * x1 * e1 -
8 * e3 * e7 ^ 2 * y1 ^ 2 * y2 ^ 2 * x2 * e1 -
4 * e3 * e7 ^ 2 * y1 ^ 2 * y2 * e2 * y3 -
4 * e3 * e7 ^ 2 * y1 ^ 2 * e5 * y2 ^ 2 + 2 * e3 * e7 ^ 2 * y1 ^ 2 * e5 * e2 -
4 * e3 * e7 ^ 2 * y1 ^ 3 * e6 * y2 + 4 * e3 * e7 ^ 2 * y1 * e6 ^ 2 * y2 -
4 * e3 * e7 ^ 2 * y1 ^ 2 * e6 * y2 ^ 2 + 2 * e3 * e7 ^ 2 * y1 ^ 2 * e6 * e2 -
4 * e3 * e7 ^ 2 * y1 ^ 3 * y2 * e2 +
4 * e3 * e7 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
e3 * e7 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 + 2 * e3 * e7 ^ 2 * y2 ^ 2 * e5 * e6 -
4 * e3 * e7 ^ 2 * y2 ^ 3 * e5 * y1 - 4 * e3 * e7 ^ 2 * y2 ^ 3 * e6 * y1 +
4 * e3 * e7 ^ 2 * y1 ^ 2 * y2 ^ 2 * e2 +
4 * e3 * e7 ^ 2 * y2 ^ 2 * x1 ^ 2 * e1 ^ 2 +
e3 * e7 ^ 2 * y2 ^ 2 * x2 ^ 2 * e1 ^ 2 + 2 * e3 * e7 ^ 2 * e2 ^ 2 * y1 * y3 -
16 * e3 * y2 ^ 3 * y3 ^ 3 * y1 ^ 2 * e2 -
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 ^ 3 * e5 +
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * e5 ^ 2 -
16 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 2 * e5 -
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 ^ 3 * e6 +
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * e6 ^ 2 -
16 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 2 * e6 -
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 ^ 3 * e2 + 8 * e3 * y2 ^ 4 * y3 ^ 2 * e5 * e6 -
16 * e3 * y2 ^ 5 * y3 ^ 2 * e5 * y1 - 16 * e3 * y2 ^ 5 * y3 ^ 2 * e6 * y1 +
16 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 2 * e2 +
16 * e3 * y2 ^ 4 * y3 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * e3 * y2 ^ 4 * y3 ^ 2 * x2 ^ 2 * e1 ^ 2 +
8 * e3 * y2 ^ 2 * y3 ^ 3 * e2 ^ 2 * y1 +
4 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e5 ^ 2 +
4 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e6 ^ 2 -
4 * e3 * e6 ^ 3 * y2 ^ 2 * x1 * e1 + 2 * e3 * e6 ^ 3 * y2 ^ 2 * x2 * e1 -
2 * e3 * e6 ^ 3 * y2 * e2 * y1 - 2 * e3 * e6 ^ 3 * y2 * e2 * y3 +
2 * e3 * e6 * e7 * y2 ^ 2 * e5 ^ 2 + 8 * e3 * e6 * e7 * y1 ^ 2 * y2 ^ 4 +
2 * e3 * e6 * e7 * e2 ^ 2 * y1 ^ 2 + 2 * e3 * e6 * e7 * e2 ^ 2 * y3 ^ 2 +
4 * e3 * y2 ^ 2 * y3 ^ 2 * e2 ^ 2 * y1 ^ 2 -
8 * e3 * y2 ^ 3 * y3 ^ 3 * e5 * e2 - 8 * e3 * y2 ^ 3 * y3 ^ 3 * e6 * e2 +
16 * e3 * y2 ^ 4 * y3 ^ 3 * y1 * e2 + 16 * e3 * e6 ^ 2 * y2 ^ 2 * y3 * y1 ^ 3 -
16 * e3 * e6 ^ 3 * y2 ^ 2 * y3 * y1 + 16 * e3 * e6 ^ 2 * y2 ^ 3 * y3 * y1 ^ 2 -
8 * e3 * e6 ^ 2 * y2 ^ 3 * y3 * e5 -
16 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e5 * x1 * e1 -
8 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e5 * x2 * e1 +
32 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * e5 * e6 +
8 * e3 * y2 ^ 2 * y3 ^ 3 * y1 * e5 * e2 -
16 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e6 * x1 * e1 +
8 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e6 * x2 * e1 +
8 * e3 * y2 ^ 2 * y3 ^ 3 * y1 * e6 * e2 +
32 * e3 * y2 ^ 3 * y3 ^ 2 * y1 ^ 3 * x1 * e1 +
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 ^ 3 * x2 * e1 -
32 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 2 * x1 * e1 +
32 * e3 * y2 ^ 4 * y3 ^ 2 * y1 ^ 2 * x2 * e1 +
8 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e5 * e6 +
8 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e5 * e2 + x2 ^ 2 * e1 ^ 3 * e7 ^ 3 +
24 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e6 * e2 +
16 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 +
4 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
4 * e3 * e7 ^ 2 * y1 ^ 2 * y2 ^ 4 + e3 * e7 ^ 2 * e2 ^ 2 * y1 ^ 2 +
e3 * e7 ^ 2 * e2 ^ 2 * y3 ^ 2 + 4 * e3 * y2 ^ 4 * y3 ^ 2 * e5 ^ 2 +
4 * e3 * y2 ^ 4 * y3 ^ 2 * e6 ^ 2 + 16 * e3 * y2 ^ 6 * y3 ^ 2 * y1 ^ 2 +
4 * e3 * y2 ^ 2 * y3 ^ 4 * e2 ^ 2 - 4 * e3 * e6 ^ 3 * y2 ^ 3 * y3 +
4 * e3 * e6 ^ 2 * y1 * e5 * y2 * x2 * e1 +
4 * e3 * e6 ^ 3 * y1 * y2 * x2 * e1 +
4 * e3 * e6 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 -
6 * e3 * e6 ^ 2 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
4 * e3 * e6 ^ 2 * y1 ^ 2 * x1 * e1 * e2 -
8 * e3 * e6 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 * y2 -
2 * e3 * e6 ^ 2 * y1 ^ 2 * x2 * e1 * e2 -
4 * e3 * e6 ^ 2 * y2 ^ 2 * e5 * x1 * e1 +
6 * e3 * e6 ^ 2 * y2 ^ 2 * e5 * x2 * e1 - 2 * e3 * e6 ^ 2 * y2 * e5 * e2 * y1 -
2 * e3 * e6 ^ 2 * y2 * e5 * e2 * y3 + 8 * e3 * e6 ^ 2 * y1 * y2 ^ 3 * x1 * e1 -
12 * e3 * e6 ^ 2 * y1 * y2 ^ 3 * x2 * e1 +
12 * e3 * e6 ^ 2 * y1 * y2 ^ 2 * e2 * y3 -
4 * e3 * e6 ^ 2 * y2 ^ 2 * x1 * e1 ^ 2 * x2 -
12 * e3 * e6 ^ 2 * y1 * x1 * e1 ^ 2 * y2 * x2 -
4 * e3 * e6 ^ 2 * y1 * x1 * e1 * e2 * y3 -
2 * e3 * e6 ^ 2 * y1 * x2 * e1 * e2 * y3 +
4 * e3 * e6 ^ 2 * y2 * x1 * e1 * e2 * y1 +
4 * e3 * e6 ^ 2 * y2 * x1 * e1 * e2 * y3 +
2 * e3 * e6 ^ 2 * y2 * x2 * e1 * e2 * y1 +
2 * e3 * e6 ^ 2 * y2 * x2 * e1 * e2 * y3 +
8 * e3 * e6 * e7 * y1 * e5 * y2 * x2 * e1 +
8 * e3 * e6 ^ 2 * e7 * y1 * y2 * x2 * e1 +
8 * e3 * e6 * e7 * y1 ^ 2 * x1 * e1 ^ 2 * x2 -
12 * e3 * e6 * e7 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
8 * e3 * e6 * e7 * y1 ^ 2 * x1 * e1 * e2 -
16 * e3 * e6 * e7 * y1 * x2 ^ 2 * e1 ^ 2 * y2 -
4 * e3 * e6 * e7 * y1 ^ 2 * x2 * e1 * e2 -
8 * e3 * e6 * e7 * y2 ^ 2 * e5 * x1 * e1 +
4 * e3 * e6 * e7 * y2 ^ 2 * e5 * x2 * e1 -
4 * e3 * e6 * e7 * y2 * e5 * e2 * y1 - 4 * e3 * e6 * e7 * y2 * e5 * e2 * y3 -
8 * e3 * e6 ^ 2 * e7 * y2 ^ 2 * x1 * e1 - 4 * e3 * e6 ^ 2 * e7 * y2 * e2 * y1 -
4 * e3 * e6 ^ 2 * e7 * y2 * e2 * y3 +
16 * e3 * e6 * e7 * y1 * y2 ^ 3 * x1 * e1 -
8 * e3 * e6 * e7 * y1 * y2 ^ 3 * x2 * e1 +
16 * e3 * e6 * e7 * y1 * y2 ^ 2 * e2 * y3 -
24 * e3 * e6 * e7 * y1 * x1 * e1 ^ 2 * y2 * x2 -
8 * e3 * e6 * e7 * y1 * x1 * e1 * e2 * y3 -
4 * e3 * e6 * e7 * y1 * x2 * e1 * e2 * y3 +
8 * e3 * e6 * e7 * y2 * x1 * e1 * e2 * y1 +
8 * e3 * e6 * e7 * y2 * x1 * e1 * e2 * y3 +
4 * e3 * e6 * e7 * y2 * x2 * e1 * e2 * y1 +
4 * e3 * e6 * e7 * y2 * x2 * e1 * e2 * y3 +
4 * e3 * e7 ^ 2 * y1 * e5 * y2 * x2 * e1 +
4 * e3 * e7 ^ 2 * y1 * e6 * y2 * x2 * e1 +
4 * e3 * e7 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 -
6 * e3 * e7 ^ 2 * y1 * x1 ^ 2 * e1 ^ 2 * y2 -
4 * e3 * e7 ^ 2 * y1 ^ 2 * x1 * e1 * e2 -
8 * e3 * e7 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 * y2 -
2 * e3 * e7 ^ 2 * y1 ^ 2 * x2 * e1 * e2 -
4 * e3 * e7 ^ 2 * y2 ^ 2 * e5 * x1 * e1 -
2 * e3 * e7 ^ 2 * y2 ^ 2 * e5 * x2 * e1 - 2 * e3 * e7 ^ 2 * y2 * e5 * e2 * y1 -
2 * e3 * e7 ^ 2 * y2 * e5 * e2 * y3 - 4 * e3 * e7 ^ 2 * y2 ^ 2 * e6 * x1 * e1 -
2 * e3 * e7 ^ 2 * y2 ^ 2 * e6 * x2 * e1 - 2 * e3 * e7 ^ 2 * y2 * e6 * e2 * y1 -
2 * e3 * e7 ^ 2 * y2 * e6 * e2 * y3 + 8 * e3 * e7 ^ 2 * y1 * y2 ^ 3 * x1 * e1 +
4 * e3 * e7 ^ 2 * y1 * y2 ^ 3 * x2 * e1 +
4 * e3 * e7 ^ 2 * y1 * y2 ^ 2 * e2 * y3 +
4 * e3 * e7 ^ 2 * y2 ^ 2 * x1 * e1 ^ 2 * x2 -
12 * e3 * e7 ^ 2 * y1 * x1 * e1 ^ 2 * y2 * x2 -
4 * e3 * e7 ^ 2 * y1 * x1 * e1 * e2 * y3 -
2 * e3 * e7 ^ 2 * y1 * x2 * e1 * e2 * y3 +
4 * e3 * e7 ^ 2 * y2 * x1 * e1 * e2 * y1 +
4 * e3 * e7 ^ 2 * y2 * x1 * e1 * e2 * y3 +
2 * e3 * e7 ^ 2 * y2 * x2 * e1 * e2 * y1 +
2 * e3 * e7 ^ 2 * y2 * x2 * e1 * e2 * y3 -
48 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * e5 * x2 * e1 -
48 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * e6 * x2 * e1 +
16 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * x1 * e1 ^ 2 * x2 -
24 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * x1 ^ 2 * e1 ^ 2 -
16 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * x1 * e1 * e2 +
32 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * x2 ^ 2 * e1 ^ 2 -
8 * e3 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * x2 * e1 * e2 -
16 * e3 * y2 ^ 4 * y3 ^ 2 * e5 * x1 * e1 -
8 * e3 * y2 ^ 4 * y3 ^ 2 * e5 * x2 * e1 -
8 * e3 * y2 ^ 3 * y3 ^ 2 * e5 * e2 * y1 -
16 * e3 * y2 ^ 4 * y3 ^ 2 * e6 * x1 * e1 -
8 * e3 * y2 ^ 4 * y3 ^ 2 * e6 * x2 * e1 -
24 * e3 * y2 ^ 3 * y3 ^ 2 * e6 * e2 * y1 +
32 * e3 * y2 ^ 5 * y3 ^ 2 * y1 * x1 * e1 +
16 * e3 * y2 ^ 5 * y3 ^ 2 * y1 * x2 * e1 +
16 * e3 * y2 ^ 4 * y3 ^ 2 * x1 * e1 ^ 2 * x2 +
16 * e3 * y2 ^ 3 * y3 ^ 2 * y1 * x1 * e1 ^ 2 * x2 -
16 * e3 * y2 ^ 2 * y3 ^ 3 * y1 * x1 * e1 * e2 -
8 * e3 * y2 ^ 2 * y3 ^ 3 * y1 * x2 * e1 * e2 +
16 * e3 * y2 ^ 3 * y3 ^ 2 * x1 * e1 * e2 * y1 +
16 * e3 * y2 ^ 3 * y3 ^ 3 * x1 * e1 * e2 +
8 * e3 * y2 ^ 3 * y3 ^ 2 * x2 * e1 * e2 * y1 +
8 * e3 * y2 ^ 3 * y3 ^ 3 * x2 * e1 * e2 - e3 * e6 ^ 3 * e7 ^ 2 +
16 * e3 * e6 * y2 * y3 * y1 ^ 2 * e5 * x1 * e1 +
8 * e3 * e6 * y2 * y3 * y1 ^ 2 * e5 * x2 * e1 -
32 * e3 * e6 ^ 2 * y2 ^ 2 * y3 * y1 * e5 -
8 * e3 * e6 * y2 * y3 ^ 2 * y1 * e5 * e2 +
16 * e3 * e6 ^ 2 * y2 * y3 * y1 ^ 2 * x1 * e1 +
8 * e3 * e6 ^ 2 * y2 * y3 * y1 ^ 2 * x2 * e1 -
8 * e3 * e6 ^ 2 * y2 * y3 ^ 2 * y1 * e2 -
32 * e3 * e6 * y2 ^ 2 * y3 * y1 ^ 3 * x1 * e1 -
16 * e3 * e6 * y2 ^ 2 * y3 * y1 ^ 3 * x2 * e1 +
32 * e3 * e6 * y2 ^ 3 * y3 * y1 ^ 2 * x1 * e1 -
8 * e3 * e6 ^ 2 * y2 * y3 * y1 ^ 2 * e5 +
16 * e3 * e6 * y2 ^ 2 * y3 * y1 ^ 3 * e5 -
16 * e3 * e6 * y2 ^ 2 * y3 * y1 * e5 ^ 2 +
16 * e3 * e6 * y2 ^ 3 * y3 * y1 ^ 2 * e5 -
8 * e3 * e6 * y2 * y3 * y1 ^ 2 * e5 * e2 +
16 * e3 * e6 * y2 ^ 2 * y3 * y1 ^ 3 * e2 -
16 * e3 * e6 * y2 * y3 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
4 * e3 * e6 * y2 * y3 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 +
16 * e3 * e6 * y2 ^ 4 * y3 * e5 * y1 + 16 * e3 * e6 ^ 2 * y2 ^ 4 * y3 * y1 -
4 * e3 * e6 ^ 3 * y2 * y3 * y1 ^ 2 - 16 * e3 * e6 * y2 ^ 3 * y3 * y1 ^ 4 -
16 * e3 * e7 * y2 ^ 3 * y3 * y1 ^ 4 - 4 * e3 * e6 * y2 ^ 3 * y3 * e5 ^ 2 -
16 * e3 * e6 * y2 ^ 5 * y3 * y1 ^ 2 - 4 * e3 * e6 * y2 * y3 ^ 3 * e2 ^ 2 +
8 * e3 * e6 ^ 2 * y2 ^ 2 * y3 ^ 2 * e2 - 4 * e3 * e7 * y2 ^ 3 * y3 * e5 ^ 2 -
4 * e3 * e7 * y2 ^ 3 * y3 * e6 ^ 2 - 16 * e3 * e7 * y2 ^ 5 * y3 * y1 ^ 2 -
4 * e3 * e7 * y2 * y3 ^ 3 * e2 ^ 2 - 16 * e3 * e6 * y2 ^ 3 * y3 * y1 ^ 2 * e2 -
16 * e3 * e6 * y2 ^ 3 * y3 * x1 ^ 2 * e1 ^ 2 +
12 * e3 * e6 * y2 ^ 3 * y3 * x2 ^ 2 * e1 ^ 2 -
8 * e3 * e6 * y2 * y3 ^ 2 * e2 ^ 2 * y1 -
4 * e3 * e6 * y2 * y3 * y1 ^ 2 * e5 ^ 2 +
16 * e3 * e7 * y2 * y3 * y1 ^ 2 * e5 * x1 * e1 +
8 * e3 * e7 * y2 * y3 * y1 ^ 2 * e5 * x2 * e1 -
32 * e3 * e7 * y2 ^ 2 * y3 * y1 * e5 * e6 -
8 * e3 * e7 * y2 * y3 ^ 2 * y1 * e5 * e2 +
16 * e3 * e7 * y2 * y3 * y1 ^ 2 * e6 * x1 * e1 +
8 * e3 * e7 * y2 * y3 * y1 ^ 2 * e6 * x2 * e1 -
8 * e3 * e7 * y2 * y3 ^ 2 * y1 * e6 * e2 -
32 * e3 * e7 * y2 ^ 2 * y3 * y1 ^ 3 * x1 * e1 -
16 * e3 * e7 * y2 ^ 2 * y3 * y1 ^ 3 * x2 * e1 +
32 * e3 * e7 * y2 ^ 3 * y3 * y1 ^ 2 * x1 * e1 +
16 * e3 * e7 * y2 ^ 2 * y3 ^ 2 * y1 ^ 2 * e2 -
8 * e3 * e7 * y2 * y3 * y1 ^ 2 * e5 * e6 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 ^ 3 * e5 -
16 * e3 * e7 * y2 ^ 2 * y3 * y1 * e5 ^ 2 +
16 * e3 * e7 * y2 ^ 3 * y3 * y1 ^ 2 * e5 -
8 * e3 * e7 * y2 * y3 * y1 ^ 2 * e5 * e2 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 ^ 3 * e6 -
16 * e3 * e7 * y2 ^ 2 * y3 * y1 * e6 ^ 2 +
16 * e3 * e7 * y2 ^ 3 * y3 * y1 ^ 2 * e6 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 ^ 3 * e2 -
16 * e3 * e7 * y2 * y3 * y1 ^ 2 * x1 ^ 2 * e1 ^ 2 -
4 * e3 * e7 * y2 * y3 * y1 ^ 2 * x2 ^ 2 * e1 ^ 2 -
8 * e3 * e7 * y2 ^ 3 * y3 * e5 * e6 + 16 * e3 * e7 * y2 ^ 4 * y3 * e5 * y1 +
16 * e3 * e7 * y2 ^ 4 * y3 * e6 * y1 -
16 * e3 * e7 * y2 ^ 3 * y3 * y1 ^ 2 * e2 -
16 * e3 * e7 * y2 ^ 3 * y3 * x1 ^ 2 * e1 ^ 2 -
4 * e3 * e7 * y2 ^ 3 * y3 * x2 ^ 2 * e1 ^ 2 -
8 * e3 * e7 * y2 * y3 ^ 2 * e2 ^ 2 * y1 -
4 * e3 * e7 * y2 * y3 * y1 ^ 2 * e5 ^ 2 -
4 * e3 * e7 * y2 * y3 * y1 ^ 2 * e6 ^ 2 + e1 ^ 3 * x3 ^ 2 * e7 ^ 3 -
4 * e3 * e6 * y2 * y3 * e2 ^ 2 * y1 ^ 2 +
16 * e3 * e6 * y2 ^ 2 * y3 * y1 * e5 * x2 * e1 +
16 * e3 * e6 ^ 2 * y2 ^ 2 * y3 * y1 * x2 * e1 -
16 * e3 * e6 * y2 * y3 * y1 ^ 2 * x1 * e1 ^ 2 * x2 +
24 * e3 * e6 * y2 ^ 2 * y3 * y1 * x1 ^ 2 * e1 ^ 2 +
16 * e3 * e6 * y2 * y3 * y1 ^ 2 * x1 * e1 * e2 +
8 * e3 * e6 * y2 * y3 * y1 ^ 2 * x2 * e1 * e2 +
16 * e3 * e6 * y2 ^ 3 * y3 * e5 * x1 * e1 -
8 * e3 * e6 * y2 ^ 3 * y3 * e5 * x2 * e1 +
8 * e3 * e6 * y2 ^ 2 * y3 * e5 * e2 * y1 +
8 * e3 * e6 * y2 ^ 2 * y3 ^ 2 * e5 * e2 +
16 * e3 * e6 ^ 2 * y2 ^ 3 * y3 * x1 * e1 -
32 * e3 * e6 * y2 ^ 4 * y3 * y1 * x1 * e1 +
16 * e3 * e6 * y2 ^ 4 * y3 * y1 * x2 * e1 +
16 * e3 * e6 * y2 ^ 2 * y3 * y1 * x1 * e1 ^ 2 * x2 +
16 * e3 * e6 * y2 * y3 ^ 2 * y1 * x1 * e1 * e2 +
8 * e3 * e6 * y2 * y3 ^ 2 * y1 * x2 * e1 * e2 -
16 * e3 * e6 * y2 ^ 2 * y3 * x1 * e1 * e2 * y1 -
16 * e3 * e6 * y2 ^ 2 * y3 ^ 2 * x1 * e1 * e2 -
8 * e3 * e6 * y2 ^ 2 * y3 * x2 * e1 * e2 * y1 -
8 * e3 * e6 * y2 ^ 2 * y3 ^ 2 * x2 * e1 * e2 - e1 * y3 ^ 2 * e6 ^ 4 -
4 * e3 * e7 * y2 * y3 * e2 ^ 2 * y1 ^ 2 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 * e5 * x2 * e1 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 * e6 * x2 * e1 -
16 * e3 * e7 * y2 * y3 * y1 ^ 2 * x1 * e1 ^ 2 * x2 +
24 * e3 * e7 * y2 ^ 2 * y3 * y1 * x1 ^ 2 * e1 ^ 2 +
16 * e3 * e7 * y2 * y3 * y1 ^ 2 * x1 * e1 * e2 +
8 * e3 * e7 * y2 * y3 * y1 ^ 2 * x2 * e1 * e2 +
16 * e3 * e7 * y2 ^ 3 * y3 * e5 * x1 * e1 +
8 * e3 * e7 * y2 ^ 3 * y3 * e5 * x2 * e1 +
8 * e3 * e7 * y2 ^ 2 * y3 * e5 * e2 * y1 +
8 * e3 * e7 * y2 ^ 2 * y3 ^ 2 * e5 * e2 +
16 * e3 * e7 * y2 ^ 3 * y3 * e6 * x1 * e1 +
8 * e3 * e7 * y2 ^ 3 * y3 * e6 * x2 * e1 +
8 * e3 * e7 * y2 ^ 2 * y3 ^ 2 * e6 * e2 -
32 * e3 * e7 * y2 ^ 4 * y3 * y1 * x1 * e1 -
16 * e3 * e7 * y2 ^ 4 * y3 * y1 * x2 * e1 -
16 * e3 * e7 * y2 ^ 3 * y3 ^ 2 * y1 * e2 -
16 * e3 * e7 * y2 ^ 3 * y3 * x1 * e1 ^ 2 * x2 +
16 * e3 * e7 * y2 ^ 2 * y3 * y1 * x1 * e1 ^ 2 * x2 +
16 * e3 * e7 * y2 * y3 ^ 2 * y1 * x1 * e1 * e2 +
8 * e3 * e7 * y2 * y3 ^ 2 * y1 * x2 * e1 * e2 -
16 * e3 * e7 * y2 ^ 2 * y3 * x1 * e1 * e2 * y1 -
16 * e3 * e7 * y2 ^ 2 * y3 ^ 2 * x1 * e1 * e2 -
8 * e3 * e7 * y2 ^ 2 * y3 * x2 * e1 * e2 * y1 -
8 * e3 * e7 * y2 ^ 2 * y3 ^ 2 * x2 * e1 * e2 - e6 ^ 3 * x3 ^ 2 * e3 ^ 3 -
16 * e1 * y2 ^ 3 * y3 ^ 2 * e4 * y1 ^ 3 - e6 ^ 3 * e3 ^ 3 * x1 ^ 2 +
2 * e6 ^ 4 * x2 * e3 ^ 2 + 2 * e6 ^ 4 * x3 * e3 ^ 2 +
2 * e6 ^ 4 * e3 ^ 2 * x1 - e5 ^ 3 * x2 ^ 2 * e3 ^ 3 -
e5 ^ 3 * x3 ^ 2 * e3 ^ 3 - e5 ^ 3 * e3 ^ 3 * x1 ^ 2 +
2 * x1 ^ 5 * e1 ^ 3 * e3 ^ 3 - 3 * e3 * e6 ^ 4 * e5 - e3 * e5 ^ 3 * e6 ^ 2 -
3 * e3 * e5 ^ 2 * e6 ^ 3 - e3 * e5 ^ 3 * e7 ^ 2 - e6 ^ 3 * x2 ^ 2 * e3 ^ 3 -
2 * e6 ^ 3 * x2 * e3 ^ 3 * x3 - 2 * e6 ^ 3 * x2 * e3 ^ 3 * x1 -
2 * e6 ^ 3 * x3 * e3 ^ 3 * x1 + 2 * e6 ^ 3 * e7 * x2 * e3 ^ 2 +
2 * e6 ^ 3 * e7 * x3 * e3 ^ 2 + 2 * e6 ^ 3 * e7 * e3 ^ 2 * x1 -
2 * e5 ^ 3 * x2 * e3 ^ 3 * x3 - 2 * e5 ^ 3 * x2 * e3 ^ 3 * x1 -
2 * e5 ^ 3 * x3 * e3 ^ 3 * x1 + 2 * e5 ^ 3 * e6 * x2 * e3 ^ 2 +
6 * e5 ^ 2 * e6 ^ 2 * x2 * e3 ^ 2 + 2 * e5 ^ 3 * e6 * x3 * e3 ^ 2 +
6 * e5 ^ 2 * e6 ^ 2 * x3 * e3 ^ 2 + 2 * e5 ^ 3 * e6 * e3 ^ 2 * x1 +
6 * e5 ^ 2 * e6 ^ 2 * e3 ^ 2 * x1 + 2 * e5 ^ 3 * e7 * x2 * e3 ^ 2 +
2 * e5 ^ 3 * e7 * x3 * e3 ^ 2 + 2 * e5 ^ 3 * e7 * e3 ^ 2 * x1 -
3 * e5 ^ 2 * e6 * x2 ^ 2 * e3 ^ 3 - 3 * e5 * e6 ^ 2 * x2 ^ 2 * e3 ^ 3 -
3 * e5 ^ 2 * e6 * x3 ^ 2 * e3 ^ 3 - 3 * e5 * e6 ^ 2 * x3 ^ 2 * e3 ^ 3 -
3 * e5 ^ 2 * e6 * e3 ^ 3 * x1 ^ 2 - 3 * e5 * e6 ^ 2 * e3 ^ 3 * x1 ^ 2 +
6 * e5 * e6 ^ 3 * x2 * e3 ^ 2 + 6 * e5 * e6 ^ 3 * x3 * e3 ^ 2 +
6 * e5 * e6 ^ 3 * e3 ^ 2 * x1 + 8 * x1 ^ 3 * e1 ^ 2 * e6 ^ 2 * e3 ^ 2 -
8 * e1 ^ 2 * x3 ^ 3 * e6 ^ 2 * e3 ^ 2 + 4 * e5 ^ 2 * x1 ^ 3 * e1 * e3 ^ 3 +
2 * e5 ^ 2 * x2 ^ 3 * e1 * e3 ^ 3 - 5 * x1 ^ 4 * e1 ^ 2 * e3 ^ 3 * e5 -
5 * x1 ^ 4 * e1 ^ 2 * e3 ^ 3 * e6 - x2 ^ 4 * e1 ^ 2 * e3 ^ 3 * e5 -
x2 ^ 4 * e1 ^ 2 * e3 ^ 3 * e6 + 3 * e1 ^ 2 * x3 ^ 4 * e3 ^ 3 * e5 +
3 * e1 ^ 2 * x3 ^ 4 * e3 ^ 3 * e6 + 8 * x1 ^ 2 * e1 ^ 3 * x2 ^ 3 * e3 ^ 3 +
2 * x1 * e1 ^ 3 * x2 ^ 4 * e3 ^ 3 + 8 * x1 ^ 4 * e1 ^ 3 * x2 * e3 ^ 3 +
12 * x1 ^ 3 * e1 ^ 3 * x2 ^ 2 * e3 ^ 3 +
4 * x1 ^ 3 * e1 ^ 3 * x3 ^ 2 * e3 ^ 3 + 6 * x1 ^ 4 * e1 ^ 3 * x3 * e3 ^ 3 -
3 * x1 ^ 4 * e1 ^ 3 * e6 * e3 ^ 2 - 3 * x1 ^ 4 * e1 ^ 3 * e7 * e3 ^ 2 -
8 * x2 ^ 3 * e1 ^ 3 * x3 ^ 2 * e3 ^ 3 - 2 * x2 ^ 4 * e1 ^ 3 * e3 ^ 3 * x3 +
x2 ^ 4 * e1 ^ 3 * e6 * e3 ^ 2 + x2 ^ 4 * e1 ^ 3 * e7 * e3 ^ 2 -
12 * e1 ^ 3 * x3 ^ 3 * x2 ^ 2 * e3 ^ 3 -
4 * e1 ^ 3 * x3 ^ 3 * e3 ^ 3 * x1 ^ 2 + 2 * e6 ^ 2 * x2 ^ 3 * e3 ^ 3 * e1 +
4 * e6 ^ 2 * e3 ^ 3 * x1 ^ 3 * e1 - 3 * e6 ^ 3 * x2 ^ 2 * e3 ^ 2 * e1 -
7 * e6 ^ 3 * e3 ^ 2 * x1 ^ 2 * e1 - 6 * e1 ^ 3 * x3 ^ 4 * e3 ^ 3 * x1 -
8 * e1 ^ 3 * x3 ^ 4 * e3 ^ 3 * x2 + e6 ^ 3 * e1 * x3 ^ 2 * e3 ^ 2 -
6 * e3 * e6 ^ 3 * e7 * e5 - 4 * e3 * e6 ^ 3 * y2 ^ 2 * y3 ^ 2 +
4 * e3 * e6 ^ 4 * y2 * y3 - 2 * e3 * e5 ^ 3 * e6 * e7 -
6 * e3 * e5 ^ 2 * e6 ^ 2 * e7 - 4 * e3 * e5 ^ 3 * y2 ^ 2 * y3 ^ 2 -
3 * e3 * e5 ^ 2 * e6 * e7 ^ 2 - 3 * e3 * e5 * e6 ^ 2 * e7 ^ 2 - e3 * e6 ^ 5 +
12 * e6 ^ 2 * x2 * e3 ^ 3 * x3 * x1 * e1 +
4 * e6 ^ 2 * x2 ^ 2 * e3 ^ 3 * x3 * e1 +
10 * e6 ^ 2 * x2 * e3 ^ 3 * x1 ^ 2 * e1 +
8 * e6 ^ 2 * x2 ^ 2 * e3 ^ 3 * x1 * e1 - 4 * e6 ^ 3 * y2 * y3 * x2 * e3 ^ 2 -
4 * e6 ^ 3 * y2 * y3 * x3 * e3 ^ 2 - 4 * e6 ^ 3 * y2 * y3 * e3 ^ 2 * x1 +
8 * x1 * e1 ^ 2 * x2 ^ 2 * e6 ^ 2 * e3 ^ 2 +
16 * x1 ^ 2 * e1 ^ 2 * x2 * e6 ^ 2 * e3 ^ 2 -
4 * e5 ^ 3 * y2 * y3 * x2 * e3 ^ 2 - 4 * e5 ^ 3 * y2 * y3 * x3 * e3 ^ 2 -
4 * e5 ^ 3 * y2 * y3 * e3 ^ 2 * x1 +
8 * x1 ^ 2 * e1 ^ 2 * e6 ^ 2 * x3 * e3 ^ 2 -
8 * x2 ^ 2 * e1 ^ 2 * e6 ^ 2 * x3 * e3 ^ 2 -
16 * e1 ^ 2 * x3 ^ 2 * e6 ^ 2 * x2 * e3 ^ 2 -
6 * e6 ^ 2 * x2 * e3 ^ 3 * x3 * e5 - 6 * e6 ^ 2 * x2 * e3 ^ 3 * x1 * e5 -
6 * e6 ^ 2 * x3 * e3 ^ 3 * x1 * e5 + 6 * e6 ^ 2 * e7 * x2 * e3 ^ 2 * e5 +
6 * e6 ^ 2 * e7 * x3 * e3 ^ 2 * e5 + 6 * e6 ^ 2 * e7 * e3 ^ 2 * x1 * e5 -
8 * x1 * e1 ^ 2 * x2 ^ 3 * e3 ^ 3 * e5 -
8 * x1 * e1 ^ 2 * x2 ^ 3 * e3 ^ 3 * e6 -
16 * x1 ^ 3 * e1 ^ 2 * x2 * e3 ^ 3 * e5 -
16 * x1 ^ 3 * e1 ^ 2 * x2 * e3 ^ 3 * e6 -
18 * x1 ^ 2 * e1 ^ 2 * x2 ^ 2 * e3 ^ 3 * e5 -
18 * x1 ^ 2 * e1 ^ 2 * x2 ^ 2 * e3 ^ 3 * e6 -
6 * e5 ^ 2 * x2 * e3 ^ 3 * x3 * e6 - 6 * e5 ^ 2 * x2 * e3 ^ 3 * x1 * e6 -
6 * e5 ^ 2 * x3 * e3 ^ 3 * x1 * e6 + 6 * e5 ^ 2 * e7 * x2 * e3 ^ 2 * e6 +
6 * e5 ^ 2 * e7 * x3 * e3 ^ 2 * e6 + 6 * e5 ^ 2 * e7 * e3 ^ 2 * x1 * e6 -
6 * x1 ^ 2 * e1 ^ 2 * x3 ^ 2 * e3 ^ 3 * e5 -
6 * x1 ^ 2 * e1 ^ 2 * x3 ^ 2 * e3 ^ 3 * e6 -
12 * x1 ^ 3 * e1 ^ 2 * x3 * e3 ^ 3 * e5 -
12 * x1 ^ 3 * e1 ^ 2 * x3 * e3 ^ 3 * e6 +
8 * x1 ^ 3 * e1 ^ 2 * e6 * e3 ^ 2 * e5 +
8 * x1 ^ 3 * e1 ^ 2 * e7 * e3 ^ 2 * e5 +
8 * x1 ^ 3 * e1 ^ 2 * e7 * e3 ^ 2 * e6 +
6 * x2 ^ 2 * e1 ^ 2 * x3 ^ 2 * e3 ^ 3 * e5 +
6 * x2 ^ 2 * e1 ^ 2 * x3 ^ 2 * e3 ^ 3 * e6 +
8 * e1 ^ 2 * x3 ^ 3 * x2 * e3 ^ 3 * e5 +
8 * e1 ^ 2 * x3 ^ 3 * x2 * e3 ^ 3 * e6 +
4 * e1 ^ 2 * x3 ^ 3 * e3 ^ 3 * x1 * e5 +
4 * e1 ^ 2 * x3 ^ 3 * e3 ^ 3 * x1 * e6 -
12 * e6 ^ 2 * y2 * y3 * x2 * e3 ^ 2 * e5 -
12 * e6 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e5 -
12 * e6 ^ 2 * y2 * y3 * e3 ^ 2 * x1 * e5 -
32 * x1 * e1 ^ 2 * x2 ^ 2 * y2 * y3 * e3 ^ 2 * e5 -
32 * x1 * e1 ^ 2 * x2 ^ 2 * y2 * y3 * e3 ^ 2 * e6 -
16 * x1 * e1 ^ 2 * x2 * y2 * y3 * x3 * e3 ^ 2 * e5 -
16 * x1 * e1 ^ 2 * x2 * y2 * y3 * x3 * e3 ^ 2 * e6 -
32 * x1 ^ 2 * e1 ^ 2 * x2 * y2 * y3 * e3 ^ 2 * e5 -
32 * x1 ^ 2 * e1 ^ 2 * x2 * y2 * y3 * e3 ^ 2 * e6 -
12 * x1 * e1 ^ 2 * x2 ^ 2 * e3 ^ 3 * x3 * e5 -
12 * x1 * e1 ^ 2 * x2 ^ 2 * e3 ^ 3 * x3 * e6 -
24 * x1 ^ 2 * e1 ^ 2 * x2 * x3 * e3 ^ 3 * e5 -
24 * x1 ^ 2 * e1 ^ 2 * x2 * x3 * e3 ^ 3 * e6 +
8 * x1 * e1 ^ 2 * x2 ^ 2 * e6 * e3 ^ 2 * e5 +
16 * x1 ^ 2 * e1 ^ 2 * x2 * e6 * e3 ^ 2 * e5 +
8 * x1 * e1 ^ 2 * x2 ^ 2 * e7 * e3 ^ 2 * e5 +
8 * x1 * e1 ^ 2 * x2 ^ 2 * e7 * e3 ^ 2 * e6 +
16 * x1 ^ 2 * e1 ^ 2 * x2 * e7 * e3 ^ 2 * e5 +
16 * x1 ^ 2 * e1 ^ 2 * x2 * e7 * e3 ^ 2 * e6 -
12 * e5 ^ 2 * y2 * y3 * x2 * e3 ^ 2 * e6 -
12 * e5 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e6 -
12 * e5 ^ 2 * y2 * y3 * e3 ^ 2 * x1 * e6 -
16 * x1 ^ 2 * e1 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e5 -
16 * x1 ^ 2 * e1 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e6 -
16 * x1 ^ 3 * e1 ^ 2 * y2 * y3 * e3 ^ 2 * e5 -
16 * x1 ^ 3 * e1 ^ 2 * y2 * y3 * e3 ^ 2 * e6 +
8 * x1 ^ 2 * e1 ^ 2 * e6 * x3 * e3 ^ 2 * e5 +
8 * x1 ^ 2 * e1 ^ 2 * e7 * x3 * e3 ^ 2 * e5 +
8 * x1 ^ 2 * e1 ^ 2 * e7 * x3 * e3 ^ 2 * e6 -
16 * x2 ^ 3 * e1 ^ 2 * y2 * y3 * e3 ^ 2 * e5 -
16 * x2 ^ 3 * e1 ^ 2 * y2 * y3 * e3 ^ 2 * e6 -
16 * x2 ^ 2 * e1 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e5 -
16 * x2 ^ 2 * e1 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * e6 -
8 * x2 ^ 2 * e1 ^ 2 * e6 * x3 * e3 ^ 2 * e5 -
8 * x2 ^ 2 * e1 ^ 2 * e7 * x3 * e3 ^ 2 * e5 -
8 * x2 ^ 2 * e1 ^ 2 * e7 * x3 * e3 ^ 2 * e6 +
12 * e1 ^ 2 * x3 ^ 2 * y2 * y3 * x2 * e3 ^ 2 * e5 +
12 * e1 ^ 2 * x3 ^ 2 * y2 * y3 * x2 * e3 ^ 2 * e6 +
12 * e1 ^ 2 * x3 ^ 3 * y2 * y3 * e3 ^ 2 * e5 +
12 * e1 ^ 2 * x3 ^ 3 * y2 * y3 * e3 ^ 2 * e6 +
12 * e1 ^ 2 * x3 ^ 2 * y2 * y3 * e3 ^ 2 * x1 * e5 +
12 * e1 ^ 2 * x3 ^ 2 * y2 * y3 * e3 ^ 2 * x1 * e6 -
16 * e1 ^ 2 * x3 ^ 2 * e6 * x2 * e3 ^ 2 * e5 -
8 * e1 ^ 2 * x3 ^ 3 * e6 * e3 ^ 2 * e5 -
8 * e1 ^ 2 * x3 ^ 3 * e7 * e3 ^ 2 * e5 -
8 * e1 ^ 2 * x3 ^ 3 * e7 * e3 ^ 2 * e6 + 8 * e5 * x1 ^ 3 * e1 * e3 ^ 3 * e6 +
4 * e5 * x2 ^ 3 * e1 * e3 ^ 3 * e6 -
8 * e1 ^ 2 * x3 ^ 2 * e6 ^ 2 * e3 ^ 2 * x1 +
8 * e6 ^ 2 * x3 * e3 ^ 3 * x1 ^ 2 * e1 -
10 * e6 ^ 2 * e7 * x2 * e3 ^ 2 * x1 * e1 -
3 * e6 ^ 2 * e7 * x2 ^ 2 * e3 ^ 2 * e1 -
6 * e6 ^ 2 * e7 * x3 * e3 ^ 2 * x1 * e1 -
2 * e6 ^ 2 * e7 * x3 * e3 ^ 2 * x2 * e1 -
7 * e6 ^ 2 * e7 * e3 ^ 2 * x1 ^ 2 * e1 +
12 * e5 ^ 2 * x2 * e3 ^ 3 * x3 * x1 * e1 +
4 * e5 ^ 2 * x2 ^ 2 * e3 ^ 3 * x3 * e1 +
10 * e5 ^ 2 * x2 * e3 ^ 3 * x1 ^ 2 * e1 +
8 * e5 ^ 2 * x2 ^ 2 * e3 ^ 3 * x1 * e1 +
8 * e5 ^ 2 * x3 * e3 ^ 3 * x1 ^ 2 * e1 -
10 * e5 ^ 2 * e6 * x2 * e3 ^ 2 * x1 * e1 -
3 * e5 ^ 2 * e6 * x2 ^ 2 * e3 ^ 2 * e1 -
6 * e5 ^ 2 * e6 * x3 * e3 ^ 2 * x1 * e1 -
2 * e5 ^ 2 * e6 * x3 * e3 ^ 2 * x2 * e1 -
7 * e5 ^ 2 * e6 * e3 ^ 2 * x1 ^ 2 * e1 -
10 * e5 ^ 2 * e7 * x2 * e3 ^ 2 * x1 * e1 -
3 * e5 ^ 2 * e7 * x2 ^ 2 * e3 ^ 2 * e1 -
6 * e5 ^ 2 * e7 * x3 * e3 ^ 2 * x1 * e1 -
2 * e5 ^ 2 * e7 * x3 * e3 ^ 2 * x2 * e1 -
7 * e5 ^ 2 * e7 * e3 ^ 2 * x1 ^ 2 * e1 +
16 * e5 * e6 * x2 ^ 2 * e3 ^ 3 * x1 * e1 +
8 * e5 * e6 * x3 ^ 2 * e3 ^ 3 * x1 * e1 +
4 * e5 * e6 * x3 ^ 2 * e3 ^ 3 * x2 * e1 +
20 * e5 * e6 * e3 ^ 3 * x1 ^ 2 * x2 * e1 -
20 * e5 * e6 ^ 2 * x2 * e3 ^ 2 * x1 * e1 -
6 * e5 * e6 ^ 2 * x2 ^ 2 * e3 ^ 2 * e1 -
12 * e5 * e6 ^ 2 * x3 * e3 ^ 2 * x1 * e1 -
4 * e5 * e6 ^ 2 * x3 * e3 ^ 2 * x2 * e1 -
14 * e5 * e6 ^ 2 * e3 ^ 2 * x1 ^ 2 * e1 +
16 * x1 ^ 3 * e1 ^ 3 * x3 * e3 ^ 3 * x2 -
8 * x1 ^ 3 * e1 ^ 3 * e6 * e3 ^ 2 * x2 -
8 * x1 ^ 3 * e1 ^ 3 * e7 * e3 ^ 2 * x2 -
12 * x2 ^ 2 * e1 ^ 3 * x3 ^ 2 * e3 ^ 3 * x1 -
16 * e1 ^ 2 * x3 ^ 3 * x2 * e3 ^ 3 * y1 * y2 -
16 * e1 ^ 3 * x3 ^ 3 * x2 * e3 ^ 3 * x1 -
8 * e1 ^ 2 * x3 ^ 3 * e3 ^ 3 * x1 * y1 * y2 +
20 * e6 ^ 2 * y2 * y3 * x2 * e3 ^ 2 * x1 * e1 +
14 * e6 ^ 2 * y2 * y3 * x2 ^ 2 * e3 ^ 2 * e1 +
12 * e6 ^ 2 * y2 * y3 * x3 * e3 ^ 2 * x1 * e1 +
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.37 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
