Butterfly
Geogebra sheet
Coq statement
Lemma butterfly: forall E O A B C D F G:point,
X E = 0 -> Y E = 0 -> Y O = 0 -> X F = 0 -> X G = 0 ->
equaldistance B O O A -> collinear A E C ->
equaldistance C O O A -> collinear B E D ->
equaldistance D O O A -> collinear A D F ->
collinear B C G ->
middle F G E
\/ (X A)^2+(Y A)^2 = 0 \/ Y A = 0 \/ (X B)^2+(Y B)^2 = 0
\/ Y B = 0 \/ X D = X A \/ X C = X B \/ Y C = Y A \/ Y D = Y B
\/ X O = 0 \/ (X A)^2 = 0.
Proof.
geo_begin.
tzRpv 0%Z (X O::X A::Y A::Y B::nil) (@nil R).
tzRpv 0%Z (X O::X A::Y A::Y B::nil) (@nil R).
Qed.
Algebraic version
First goal
p:= 0
F:= [
(1) *k^2 + ((-2)*u1) *k + ((-1)*u2^2+2*u1*u2+(-1)*u3^2+u4^2) ;
(1) *i^2 + (1) *j^2 + ((-2)*u1) *j + ((-1)*u2^2+2*u1*u2+(-1)*u3^2) ;
(1) *g^2 + (1) *h^2 + ((-2)*u1) *h + ((-1)*u2^2+2*u1*u2+(-1)*u3^2) ;
(u2) *i + ((-1)*u3) *j ;
(1) *g*k + ((-1)*u4) *h ;
((-1)) *f*h + (u2) *f + ((-1)*u2) *g + (u3) *h ;
((-1)) *e*j + (1) *e*k + ((-1)) *i*k + (u4) *j ;
];
Second goal
p:= (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4) *e*g*h*i*j*k^2 + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4) *f*g*h*i*j*k^2 + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4) *e*g*h*i*k^3 + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4) *f*g*h*i*k^3 + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4) *e*g*h*j*k^2 + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4) *f*g*h*j*k^2 + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4) *e*g*i*j*k^2 + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4) *f*g*i*j*k^2 + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^2) *e*h*i*j*k^2 + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^2) *f*h*i*j*k^2 + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4) *e*g*h*k^3 + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4) *f*g*h*k^3 + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4) *e*g*i*k^3 + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4) *f*g*i*k^3 + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^2) *e*h*i*k^3 + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^2) *f*h*i*k^3 + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^3) *e*g*h*i*j + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^3) *f*g*h*i*j + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^3) *e*g*h*i*k + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^3) *f*g*h*i*k + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4) *e*g*j*k^2 + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4) *f*g*j*k^2 + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^2) *e*h*j*k^2 + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^2) *f*h*j*k^2 + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^2) *e*i*j*k^2 + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^2) *f*i*j*k^2 + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4) *e*g*k^3 + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4) *f*g*k^3 + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^2) *e*h*k^3 + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^2) *f*h*k^3 + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^2) *e*i*k^3 + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^2) *f*i*k^3 + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^3) *e*g*h*j + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^3) *f*g*h*j + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^3) *e*g*i*j + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^3) *f*g*i*j + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^4) *e*h*i*j + ((u1*u2^2*u3^3+u1*u2^4*u3)*u4^4) *f*h*i*j + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^3) *e*g*h*k + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^3) *f*g*h*k + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^3) *e*g*i*k + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^3) *f*g*i*k + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^4) *e*h*i*k + (((-1)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3)*u4^4) *f*h*i*k + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^2) *e*j*k^2 + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^2) *f*j*k^2 + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^2) *e*k^3 + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^2) *f*k^3 + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^3) *e*g*j + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^3) *f*g*j + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^4) *e*h*j + (((-1)*u1*u2^2*u3^4+(-1)*u1*u2^4*u3^2)*u4^4) *f*h*j + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^4) *e*i*j + (((-1)*u1*u2^3*u3^3+(-1)*u1*u2^5*u3)*u4^4) *f*i*j + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^3) *e*g*k + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^3) *f*g*k + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^4) *e*h*k + ((u1*u2^2*u3^4+u1*u2^4*u3^2)*u4^4) *f*h*k + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^4) *e*i*k + ((u1*u2^3*u3^3+u1*u2^5*u3)*u4^4) *f*i*k + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^4) *e*j + ((u1*u2^3*u3^4+u1*u2^5*u3^2)*u4^4) *f*j + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^4) *e*k + (((-1)*u1*u2^3*u3^4+(-1)*u1*u2^5*u3^2)*u4^4) *f*k
F:= [
(1) *k^2 + ((-2)*u1) *k + ((-1)*u2^2+2*u1*u2+(-1)*u3^2+u4^2) ;
(1) *i^2 + (1) *j^2 + ((-2)*u1) *j + ((-1)*u2^2+2*u1*u2+(-1)*u3^2) ;
(1) *g^2 + (1) *h^2 + ((-2)*u1) *h + ((-1)*u2^2+2*u1*u2+(-1)*u3^2) ;
(u2) *i + ((-1)*u3) *j ;
(1) *g*k + ((-1)*u4) *h ;
((-1)) *f*h + (u2) *f + ((-1)*u2) *g + (u3) *h ;
((-1)) *e*j + (1) *e*k + ((-1)) *i*k + (u4) *j ;
];
Certificates
First certificate
CR:=[
0; 0; 0; 0; 0; 0; 0; ];
C:=[
[
0; 0; 0; 0; 0; 0; 0; ];
];
c:=
1;
Second certificate
CR:=[
((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2) *e + ((u2^2+2*u1*u2)*u3^5+u2^4*u3^3+2*u1*u2*u3^4*u4) *j + (((-1)*u2^3+(-2)*u1*u2^2)*u3^5+(-1)*u2^5*u3^3+2*u1*u2^4*u3^2*u4) ; (2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2) *e + (((-1)*u2^2+(-2)*u1*u2)*u3^7+((-2)*u2^4+4*u1^2*u2^2)*u3^5+((-1)*u2^6+2*u1*u2^5)*u3^3+4*u1^2*u2^2*u3^3*u4^2+((-2)*u1*u2*u3^6+8*u1^2*u2^2*u3^4+2*u1*u2^5*u3^2)*u4) *j + ((u2^3+2*u1*u2^2)*u3^7+(2*u2^5+(-4)*u1^2*u2^3)*u3^5+(u2^7+(-2)*u1*u2^6)*u3^3+(-4)*u1^2*u2^3*u3^3*u4^2+(((-4)*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+((-4)*u1*u2^6+4*u1^2*u2^5)*u3^2)*u4) ; (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4) *e + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4^2) ; ((-4)*u1^2*u3^3*u4^3+((-2)*u1*u2*u3^4+((-2)*u1*u2^3+8*u1^2*u2^2)*u3^2)*u4^2+((-2)*u1*u2*u3^5+((-2)*u1*u2^3+4*u1^2*u2^2)*u3^3)*u4) *g*h + ((-4)*u1^2*u2*u3^2*u4^3+(2*u1*u3^5+(2*u1*u2^2+(-8)*u1^2*u2)*u3^3)*u4^2+((-2)*u1*u2^2*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4) *h^2 + (4*u1^2*u2*u3^2*u4^3+((-2)*u1*u3^5+((-2)*u1*u2^2+4*u1^2*u2)*u3^3)*u4^2) *h*k + (4*u1^2*u3^3*u4^4+(2*u1*u2*u3^4+(2*u1*u2^3+(-4)*u1^2*u2^2)*u3^2)*u4^3+((-4)*u1^2*u3^5+((-4)*u1^2*u2^2+8*u1^3*u2)*u3^3)*u4^2+(4*u1^2*u2^2*u3^4+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4) *h + ((-4)*u1^2*u2^2*u3^2*u4^3+((4*u1^2+2*u1*u2)*u3^5+2*u1*u2^3*u3^3)*u4^2) *k + ((-4)*u1^2*u2*u3^3*u4^4+((-2)*u1*u2^2*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4^3+(4*u1^2*u2*u3^5+(4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3)*u4^2+(2*u1*u2^2*u3^6+(4*u1*u2^4+(-8)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-8)*u1^2*u2^5+8*u1^3*u2^4)*u3^2)*u4) ; ((4*u1^2*u3^5+4*u1^2*u2^2*u3^3)*u4^2) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *e + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+((-4)*u1^2*u2*u3^5+(-4)*u1^2*u2^3*u3^3)*u4^2) *j ; ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4) *g*h*j + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*j + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h*j*k + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^3+(((-2)*u1*u2^2+(-4)*u1^2*u2)*u3^6+((-4)*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4) *g*h + ((((-4)*u1^2*u2^2+(-8)*u1^3*u2)*u3^4+((-4)*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h^2 + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5)*u3^2)*u4) *g*j + (((-2)*u1*u2*u3^6+(-4)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *h*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^3+((2*u1*u2^3+4*u1^2*u2^2)*u3^6+(4*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-8)*u1^3*u2^5)*u3^2)*u4) *g + ((2*u1*u2^2*u3^6+(4*u1*u2^4+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4^2) *h + ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2)*u4^2) *j + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *k + (((-2)*u1*u2^3*u3^6+((-4)*u1*u2^5+4*u1^2*u2^4)*u3^4+((-2)*u1*u2^7+4*u1^2*u2^6)*u3^2)*u4^2) ; ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4) *g*j^2 + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *j^2*k + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^3+(((-2)*u1*u2^2+(-4)*u1^2*u2)*u3^6+((-4)*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4) *g*j + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+(-8)*u1^3*u2)*u3^4+((-2)*u1*u2^5+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h*j + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^4+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^2)*u4^2) *j^2 + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^3+(4*u1^2*u2^2*u3^6+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3^2)*u4) *g + ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3^2)*u4^2) *h + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^4+((2*u1*u2^2+4*u1^2*u2)*u3^6+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4^2) *j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *k + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^4+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4^2) ; (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4) *e*h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4) *f*h*j^2 + (((4*u1^2*u2^2+8*u1^3*u2)*u3^4+(4*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4) *e*h*j + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4) *f*h*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4) *e*j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4) *f*j^2 + ((2*u1*u3^7+(4*u1*u2^2+(-4)*u1^2*u2)*u3^5+(2*u1*u2^4+(-4)*u1^2*u2^3)*u3^3)*u4) *h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+(4*u1^2*u2*u3^6+(8*u1^2*u2^3+(-16)*u1^3*u2^2)*u3^4+(4*u1^2*u2^5+(-16)*u1^3*u2^4)*u3^2)*u4) *e*h + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4) *f*h + ((((-4)*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-4)*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4) *e*j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4) *f*j + ((4*u1^2*u3^5+4*u1^2*u2^2*u3^3)*u4^3+(((-4)*u1^2+(-2)*u1*u2)*u3^7+((-4)*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^5+((-2)*u1*u2^5+8*u1^3*u2^3)*u3^3)*u4) *h*j + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^2+((-2)*u1*u2*u3^7+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^5+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^3)*u4) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^3+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+16*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+16*u1^3*u2^5)*u3^2)*u4) *e + ((2*u1*u2^3*u3^6+(4*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4) *f + (((-4)*u1^2*u2*u3^5+(-4)*u1^2*u2^3*u3^3)*u4^3+(2*u1*u2^2*u3^6+(4*u1*u2^4+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4^2+((2*u1*u2^2+4*u1^2*u2)*u3^7+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^5+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^3)*u4) *j + (((-2)*u1*u2^3*u3^6+((-4)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+((-2)*u1*u2^7+4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3^2)*u4^2) ; (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4) *e*g*h*j*k + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4) *f*g*h*j*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4)*u3)*u4) *e*g*h*j + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4)*u3)*u4) *f*g*h*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3)*u4) *e*g*h*k + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3)*u4) *f*g*h*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *e*g*j*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *f*g*j*k + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^2) *e*h*j*k + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^2) *f*h*j*k + ((2*u1*u3^6+(4*u1*u2^2+(-4)*u1^2*u2)*u3^4+(2*u1*u2^4+(-4)*u1^2*u2^3)*u3^2)*u4) *g*h*j*k + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^2) *h^2*j*k + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4^3+(4*u1^2*u2*u3^5+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *e*g*h + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4^3+(4*u1^2*u2*u3^5+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *f*g*h + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3)*u4) *e*g*j + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3)*u4) *f*g*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3)*u4^2) *e*h*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3)*u4^2) *f*h*j + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *e*g*k + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *f*g*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2+(-8)*u1^3*u2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3)*u4^2) *e*h*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2+(-8)*u1^3*u2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3)*u4^2) *f*h*k + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^3+(((-4)*u1^2+(-2)*u1*u2)*u3^6+((-4)*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^4+((-2)*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4) *g*h*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h^2*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *e*j*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *f*j*k + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^4+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^2)*u4) *g*j*k + (((-2)*u1*u3^6+((-8)*u1^3+(-4)*u1*u2^2)*u3^4+((-2)*u1*u2^4+(-8)*u1^3*u2^2)*u3^2)*u4^2) *h*j*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4^3+((-4)*u1^2*u2^2*u3^5+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^3+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3)*u4) *e*g + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4^3+((-4)*u1^2*u2^2*u3^5+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^3+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3)*u4) *f*g + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^4+((-4)*u1^2*u2*u3^5+((-8)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *e*h + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^4+((-4)*u1^2*u2*u3^5+((-8)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *f*h + (((-4)*u1^2*u3^4+(-4)*u1^2*u2^2*u3^2)*u4^4+(4*u1^2*u3^6+(8*u1^2*u2^2+(-8)*u1^3*u2)*u3^4+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h^2 + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5)*u3)*u4^2) *e*j + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5)*u3)*u4^2) *f*j + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^4+((-4)*u1^2*u3^6+((-8)*u1^2*u2^2+8*u1^3*u2)*u3^4+((-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4^2) *h*j + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *e*k + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *f*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+((2*u1*u2^2+4*u1^2*u2)*u3^6+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4) *g*k + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4^2) *h*k + ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^4+(4*u1^2*u2^2*u3^5+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3)*u4^2) *e + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^4+(4*u1^2*u2^2*u3^5+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3)*u4^2) *f + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^4+(4*u1^2*u2*u3^6+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *k + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^4+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4^2) ; ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2)*u4) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^3+(((-2)*u1*u2^3+(-4)*u1^2*u2^2)*u3^6+((-4)*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-2)*u1*u2^7+8*u1^3*u2^5)*u3^2)*u4) *j + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^3+(4*u1^2*u2^3*u3^6+(8*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^4+(4*u1^2*u2^7+(-8)*u1^3*u2^6)*u3^2)*u4) ; 0; (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4) *e*g*h*i*j + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4) *f*g*h*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4) *e*g*h*i*k + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4) *f*g*h*i*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *e*g*h*i + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *f*g*h*i + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4) *e*g*h*j + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4) *f*g*h*j + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4) *e*g*i*j + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4) *f*g*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4^2) *e*h*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4^2) *f*h*i*j + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4) *e*g*h*k + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4) *f*g*h*k + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4) *e*g*i*k + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4) *f*g*i*k + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4^2) *e*h*i*k + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4^2) *f*h*i*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4) *e*g*h + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4) *f*g*h + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *e*h^2 + (((-4)*u1^2*u2^3*u3^3+(-4)*u1^2*u2^5*u3)*u4) *e*g*i + (((-4)*u1^2*u2^3*u3^3+(-4)*u1^2*u2^5*u3)*u4) *f*g*i + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *e*h*i + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *f*h*i + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*i + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4) *e*g*j + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4) *f*g*j + ((((-2)*u1*u2^2+4*u1^2*u2)*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4^2) *e*h*j + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4^2) *f*h*j + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4^2) *e*i*j + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4^2) *f*i*j + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h*i*j + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4) *e*g*k + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4) *f*g*k + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4^2) *e*h*k + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4^2) *f*h*k + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4^2) *e*i*k + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4^2) *f*i*k + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4) *e*g + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4) *f*g + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *e*h + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *f*h + ((4*u1^2*u2^3*u3^3+4*u1^2*u2^5*u3)*u4^2) *e*i + ((4*u1^2*u2^3*u3^3+4*u1^2*u2^5*u3)*u4^2) *f*i + (((2*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4^2) *e*j + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4^2) *f*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *i*j + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *e*k + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *f*k + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *f + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *i + ((4*u1^2*u2^2*u3^5+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3)*u4^2+((2*u1*u2^3+4*u1^2*u2^2)*u3^6+(4*u1*u2^5+(-8)*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-4)*u1^2*u2^6)*u3^2)*u4) *j + (((-4)*u1^2*u2^3*u3^5+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3^3)*u4^2+(((-2)*u1*u2^4+(-4)*u1^2*u2^3)*u3^6+((-4)*u1*u2^6+8*u1^3*u2^4)*u3^4+((-2)*u1*u2^8+4*u1^2*u2^7)*u3^2)*u4) ; ];
C:=[
[
((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2) *e + ((u2^2+2*u1*u2)*u3^5+u2^4*u3^3+2*u1*u2*u3^4*u4) *j + (((-1)*u2^3+(-2)*u1*u2^2)*u3^5+(-1)*u2^5*u3^3+2*u1*u2^4*u3^2*u4) ; (2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2) *e + (((-1)*u2^2+(-2)*u1*u2)*u3^7+((-2)*u2^4+4*u1^2*u2^2)*u3^5+((-1)*u2^6+2*u1*u2^5)*u3^3+4*u1^2*u2^2*u3^3*u4^2+((-2)*u1*u2*u3^6+8*u1^2*u2^2*u3^4+2*u1*u2^5*u3^2)*u4) *j + ((u2^3+2*u1*u2^2)*u3^7+(2*u2^5+(-4)*u1^2*u2^3)*u3^5+(u2^7+(-2)*u1*u2^6)*u3^3+(-4)*u1^2*u2^3*u3^3*u4^2+(((-4)*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+((-4)*u1*u2^6+4*u1^2*u2^5)*u3^2)*u4) ; (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4) *e + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4^2) ; ((-4)*u1^2*u3^3*u4^3+((-2)*u1*u2*u3^4+((-2)*u1*u2^3+8*u1^2*u2^2)*u3^2)*u4^2+((-2)*u1*u2*u3^5+((-2)*u1*u2^3+4*u1^2*u2^2)*u3^3)*u4) *g*h + ((-4)*u1^2*u2*u3^2*u4^3+(2*u1*u3^5+(2*u1*u2^2+(-8)*u1^2*u2)*u3^3)*u4^2+((-2)*u1*u2^2*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4) *h^2 + (4*u1^2*u2*u3^2*u4^3+((-2)*u1*u3^5+((-2)*u1*u2^2+4*u1^2*u2)*u3^3)*u4^2) *h*k + (4*u1^2*u3^3*u4^4+(2*u1*u2*u3^4+(2*u1*u2^3+(-4)*u1^2*u2^2)*u3^2)*u4^3+((-4)*u1^2*u3^5+((-4)*u1^2*u2^2+8*u1^3*u2)*u3^3)*u4^2+(4*u1^2*u2^2*u3^4+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4) *h + ((-4)*u1^2*u2^2*u3^2*u4^3+((4*u1^2+2*u1*u2)*u3^5+2*u1*u2^3*u3^3)*u4^2) *k + ((-4)*u1^2*u2*u3^3*u4^4+((-2)*u1*u2^2*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4^3+(4*u1^2*u2*u3^5+(4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3)*u4^2+(2*u1*u2^2*u3^6+(4*u1*u2^4+(-8)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-8)*u1^2*u2^5+8*u1^3*u2^4)*u3^2)*u4) ; ((4*u1^2*u3^5+4*u1^2*u2^2*u3^3)*u4^2) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *e + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+((-4)*u1^2*u2*u3^5+(-4)*u1^2*u2^3*u3^3)*u4^2) *j ; ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4) *g*h*j + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*j + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h*j*k + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^3+(((-2)*u1*u2^2+(-4)*u1^2*u2)*u3^6+((-4)*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4) *g*h + ((((-4)*u1^2*u2^2+(-8)*u1^3*u2)*u3^4+((-4)*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h^2 + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5)*u3^2)*u4) *g*j + (((-2)*u1*u2*u3^6+(-4)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *h*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^3+((2*u1*u2^3+4*u1^2*u2^2)*u3^6+(4*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-8)*u1^3*u2^5)*u3^2)*u4) *g + ((2*u1*u2^2*u3^6+(4*u1*u2^4+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4^2) *h + ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2)*u4^2) *j + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *k + (((-2)*u1*u2^3*u3^6+((-4)*u1*u2^5+4*u1^2*u2^4)*u3^4+((-2)*u1*u2^7+4*u1^2*u2^6)*u3^2)*u4^2) ; ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4) *g*j^2 + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *j^2*k + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^3+(((-2)*u1*u2^2+(-4)*u1^2*u2)*u3^6+((-4)*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4) *g*j + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+(-8)*u1^3*u2)*u3^4+((-2)*u1*u2^5+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h*j + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^4+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^2)*u4^2) *j^2 + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^3+(4*u1^2*u2^2*u3^6+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3^2)*u4) *g + ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3^2)*u4^2) *h + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^4+((2*u1*u2^2+4*u1^2*u2)*u3^6+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4^2) *j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *k + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^4+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4^2) ; (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4) *e*h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4) *f*h*j^2 + (((4*u1^2*u2^2+8*u1^3*u2)*u3^4+(4*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4) *e*h*j + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4) *f*h*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4) *e*j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4) *f*j^2 + ((2*u1*u3^7+(4*u1*u2^2+(-4)*u1^2*u2)*u3^5+(2*u1*u2^4+(-4)*u1^2*u2^3)*u3^3)*u4) *h*j^2 + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+(4*u1^2*u2*u3^6+(8*u1^2*u2^3+(-16)*u1^3*u2^2)*u3^4+(4*u1^2*u2^5+(-16)*u1^3*u2^4)*u3^2)*u4) *e*h + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4) *f*h + ((((-4)*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-4)*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4) *e*j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4) *f*j + ((4*u1^2*u3^5+4*u1^2*u2^2*u3^3)*u4^3+(((-4)*u1^2+(-2)*u1*u2)*u3^7+((-4)*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^5+((-2)*u1*u2^5+8*u1^3*u2^3)*u3^3)*u4) *h*j + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4^2+((-2)*u1*u2*u3^7+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^5+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^3)*u4) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^3+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+16*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+16*u1^3*u2^5)*u3^2)*u4) *e + ((2*u1*u2^3*u3^6+(4*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4) *f + (((-4)*u1^2*u2*u3^5+(-4)*u1^2*u2^3*u3^3)*u4^3+(2*u1*u2^2*u3^6+(4*u1*u2^4+8*u1^3*u2^2)*u3^4+(2*u1*u2^6+8*u1^3*u2^4)*u3^2)*u4^2+((2*u1*u2^2+4*u1^2*u2)*u3^7+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^5+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^3)*u4) *j + (((-2)*u1*u2^3*u3^6+((-4)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^4+((-2)*u1*u2^7+4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3^2)*u4^2) ; (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4) *e*g*h*j*k + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4) *f*g*h*j*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4)*u3)*u4) *e*g*h*j + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4)*u3)*u4) *f*g*h*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3)*u4) *e*g*h*k + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3)*u4) *f*g*h*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *e*g*j*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *f*g*j*k + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^2) *e*h*j*k + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^2) *f*h*j*k + ((2*u1*u3^6+(4*u1*u2^2+(-4)*u1^2*u2)*u3^4+(2*u1*u2^4+(-4)*u1^2*u2^3)*u3^2)*u4) *g*h*j*k + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^2) *h^2*j*k + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4^3+(4*u1^2*u2*u3^5+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *e*g*h + (((-4)*u1^2*u2*u3^3+(-4)*u1^2*u2^3*u3)*u4^3+(4*u1^2*u2*u3^5+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *f*g*h + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3)*u4) *e*g*j + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3)*u4) *f*g*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3)*u4^2) *e*h*j + ((2*u1*u2*u3^5+(4*u1*u2^3+(-4)*u1^2*u2^2)*u3^3+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3)*u4^2) *f*h*j + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *e*g*k + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3)*u4) *f*g*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2+(-8)*u1^3*u2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3)*u4^2) *e*h*k + (((-2)*u1*u2*u3^5+((-4)*u1*u2^3+4*u1^2*u2^2+(-8)*u1^3*u2)*u3^3+((-2)*u1*u2^5+4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3)*u4^2) *f*h*k + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^3+(((-4)*u1^2+(-2)*u1*u2)*u3^6+((-4)*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^4+((-2)*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4) *g*h*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h^2*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *e*j*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *f*j*k + (((-2)*u1*u2*u3^6+((-4)*u1*u2^3+4*u1^2*u2^2)*u3^4+((-2)*u1*u2^5+4*u1^2*u2^4)*u3^2)*u4) *g*j*k + (((-2)*u1*u3^6+((-8)*u1^3+(-4)*u1*u2^2)*u3^4+((-2)*u1*u2^4+(-8)*u1^3*u2^2)*u3^2)*u4^2) *h*j*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4^3+((-4)*u1^2*u2^2*u3^5+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^3+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3)*u4) *e*g + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4^3+((-4)*u1^2*u2^2*u3^5+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^3+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3)*u4) *f*g + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^4+((-4)*u1^2*u2*u3^5+((-8)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *e*h + ((4*u1^2*u2*u3^3+4*u1^2*u2^3*u3)*u4^4+((-4)*u1^2*u2*u3^5+((-8)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *f*h + (((-4)*u1^2*u3^4+(-4)*u1^2*u2^2*u3^2)*u4^4+(4*u1^2*u3^6+(8*u1^2*u2^2+(-8)*u1^3*u2)*u3^4+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^2)*u4^2) *h^2 + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5)*u3)*u4^2) *e*j + (((-2)*u1*u2^2*u3^5+((-4)*u1*u2^4+4*u1^2*u2^3)*u3^3+((-2)*u1*u2^6+4*u1^2*u2^5)*u3)*u4^2) *f*j + ((4*u1^2*u3^4+4*u1^2*u2^2*u3^2)*u4^4+((-4)*u1^2*u3^6+((-8)*u1^2*u2^2+8*u1^3*u2)*u3^4+((-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4^2) *h*j + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *e*k + ((2*u1*u2^2*u3^5+(4*u1*u2^4+(-4)*u1^2*u2^3+8*u1^3*u2^2)*u3^3+(2*u1*u2^6+(-4)*u1^2*u2^5+8*u1^3*u2^4)*u3)*u4^2) *f*k + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^3+((2*u1*u2^2+4*u1^2*u2)*u3^6+(4*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(2*u1*u2^6+(-8)*u1^3*u2^4)*u3^2)*u4) *g*k + ((2*u1*u2*u3^6+(4*u1*u2^3+8*u1^3*u2)*u3^4+(2*u1*u2^5+8*u1^3*u2^3)*u3^2)*u4^2) *h*k + ((2*u1*u2*u3^6+(4*u1*u2^3+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^2)*u4^2) *j*k + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^4+(4*u1^2*u2^2*u3^5+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3)*u4^2) *e + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^4+(4*u1^2*u2^2*u3^5+(8*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3+(4*u1^2*u2^6+(-8)*u1^3*u2^5)*u3)*u4^2) *f + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^4+(4*u1^2*u2*u3^6+(8*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+(4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *j + (((-2)*u1*u2^2*u3^6+((-4)*u1*u2^4+4*u1^2*u2^3+(-8)*u1^3*u2^2)*u3^4+((-2)*u1*u2^6+4*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^2)*u4^2) *k + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^4+((-4)*u1^2*u2^2*u3^6+((-8)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-4)*u1^2*u2^6+8*u1^3*u2^5)*u3^2)*u4^2) ; ((2*u1*u2^2*u3^6+(4*u1*u2^4+(-4)*u1^2*u2^3)*u3^4+(2*u1*u2^6+(-4)*u1^2*u2^5)*u3^2)*u4) *j^2 + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^3+(((-2)*u1*u2^3+(-4)*u1^2*u2^2)*u3^6+((-4)*u1*u2^5+(-4)*u1^2*u2^4+8*u1^3*u2^3)*u3^4+((-2)*u1*u2^7+8*u1^3*u2^5)*u3^2)*u4) *j + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^3+(4*u1^2*u2^3*u3^6+(8*u1^2*u2^5+(-8)*u1^3*u2^4)*u3^4+(4*u1^2*u2^7+(-8)*u1^3*u2^6)*u3^2)*u4) ; 0; (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4) *e*g*h*i*j + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4) *f*g*h*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4) *e*g*h*i*k + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4) *f*g*h*i*k + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *e*g*h*i + ((4*u1^2*u2^2*u3^3+4*u1^2*u2^4*u3)*u4) *f*g*h*i + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4) *e*g*h*j + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4) *f*g*h*j + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4) *e*g*i*j + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4) *f*g*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4^2) *e*h*i*j + ((2*u1*u2^2*u3^3+2*u1*u2^4*u3)*u4^2) *f*h*i*j + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4) *e*g*h*k + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4) *f*g*h*k + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4) *e*g*i*k + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4) *f*g*i*k + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4^2) *e*h*i*k + (((-2)*u1*u2^2*u3^3+(-2)*u1*u2^4*u3)*u4^2) *f*h*i*k + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4) *e*g*h + (((-4)*u1^2*u2^2*u3^4+(-4)*u1^2*u2^4*u3^2)*u4) *f*g*h + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *e*h^2 + (((-4)*u1^2*u2^3*u3^3+(-4)*u1^2*u2^5*u3)*u4) *e*g*i + (((-4)*u1^2*u2^3*u3^3+(-4)*u1^2*u2^5*u3)*u4) *f*g*i + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *e*h*i + (((-4)*u1^2*u2^2*u3^3+(-4)*u1^2*u2^4*u3)*u4^2) *f*h*i + ((4*u1^2*u2*u3^4+4*u1^2*u2^3*u3^2)*u4^2) *h^2*i + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4) *e*g*j + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4) *f*g*j + ((((-2)*u1*u2^2+4*u1^2*u2)*u3^4+((-2)*u1*u2^4+4*u1^2*u2^3)*u3^2)*u4^2) *e*h*j + (((-2)*u1*u2^2*u3^4+(-2)*u1*u2^4*u3^2)*u4^2) *f*h*j + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4^2) *e*i*j + (((-2)*u1*u2^3*u3^3+(-2)*u1*u2^5*u3)*u4^2) *f*i*j + (((-4)*u1^2*u2*u3^4+(-4)*u1^2*u2^3*u3^2)*u4^2) *h*i*j + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4) *e*g*k + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4) *f*g*k + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4^2) *e*h*k + ((2*u1*u2^2*u3^4+2*u1*u2^4*u3^2)*u4^2) *f*h*k + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4^2) *e*i*k + ((2*u1*u2^3*u3^3+2*u1*u2^5*u3)*u4^2) *f*i*k + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4) *e*g + ((4*u1^2*u2^3*u3^4+4*u1^2*u2^5*u3^2)*u4) *f*g + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *e*h + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *f*h + ((4*u1^2*u2^3*u3^3+4*u1^2*u2^5*u3)*u4^2) *e*i + ((4*u1^2*u2^3*u3^3+4*u1^2*u2^5*u3)*u4^2) *f*i + (((2*u1*u2^3+(-4)*u1^2*u2^2)*u3^4+(2*u1*u2^5+(-4)*u1^2*u2^4)*u3^2)*u4^2) *e*j + ((2*u1*u2^3*u3^4+2*u1*u2^5*u3^2)*u4^2) *f*j + ((4*u1^2*u2^2*u3^4+4*u1^2*u2^4*u3^2)*u4^2) *i*j + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *e*k + (((-2)*u1*u2^3*u3^4+(-2)*u1*u2^5*u3^2)*u4^2) *f*k + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *f + (((-4)*u1^2*u2^3*u3^4+(-4)*u1^2*u2^5*u3^2)*u4^2) *i + ((4*u1^2*u2^2*u3^5+(4*u1^2*u2^4+(-8)*u1^3*u2^3)*u3^3)*u4^2+((2*u1*u2^3+4*u1^2*u2^2)*u3^6+(4*u1*u2^5+(-8)*u1^3*u2^3)*u3^4+(2*u1*u2^7+(-4)*u1^2*u2^6)*u3^2)*u4) *j + (((-4)*u1^2*u2^3*u3^5+((-4)*u1^2*u2^5+8*u1^3*u2^4)*u3^3)*u4^2+(((-2)*u1*u2^4+(-4)*u1^2*u2^3)*u3^6+((-4)*u1*u2^6+8*u1^3*u2^4)*u3^4+((-2)*u1*u2^8+4*u1^2*u2^7)*u3^2)*u4) ; ];
[
(u2^2+(-2)*u1*u2+u3^2) ; ((-2)*u1*u4) *h ; 0; (2*u1*u4^2) ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; (1) *k + ((-2)*u1) ; 0; 0; ((-1)*u4) *h ; 0; 0; 0; ((-1)) *h^2 + (2*u1) *h ; ];
[
0; 0; 0; 0; ((-1)) *k + (2*u1) ; 0; 0; 0; (1) *g ; ];
[
0; 0; 0; 0; ((-1)*u2) *i + ((-1)*u3) *j ; 0; (u2^2) ; 0; ];
[
0; 0; ((-1)) *g ; 0; (1) *k ; 0; 0; ];
];
c:=
2;