Morley
Geogebra sheet
Coq statement
Lemma Morley: forall A B C A1 A2 B1 B2 C1 C2 A3 B3 C3:point,
X A = 0 -> Y A = 0 -> Y B = 0 ->
equalangle B A A1 A1 A A2 ->
equalangle A1 A A2 A2 A C ->
equalangle C B B1 B1 B B2 ->
equalangle B1 B B2 B2 B A ->
equalangle A C C1 C1 C C2 ->
equalangle C1 C C2 C2 C B ->
collinear A1 B C -> collinear A2 B C ->
collinear B1 A C -> collinear B2 A C ->
collinear C1 A B -> collinear C2 A B ->
collinear A3 B B1 -> collinear A3 C C2 ->
collinear B3 A A2 -> collinear B3 C C1 ->
collinear C3 A A1 -> collinear C3 B B2 ->
distance2 A3 B3 = distance2 A3 C3
\/ X B^7 = 0
\/ 2*Y C3^3=0
\/ Y C^9=0
\/ (Y C3^2+X C3^2)^2=0
\/ orthogonal A C3 B C.
Proof.
geo_begin.
tzRpv 0%Z (X B::X C::Y C::X C3::Y C3::nil)
(X A1::Y A1::X A2:: Y A2:: X B1::Y B1::X B2::Y B2::X C1::Y C1::X C2::Y C2::
X A3::Y A3::X B3::Y B3::nil).
Qed.
Algebraic version
p:= ((-4)*u1^7*u3^10*u5^8+(((4*u1^8+(-4)*u1^7*u2)*u3^9)*u4)*u5^7+(-8)*u1^7*u3^10*u4^2*u5^6+(((8*u1^8+(-8)*u1^7*u2)*u3^9)*u4^3)*u5^5+(-4)*u1^7*u3^10*u4^4*u5^4+(((4*u1^8+(-4)*u1^7*u2)*u3^9)*u4^5)*u5^3) *r*t + (2*u1^7*u3^10*u5^8+((((-2)*u1^8+2*u1^7*u2)*u3^9)*u4)*u5^7+4*u1^7*u3^10*u4^2*u5^6+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4^3)*u5^5+2*u1^7*u3^10*u4^4*u5^4+((((-2)*u1^8+2*u1^7*u2)*u3^9)*u4^5)*u5^3) *t^2 + ((-4)*u1^7*u3^10*u5^8+(((4*u1^8+(-4)*u1^7*u2)*u3^9)*u4)*u5^7+(-8)*u1^7*u3^10*u4^2*u5^6+(((8*u1^8+(-8)*u1^7*u2)*u3^9)*u4^3)*u5^5+(-4)*u1^7*u3^10*u4^4*u5^4+(((4*u1^8+(-4)*u1^7*u2)*u3^9)*u4^5)*u5^3) *s*u + (2*u1^7*u3^10*u5^8+((((-2)*u1^8+2*u1^7*u2)*u3^9)*u4)*u5^7+4*u1^7*u3^10*u4^2*u5^6+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4^3)*u5^5+2*u1^7*u3^10*u4^4*u5^4+((((-2)*u1^8+2*u1^7*u2)*u3^9)*u4^5)*u5^3) *u^2 + (4*u1^7*u3^10*u4*u5^8+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4^2)*u5^7+8*u1^7*u3^10*u4^3*u5^6+((((-8)*u1^8+8*u1^7*u2)*u3^9)*u4^4)*u5^5+4*u1^7*u3^10*u4^5*u5^4+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4^6)*u5^3) *r + (4*u1^7*u3^10*u5^9+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4)*u5^8+8*u1^7*u3^10*u4^2*u5^7+((((-8)*u1^8+8*u1^7*u2)*u3^9)*u4^3)*u5^6+4*u1^7*u3^10*u4^4*u5^5+((((-4)*u1^8+4*u1^7*u2)*u3^9)*u4^5)*u5^4) *s + ((-2)*u1^7*u3^10*u5^10+(((2*u1^8+(-2)*u1^7*u2)*u3^9)*u4)*u5^9+(-6)*u1^7*u3^10*u4^2*u5^8+(((6*u1^8+(-6)*u1^7*u2)*u3^9)*u4^3)*u5^7+(-6)*u1^7*u3^10*u4^4*u5^6+(((6*u1^8+(-6)*u1^7*u2)*u3^9)*u4^5)*u5^5+(-2)*u1^7*u3^10*u4^6*u5^4+(((2*u1^8+(-2)*u1^7*u2)*u3^9)*u4^7)*u5^3)
F:= [
(u3) *n^2*p^3 + (u3) *o^2*p^3 + (u1+(-1)*u2) *n^2*p^2*q + (u1+(-1)*u2) *o^2*p^2*q + (u3) *n^2*p*q^2 + (u3) *o^2*p*q^2 + (u1+(-1)*u2) *n^2*q^3 + (u1+(-1)*u2) *o^2*q^3 + (((-1)*u1+(-2)*u2)*u3) *n^2*p^2 + (((-1)*u1+(-2)*u2)*u3) *o^2*p^2 + ((-2)*u2*u3) *n*p^3 + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-3)*u3^2) *o*p^3 + (2*u2^2+(-2)*u1*u2+(-2)*u3^2) *n^2*p*q + (2*u2^2+(-2)*u1*u2+(-2)*u3^2) *o^2*p*q + (u1^2+3*u2^2+(-4)*u1*u2+u3^2) *n*p^2*q + (((-2)*u1+2*u2)*u3) *o*p^2*q + (((-3)*u1+2*u2)*u3) *n^2*q^2 + (((-3)*u1+2*u2)*u3) *o^2*q^2 + ((-2)*u2*u3) *n*p*q^2 + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-3)*u3^2) *o*p*q^2 + (u1^2+3*u2^2+(-4)*u1*u2+u3^2) *n*q^3 + (((-2)*u1+2*u2)*u3) *o*q^3 + (u3^3+(u2^2+2*u1*u2)*u3) *n^2*p + (u3^3+(u2^2+2*u1*u2)*u3) *o^2*p + ((-1)*u3^3+((-1)*u1^2+3*u2^2+4*u1*u2)*u3) *n*p^2 + (3*u2^3+(-6)*u1*u2^2+3*u1^2*u2+(2*u1+7*u2)*u3^2) *o*p^2 + (2*u3^3+(u1^2+2*u2^2+(-2)*u1*u2)*u3) *p^3 + ((-1)*u2^3+u1*u2^2+(3*u1+(-1)*u2)*u3^2) *n^2*q + ((-1)*u2^3+u1*u2^2+(3*u1+(-1)*u2)*u3^2) *o^2*q + ((-6)*u2^3+8*u1*u2^2+(-2)*u1^2*u2+2*u2*u3^2) *n*p*q + (6*u3^3+(2*u1^2+(-2)*u2^2)*u3) *o*p*q + ((-2)*u2^3+3*u1*u2^2+(-1)*u1^2*u2+(u1+(-2)*u2)*u3^2) *p^2*q + ((-3)*u3^3+((-3)*u1^2+(-7)*u2^2+12*u1*u2)*u3) *n*q^2 + (u2^3+(-2)*u1*u2^2+u1^2*u2+(6*u1+(-3)*u2)*u3^2) *o*q^2 + (2*u3^3+(u1^2+2*u2^2+(-2)*u1*u2)*u3) *p*q^2 + ((-2)*u2^3+3*u1*u2^2+(-1)*u1^2*u2+(u1+(-2)*u2)*u3^2) *q^3 + ((-1)*u1*u3^3+(-1)*u1*u2^2*u3) *n^2 + ((-1)*u1*u3^3+(-1)*u1*u2^2*u3) *o^2 + (((-8)*u1*u2^2+2*u1^2*u2)*u3) *n*p + ((-3)*u2^4+6*u1*u2^3+(-3)*u1^2*u2^2+(-3)*u3^4+((-1)*u1^2+(-6)*u2^2+(-2)*u1*u2)*u3^2) *o*p + (((-1)*u1+(-4)*u2)*u3^3+((-4)*u2^3+3*u1*u2^2+(-2)*u1^2*u2)*u3) *p^2 + (3*u2^4+(-4)*u1*u2^3+u1^2*u2^2+3*u3^4+(3*u1^2+6*u2^2+(-12)*u1*u2)*u3^2) *n*q + ((-6)*u1*u3^3+(2*u1*u2^2+(-2)*u1^2*u2)*u3) *o*q + (4*u2^4+(-6)*u1*u2^3+2*u1^2*u2^2+(-4)*u3^4+((-2)*u1^2+2*u1*u2)*u3^2) *p*q + (((-3)*u1+4*u2)*u3^3+(4*u2^3+(-7)*u1*u2^2+2*u1^2*u2)*u3) *q^2 + ((-1)*u3^5+((-1)*u1^2+(-2)*u2^2+4*u1*u2)*u3^3+((-1)*u2^4+4*u1*u2^3+(-1)*u1^2*u2^2)*u3) *n + (u2^5+(-2)*u1*u2^4+u1^2*u2^3+(2*u1+u2)*u3^4+(2*u2^3+u1^2*u2)*u3^2) *o + (2*u3^5+(u1^2+4*u2^2)*u3^3+(2*u2^4+u1^2*u2^2)*u3) *p + ((-2)*u2^5+3*u1*u2^4+(-1)*u1^2*u2^3+(3*u1+(-2)*u2)*u3^4+((-4)*u2^3+6*u1*u2^2+(-1)*u1^2*u2)*u3^2) *q + ((-1)*u1*u3^5+(-2)*u1*u2^2*u3^3+(-1)*u1*u2^4*u3) ;
((-1)*u1+u2) *n^2*p^3 + ((-1)*u1+u2) *o^2*p^3 + (u3) *n^2*p^2*q + (u3) *o^2*p^2*q + ((-1)*u1+u2) *n^2*p*q^2 + ((-1)*u1+u2) *o^2*p*q^2 + (u3) *n^2*q^3 + (u3) *o^2*q^3 + ((-3)*u2^2+3*u1*u2+(-1)*u3^2) *n^2*p^2 + ((-3)*u2^2+3*u1*u2+(-1)*u3^2) *o^2*p^2 + (u1^2+(-1)*u2^2+u3^2) *n*p^3 + ((2*u1+(-2)*u2)*u3) *o*p^3 + ((2*u1+(-4)*u2)*u3) *n^2*p*q + ((2*u1+(-4)*u2)*u3) *o^2*p*q + ((-2)*u2*u3) *n*p^2*q + (u1^2+u2^2+(-2)*u1*u2+(-1)*u3^2) *o*p^2*q + ((-1)*u2^2+u1*u2+(-3)*u3^2) *n^2*q^2 + ((-1)*u2^2+u1*u2+(-3)*u3^2) *o^2*q^2 + (u1^2+(-1)*u2^2+u3^2) *n*p*q^2 + ((2*u1+(-2)*u2)*u3) *o*p*q^2 + ((-2)*u2*u3) *n*q^3 + (u1^2+u2^2+(-2)*u1*u2+(-1)*u3^2) *o*q^3 + (3*u2^3+(-3)*u1*u2^2+((-1)*u1+3*u2)*u3^2) *n^2*p + (3*u2^3+(-3)*u1*u2^2+((-1)*u1+3*u2)*u3^2) *o^2*p + (3*u2^3+(-3)*u1^2*u2+(-1)*u2*u3^2) *n*p^2 + (u3^3+((-1)*u1^2+5*u2^2+(-4)*u1*u2)*u3) *o*p^2 + (u1*u2^2+(-1)*u1^2*u2+(-1)*u1*u3^2) *p^3 + (3*u3^3+(3*u2^2+(-2)*u1*u2)*u3) *n^2*q + (3*u3^3+(3*u2^2+(-2)*u1*u2)*u3) *o^2*q + ((-2)*u3^3+((-2)*u1^2+6*u2^2)*u3) *n*p*q + ((-2)*u2^3+4*u1*u2^2+(-2)*u1^2*u2+((-4)*u1+6*u2)*u3^2) *o*p*q + (((-1)*u1^2+2*u1*u2)*u3) *p^2*q + (u2^3+(-1)*u1^2*u2+5*u2*u3^2) *n*q^2 + (3*u3^3+((-3)*u1^2+(-1)*u2^2+4*u1*u2)*u3) *o*q^2 + (u1*u2^2+(-1)*u1^2*u2+(-1)*u1*u3^2) *p*q^2 + (((-1)*u1^2+2*u1*u2)*u3) *q^3 + ((-1)*u2^4+u1*u2^3+(-1)*u3^4+((-2)*u2^2+u1*u2)*u3^2) *n^2 + ((-1)*u2^4+u1*u2^3+(-1)*u3^4+((-2)*u2^2+u1*u2)*u3^2) *o^2 + ((-3)*u2^4+3*u1^2*u2^2+u3^4+(u1^2+(-2)*u2^2)*u3^2) *n*p + ((2*u1+(-4)*u2)*u3^3+((-4)*u2^3+2*u1*u2^2+2*u1^2*u2)*u3) *o*p + ((-3)*u1*u2^3+3*u1^2*u2^2+(u1^2+u1*u2)*u3^2) *p^2 + ((-4)*u2*u3^3+((-4)*u2^3+2*u1^2*u2)*u3) *n*q + (u2^4+(-2)*u1*u2^3+u1^2*u2^2+(-3)*u3^4+(3*u1^2+(-2)*u2^2+(-2)*u1*u2)*u3^2) *o*q + (2*u1*u3^3+((-6)*u1*u2^2+4*u1^2*u2)*u3) *p*q + ((-1)*u1*u2^3+u1^2*u2^2+(3*u1^2+(-5)*u1*u2)*u3^2) *q^2 + (u2^5+(-1)*u1^2*u2^3+u2*u3^4+(2*u2^3+(-1)*u1^2*u2)*u3^2) *n + (u3^5+((-1)*u1^2+2*u2^2)*u3^3+(u2^4+(-1)*u1^2*u2^2)*u3) *o + (3*u1*u2^4+(-3)*u1^2*u2^3+(-1)*u1*u3^4+(2*u1*u2^2+(-3)*u1^2*u2)*u3^2) *p + (((-3)*u1^2+4*u1*u2)*u3^3+(4*u1*u2^3+(-3)*u1^2*u2^2)*u3) *q + ((-1)*u1*u2^5+u1^2*u2^4+(u1^2+(-1)*u1*u2)*u3^4+((-2)*u1*u2^3+2*u1^2*u2^2)*u3^2) ;
(u3) *n^3*p^2 + ((-1)*u2) *n^2*o*p^2 + (u3) *n*o^2*p^2 + ((-1)*u2) *o^3*p^2 + (u3) *n^3*q^2 + ((-1)*u2) *n^2*o*q^2 + (u3) *n*o^2*q^2 + ((-1)*u2) *o^3*q^2 + ((-2)*u2*u3) *n^3*p + (3*u2^2+u3^2) *n^2*o*p + ((-2)*u2*u3) *n*o^2*p + (3*u2^2+u3^2) *o^3*p + ((-2)*u2*u3) *n^2*p^2 + (2*u2^2+(-2)*u3^2) *n*o*p^2 + (2*u2*u3) *o^2*p^2 + ((-1)*u2^2+(-3)*u3^2) *n^3*q + (2*u2*u3) *n^2*o*q + ((-1)*u2^2+(-3)*u3^2) *n*o^2*q + (2*u2*u3) *o^3*q + ((-2)*u2*u3) *n^2*q^2 + (2*u2^2+(-2)*u3^2) *n*o*q^2 + (2*u2*u3) *o^2*q^2 + (2*u3^3+2*u2^2*u3) *n^3 + ((-2)*u2^3+(-2)*u2*u3^2) *n^2*o + (2*u3^3+2*u2^2*u3) *n*o^2 + ((-2)*u2^3+(-2)*u2*u3^2) *o^3 + ((-1)*u3^3+3*u2^2*u3) *n^2*p + ((-6)*u2^3+2*u2*u3^2) *n*o*p + ((-3)*u3^3+(-7)*u2^2*u3) *o^2*p + (u3^3+u2^2*u3) *n*p^2 + ((-1)*u2^3+(-1)*u2*u3^2) *o*p^2 + (3*u2^3+7*u2*u3^2) *n^2*q + (6*u3^3+(-2)*u2^2*u3) *n*o*q + (u2^3+(-3)*u2*u3^2) *o^2*q + (u3^3+u2^2*u3) *n*q^2 + ((-1)*u2^3+(-1)*u2*u3^2) *o*q^2 + ((-4)*u2*u3^3+(-4)*u2^3*u3) *n^2 + (4*u2^4+(-4)*u3^4) *n*o + (4*u2*u3^3+4*u2^3*u3) *o^2 + (3*u2^4+3*u3^4+6*u2^2*u3^2) *o*p + ((-3)*u2^4+(-3)*u3^4+(-6)*u2^2*u3^2) *n*q + (2*u3^5+4*u2^2*u3^3+2*u2^4*u3) *n + ((-2)*u2^5+(-2)*u2*u3^4+(-4)*u2^3*u3^2) *o + ((-1)*u3^5+(-2)*u2^2*u3^3+(-1)*u2^4*u3) *p + (u2^5+u2*u3^4+2*u2^3*u3^2) *q ;
((-1)*u2) *n^3*p^2 + ((-1)*u3) *n^2*o*p^2 + ((-1)*u2) *n*o^2*p^2 + ((-1)*u3) *o^3*p^2 + ((-1)*u2) *n^3*q^2 + ((-1)*u3) *n^2*o*q^2 + ((-1)*u2) *n*o^2*q^2 + ((-1)*u3) *o^3*q^2 + (u2^2+(-1)*u3^2) *n^3*p + (2*u2*u3) *n^2*o*p + (u2^2+(-1)*u3^2) *n*o^2*p + (2*u2*u3) *o^3*p + (3*u2^2+u3^2) *n^2*p^2 + (4*u2*u3) *n*o*p^2 + (u2^2+3*u3^2) *o^2*p^2 + (2*u2*u3) *n^3*q + ((-1)*u2^2+u3^2) *n^2*o*q + (2*u2*u3) *n*o^2*q + ((-1)*u2^2+u3^2) *o^3*q + (3*u2^2+u3^2) *n^2*q^2 + (4*u2*u3) *n*o*q^2 + (u2^2+3*u3^2) *o^2*q^2 + ((-3)*u2^3+u2*u3^2) *n^2*p + (2*u3^3+(-6)*u2^2*u3) *n*o*p + ((-1)*u2^3+(-5)*u2*u3^2) *o^2*p + ((-3)*u2^3+(-3)*u2*u3^2) *n*p^2 + ((-3)*u3^3+(-3)*u2^2*u3) *o*p^2 + ((-1)*u3^3+(-5)*u2^2*u3) *n^2*q + (2*u2^3+(-6)*u2*u3^2) *n*o*q + ((-3)*u3^3+u2^2*u3) *o^2*q + ((-3)*u2^3+(-3)*u2*u3^2) *n*q^2 + ((-3)*u3^3+(-3)*u2^2*u3) *o*q^2 + (3*u2^4+(-1)*u3^4+2*u2^2*u3^2) *n*p + (4*u2*u3^3+4*u2^3*u3) *o*p + (u2^4+u3^4+2*u2^2*u3^2) *p^2 + (4*u2*u3^3+4*u2^3*u3) *n*q + ((-1)*u2^4+3*u3^4+2*u2^2*u3^2) *o*q + (u2^4+u3^4+2*u2^2*u3^2) *q^2 + ((-1)*u2^5+(-1)*u2*u3^4+(-2)*u2^3*u3^2) *p + ((-1)*u3^5+(-2)*u2^2*u3^3+(-1)*u2^4*u3) *q ;
((-1)*u1) *j^2*l^2*m + ((-1)*u1) *k^2*l^2*m + ((-1)*u1) *j^2*m^3 + ((-1)*u1) *k^2*m^3 + ((-1)*u1^2) *k*l^3 + (2*u1^2) *j^2*l*m + (2*u1^2) *k^2*l*m + (3*u1^2) *j*l^2*m + ((-1)*u1^2) *k*l*m^2 + (3*u1^2) *j*m^3 + (3*u1^3) *k*l^2 + ((-1)*u1^3) *j^2*m + ((-1)*u1^3) *k^2*m + ((-6)*u1^3) *j*l*m + ((-2)*u1^3) *l^2*m + (u1^3) *k*m^2 + ((-2)*u1^3) *m^3 + ((-3)*u1^4) *k*l + (3*u1^4) *j*m + (4*u1^4) *l*m + (u1^5) *k + ((-2)*u1^5) *m ;
(u1) *j^2*l^3 + (u1) *k^2*l^3 + (u1) *j^2*l*m^2 + (u1) *k^2*l*m^2 + ((-3)*u1^2) *j^2*l^2 + ((-3)*u1^2) *k^2*l^2 + ((-1)*u1^2) *j*l^3 + (u1^2) *k*l^2*m + ((-1)*u1^2) *j^2*m^2 + ((-1)*u1^2) *k^2*m^2 + ((-1)*u1^2) *j*l*m^2 + (u1^2) *k*m^3 + (3*u1^3) *j^2*l + (3*u1^3) *k^2*l + (3*u1^3) *j*l^2 + ((-2)*u1^3) *k*l*m + (u1^3) *j*m^2 + ((-1)*u1^4) *j^2 + ((-1)*u1^4) *k^2 + ((-3)*u1^4) *j*l + (u1^4) *k*m + (u1^5) *j ;
((-1)*u3) *j^3*l^2 + ((-1)*u1+u2) *j^2*k*l^2 + ((-1)*u3) *j*k^2*l^2 + ((-1)*u1+u2) *k^3*l^2 + ((-1)*u3) *j^3*m^2 + ((-1)*u1+u2) *j^2*k*m^2 + ((-1)*u3) *j*k^2*m^2 + ((-1)*u1+u2) *k^3*m^2 + (2*u1*u3) *j^3*l + (3*u1^2+u2^2+(-4)*u1*u2+u3^2) *j^2*k*l + (2*u1*u3) *j*k^2*l + (3*u1^2+u2^2+(-4)*u1*u2+u3^2) *k^3*l + (3*u1*u3) *j^2*l^2 + (2*u1^2+(-2)*u1*u2) *j*k*l^2 + (u1*u3) *k^2*l^2 + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-1)*u3^2) *j^3*m + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-1)*u3^2) *j*k^2*m + (3*u1*u3) *j^2*m^2 + (2*u1^2+(-2)*u1*u2) *j*k*m^2 + (u1*u3) *k^2*m^2 + ((-1)*u1^2*u3) *j^3 + ((-2)*u1^3+(-1)*u1*u2^2+3*u1^2*u2+(-1)*u1*u3^2) *j^2*k + ((-1)*u1^2*u3) *j*k^2 + ((-2)*u1^3+(-1)*u1*u2^2+3*u1^2*u2+(-1)*u1*u3^2) *k^3 + ((-6)*u1^2*u3) *j^2*l + ((-6)*u1^3+(-2)*u1*u2^2+8*u1^2*u2+(-2)*u1*u3^2) *j*k*l + ((-2)*u1^2*u3) *k^2*l + ((-3)*u1^2*u3) *j*l^2 + ((-1)*u1^3+u1^2*u2) *k*l^2 + (3*u1^3+3*u1*u2^2+(-6)*u1^2*u2+3*u1*u3^2) *j^2*m + (u1^3+u1*u2^2+(-2)*u1^2*u2+u1*u3^2) *k^2*m + ((-3)*u1^2*u3) *j*m^2 + ((-1)*u1^3+u1^2*u2) *k*m^2 + (3*u1^3*u3) *j^2 + (4*u1^4+2*u1^2*u2^2+(-6)*u1^3*u2+2*u1^2*u3^2) *j*k + (u1^3*u3) *k^2 + (6*u1^3*u3) *j*l + (3*u1^4+u1^2*u2^2+(-4)*u1^3*u2+u1^2*u3^2) *k*l + (u1^3*u3) *l^2 + ((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2+(-3)*u1^2*u3^2) *j*m + (u1^3*u3) *m^2 + ((-3)*u1^4*u3) *j + ((-2)*u1^5+(-1)*u1^3*u2^2+3*u1^4*u2+(-1)*u1^3*u3^2) *k + ((-2)*u1^4*u3) *l + (u1^5+u1^3*u2^2+(-2)*u1^4*u2+u1^3*u3^2) *m + (u1^5*u3) ;
((-1)*u1+u2) *j^3*l^2 + (u3) *j^2*k*l^2 + ((-1)*u1+u2) *j*k^2*l^2 + (u3) *k^3*l^2 + ((-1)*u1+u2) *j^3*m^2 + (u3) *j^2*k*m^2 + ((-1)*u1+u2) *j*k^2*m^2 + (u3) *k^3*m^2 + (u1^2+(-1)*u2^2+(-1)*u3^2) *j^3*l + ((-2)*u1*u3) *j^2*k*l + (u1^2+(-1)*u2^2+(-1)*u3^2) *j*k^2*l + ((-2)*u1*u3) *k^3*l + (3*u1^2+(-3)*u1*u2) *j^2*l^2 + ((-2)*u1*u3) *j*k*l^2 + (u1^2+(-1)*u1*u2) *k^2*l^2 + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-1)*u3^2) *j^2*k*m + ((-1)*u1^2+(-1)*u2^2+2*u1*u2+(-1)*u3^2) *k^3*m + (3*u1^2+(-3)*u1*u2) *j^2*m^2 + ((-2)*u1*u3) *j*k*m^2 + (u1^2+(-1)*u1*u2) *k^2*m^2 + (u1*u2^2+(-1)*u1^2*u2+u1*u3^2) *j^3 + (u1^2*u3) *j^2*k + (u1*u2^2+(-1)*u1^2*u2+u1*u3^2) *j*k^2 + (u1^2*u3) *k^3 + ((-3)*u1^3+3*u1*u2^2+3*u1*u3^2) *j^2*l + (4*u1^2*u3) *j*k*l + ((-1)*u1^3+u1*u2^2+u1*u3^2) *k^2*l + ((-3)*u1^3+3*u1^2*u2) *j*l^2 + (u1^2*u3) *k*l^2 + (2*u1^3+2*u1*u2^2+(-4)*u1^2*u2+2*u1*u3^2) *j*k*m + ((-3)*u1^3+3*u1^2*u2) *j*m^2 + (u1^2*u3) *k*m^2 + ((-3)*u1^2*u2^2+3*u1^3*u2+(-3)*u1^2*u3^2) *j^2 + ((-2)*u1^3*u3) *j*k + ((-1)*u1^2*u2^2+u1^3*u2+(-1)*u1^2*u3^2) *k^2 + (3*u1^4+(-3)*u1^2*u2^2+(-3)*u1^2*u3^2) *j*l + ((-2)*u1^3*u3) *k*l + (u1^4+(-1)*u1^3*u2) *l^2 + ((-1)*u1^4+(-1)*u1^2*u2^2+2*u1^3*u2+(-1)*u1^2*u3^2) *k*m + (u1^4+(-1)*u1^3*u2) *m^2 + (3*u1^3*u2^2+(-3)*u1^4*u2+3*u1^3*u3^2) *j + (u1^4*u3) *k + ((-1)*u1^5+u1^3*u2^2+u1^3*u3^2) *l + ((-1)*u1^4*u2^2+u1^5*u2+(-1)*u1^4*u3^2) ;
((-1)*u3) *f^2*h^3 + ((-1)*u3) *g^2*h^3 + (u2) *f^2*h^2*i + (u2) *g^2*h^2*i + ((-1)*u3) *f^2*h*i^2 + ((-1)*u3) *g^2*h*i^2 + (u2) *f^2*i^3 + (u2) *g^2*i^3 + ((-1)*u2^2+(-1)*u3^2) *g*h^3 + (u2^2+u3^2) *f*h^2*i + ((-1)*u2^2+(-1)*u3^2) *g*h*i^2 + (u2^2+u3^2) *f*i^3 ;
((-1)*u2) *f^2*h^3 + ((-1)*u2) *g^2*h^3 + ((-1)*u3) *f^2*h^2*i + ((-1)*u3) *g^2*h^2*i + ((-1)*u2) *f^2*h*i^2 + ((-1)*u2) *g^2*h*i^2 + ((-1)*u3) *f^2*i^3 + ((-1)*u3) *g^2*i^3 + (u2^2+u3^2) *f*h^3 + (u2^2+u3^2) *g*h^2*i + (u2^2+u3^2) *f*h*i^2 + (u2^2+u3^2) *g*i^3 ;
(u1) *f^2*g*h^2 + (u1) *g^3*h^2 + (u1) *f^2*g*i^2 + (u1) *g^3*i^2 + (u1^2) *f^2*g*h + (u1^2) *g^3*h + ((-1)*u1^2) *f^3*i + ((-1)*u1^2) *f*g^2*i ;
(u1) *f^3*h^2 + (u1) *f*g^2*h^2 + (u1) *f^3*i^2 + (u1) *f*g^2*i^2 + ((-1)*u1^2) *f^3*h + ((-1)*u1^2) *f*g^2*h + ((-1)*u1^2) *f^2*g*i + ((-1)*u1^2) *g^3*i ;
(u3) *f + (u1+(-1)*u2) *g + ((-1)*u1*u3) ;
(u3) *h + (u1+(-1)*u2) *i + ((-1)*u1*u3) ;
(u3) *j + ((-1)*u2) *k ;
(u3) *l + ((-1)*u2) *m ;
((-1)*u1) *o ;
((-1)*u1) *q ;
(1) *k*r + ((-1)) *j*s + ((-1)*u1) *k + (u1) *s ;
(1) *q*r + ((-1)) *p*s + (u3) *p + ((-1)*u2) *q + ((-1)*u3) *r + (u2) *s ;
(1) *i*t + ((-1)) *h*u ;
(1) *o*t + ((-1)) *n*u + (u3) *n + ((-1)*u2) *o + ((-1)*u3) *t + (u2) *u ;
((-1)*u5) *f + (u4) *g ;
((-1)*u5) *l + ((-1)*u1+u4) *m + (u1*u5) ;
];
Certificate
CR:=[
((-2)) *r*t + (1) *t^2 + ((-2)) *s*u + (1) *u^2 + (2*u4) *r + (2*u5) *s + ((-1)*u4^2+(-1)*u5^2) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
C:=[
[
((-2)) *r*t + (1) *t^2 + ((-2)) *s*u + (1) *u^2 + (2*u4) *r + (2*u5) *s + ((-1)*u4^2+(-1)*u5^2) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
(((-1)*u3^3+((-1)*u1^2+(-1)*u2^2+2*u1*u2)*u3)*u5^4+((2*u1^3+(-2)*u2^3+6*u1*u2^2+(-6)*u1^2*u2+(2*u1+(-2)*u2)*u3^2)*u4)*u5^3+((u3^3+(u1^2+u2^2+(-2)*u1*u2)*u3)*u4^2)*u5^2) *i + (((3*u1^2+(-3)*u1*u2)*u3^2)*u5^4+((3*u1*u3^3+((-4)*u1^3+(-4)*u1*u2^2+8*u1^2*u2)*u3)*u4)*u5^3+((((-5)*u1^2+5*u1*u2)*u3^2)*u4^2)*u5^2+(-1)*u1*u3^3*u4^3*u5) ; ((((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^6)*u4^7+((u1^4+u1^2*u2^2+(-2)*u1^3*u2)*u3^7+(2*u1^6+2*u1^2*u2^4+(-8)*u1^3*u2^3+12*u1^4*u2^2+(-8)*u1^5*u2)*u3^5)*u5^7+(((2*u1^3+(-2)*u1^2*u2)*u3^8+((-9)*u1^7+9*u1^2*u2^5+(-45)*u1^3*u2^4+90*u1^4*u2^3+(-90)*u1^5*u2^2+45*u1^6*u2)*u3^4)*u4)*u5^6+((u1^2*u3^9+((-8)*u1^4+(-8)*u1^2*u2^2+16*u1^3*u2)*u3^7+((-18)*u1^6+(-18)*u1^2*u2^4+72*u1^3*u2^3+(-108)*u1^4*u2^2+72*u1^5*u2)*u3^5+(12*u1^8+12*u1^2*u2^6+(-72)*u1^3*u2^5+180*u1^4*u2^4+(-240)*u1^5*u2^3+180*u1^6*u2^2+(-72)*u1^7*u2)*u3^3)*u4^2)*u5^5+((((-8)*u1^3+8*u1^2*u2)*u3^8+((-5)*u1^5+5*u1^2*u2^3+(-15)*u1^3*u2^2+15*u1^4*u2)*u3^6+(34*u1^7+(-34)*u1^2*u2^5+170*u1^3*u2^4+(-340)*u1^4*u2^3+340*u1^5*u2^2+(-170)*u1^6*u2)*u3^4+((-4)*u1^9+4*u1^2*u2^7+(-28)*u1^3*u2^6+84*u1^4*u2^5+(-140)*u1^5*u2^4+140*u1^6*u2^3+(-84)*u1^7*u2^2+28*u1^8*u2)*u3^2)*u4^3)*u5^4+(((-2)*u1^2*u3^9+(9*u1^4+9*u1^2*u2^2+(-18)*u1^3*u2)*u3^7+(34*u1^6+34*u1^2*u2^4+(-136)*u1^3*u2^3+204*u1^4*u2^2+(-136)*u1^5*u2)*u3^5+((-12)*u1^8+(-12)*u1^2*u2^6+72*u1^3*u2^5+(-180)*u1^4*u2^4+240*u1^5*u2^3+(-180)*u1^6*u2^2+72*u1^7*u2)*u3^3)*u4^4)*u5^3+(((6*u1^3+(-6)*u1^2*u2)*u3^8+(14*u1^5+(-14)*u1^2*u2^3+42*u1^3*u2^2+(-42)*u1^4*u2)*u3^6+((-13)*u1^7+13*u1^2*u2^5+(-65)*u1^3*u2^4+130*u1^4*u2^3+(-130)*u1^5*u2^2+65*u1^6*u2)*u3^4)*u4^5)*u5^2+((u1^2*u3^9+(2*u1^4+2*u1^2*u2^2+(-4)*u1^3*u2)*u3^7+((-6)*u1^6+(-6)*u1^2*u2^4+24*u1^3*u2^3+(-36)*u1^4*u2^2+24*u1^5*u2)*u3^5)*u4^6)*u5) *g^2*i^2 + (((2*u1^5+2*u1^3*u2^2+(-4)*u1^4*u2)*u3^7)*u4^7+(((-2)*u1^6+2*u1^3*u2^3+(-6)*u1^4*u2^2+6*u1^5*u2)*u3^6)*u5^7+((((-4)*u1^5+(-4)*u1^3*u2^2+8*u1^4*u2)*u3^7+(10*u1^7+10*u1^3*u2^4+(-40)*u1^4*u2^3+60*u1^5*u2^2+(-40)*u1^6*u2)*u3^5)*u4)*u5^6+((((-2)*u1^4+2*u1^3*u2)*u3^8+(24*u1^6+(-24)*u1^3*u2^3+72*u1^4*u2^2+(-72)*u1^5*u2)*u3^6+((-16)*u1^8+16*u1^3*u2^5+(-80)*u1^4*u2^4+160*u1^5*u2^3+(-160)*u1^6*u2^2+80*u1^7*u2)*u3^4)*u4^2)*u5^5+(((18*u1^5+18*u1^3*u2^2+(-36)*u1^4*u2)*u3^7+((-44)*u1^7+(-44)*u1^3*u2^4+176*u1^4*u2^3+(-264)*u1^5*u2^2+176*u1^6*u2)*u3^5+(8*u1^9+8*u1^3*u2^6+(-48)*u1^4*u2^5+120*u1^5*u2^4+(-160)*u1^6*u2^3+120*u1^7*u2^2+(-48)*u1^8*u2)*u3^3)*u4^3)*u5^4+(((4*u1^4+(-4)*u1^3*u2)*u3^8+((-42)*u1^6+42*u1^3*u2^3+(-126)*u1^4*u2^2+126*u1^5*u2)*u3^6+(24*u1^8+(-24)*u1^3*u2^5+120*u1^4*u2^4+(-240)*u1^5*u2^3+240*u1^6*u2^2+(-120)*u1^7*u2)*u3^4)*u4^4)*u5^3+((((-16)*u1^5+(-16)*u1^3*u2^2+32*u1^4*u2)*u3^7+(26*u1^7+26*u1^3*u2^4+(-104)*u1^4*u2^3+156*u1^5*u2^2+(-104)*u1^6*u2)*u3^5)*u4^5)*u5^2+((((-2)*u1^4+2*u1^3*u2)*u3^8+(12*u1^6+(-12)*u1^3*u2^3+36*u1^4*u2^2+(-36)*u1^5*u2)*u3^6)*u4^6)*u5) *g^2*i + (((u1^5+u1^3*u2^2+(-2)*u1^4*u2)*u3^7)*u4^7+((u1^4+(-1)*u1^3*u2)*u3^8)*u5^7+((u1^3*u3^9+((-6)*u1^5+(-6)*u1^3*u2^2+12*u1^4*u2)*u3^7)*u4)*u5^6+((((-8)*u1^4+8*u1^3*u2)*u3^8+(13*u1^6+(-13)*u1^3*u2^3+39*u1^4*u2^2+(-39)*u1^5*u2)*u3^6)*u4^2)*u5^5+(((-2)*u1^3*u3^9+(21*u1^5+21*u1^3*u2^2+(-42)*u1^4*u2)*u3^7+((-12)*u1^7+(-12)*u1^3*u2^4+48*u1^4*u2^3+(-72)*u1^5*u2^2+48*u1^6*u2)*u3^5)*u4^3)*u5^4+(((9*u1^4+(-9)*u1^3*u2)*u3^8+((-22)*u1^6+22*u1^3*u2^3+(-66)*u1^4*u2^2+66*u1^5*u2)*u3^6+(4*u1^8+(-4)*u1^3*u2^5+20*u1^4*u2^4+(-40)*u1^5*u2^3+40*u1^6*u2^2+(-20)*u1^7*u2)*u3^4)*u4^4)*u5^3+((u1^3*u3^9+((-12)*u1^5+(-12)*u1^3*u2^2+24*u1^4*u2)*u3^7+(8*u1^7+8*u1^3*u2^4+(-32)*u1^4*u2^3+48*u1^5*u2^2+(-32)*u1^6*u2)*u3^5)*u4^5)*u5^2+((((-2)*u1^4+2*u1^3*u2)*u3^8+(5*u1^6+(-5)*u1^3*u2^3+15*u1^4*u2^2+(-15)*u1^5*u2)*u3^6)*u4^6)*u5) *g*i^2 + ((((-1)*u1^5+u1^4*u2)*u3^8)*u4^7+((2*u1^6+2*u1^4*u2^2+(-4)*u1^5*u2)*u3^7+(u1^8+u1^4*u2^4+(-4)*u1^5*u2^3+6*u1^6*u2^2+(-4)*u1^7*u2)*u3^5)*u5^7+(((4*u1^5+(-4)*u1^4*u2)*u3^8+((-7)*u1^7+7*u1^4*u2^3+(-21)*u1^5*u2^2+21*u1^6*u2)*u3^6+((-4)*u1^9+4*u1^4*u2^5+(-20)*u1^5*u2^4+40*u1^6*u2^3+(-40)*u1^7*u2^2+20*u1^8*u2)*u3^4)*u4)*u5^6+((2*u1^4*u3^9+((-21)*u1^6+(-21)*u1^4*u2^2+42*u1^5*u2)*u3^7+(2*u1^8+2*u1^4*u2^4+(-8)*u1^5*u2^3+12*u1^6*u2^2+(-8)*u1^7*u2)*u3^5+(4*u1^10+4*u1^4*u2^6+(-24)*u1^5*u2^5+60*u1^6*u2^4+(-80)*u1^7*u2^3+60*u1^8*u2^2+(-24)*u1^9*u2)*u3^3)*u4^2)*u5^5+((((-17)*u1^5+17*u1^4*u2)*u3^8+(26*u1^7+(-26)*u1^4*u2^3+78*u1^5*u2^2+(-78)*u1^6*u2)*u3^6+(8*u1^9+(-8)*u1^4*u2^5+40*u1^5*u2^4+(-80)*u1^6*u2^3+80*u1^7*u2^2+(-40)*u1^8*u2)*u3^4)*u4^3)*u5^4+(((-4)*u1^4*u3^9+(32*u1^6+32*u1^4*u2^2+(-64)*u1^5*u2)*u3^7+(u1^8+u1^4*u2^4+(-4)*u1^5*u2^3+6*u1^6*u2^2+(-4)*u1^7*u2)*u3^5)*u4^4)*u5^3+(((14*u1^5+(-14)*u1^4*u2)*u3^8+((-7)*u1^7+7*u1^4*u2^3+(-21)*u1^5*u2^2+21*u1^6*u2)*u3^6)*u4^5)*u5^2+((2*u1^4*u3^9+((-5)*u1^6+(-5)*u1^4*u2^2+10*u1^5*u2)*u3^7)*u4^6)*u5) *g^2 + ((((-2)*u1^5+2*u1^4*u2)*u3^8)*u4^7+(((-3)*u1^6+(-3)*u1^4*u2^2+6*u1^5*u2)*u3^7+((-1)*u1^8+(-1)*u1^4*u2^4+4*u1^5*u2^3+(-6)*u1^6*u2^2+4*u1^7*u2)*u3^5)*u5^7+((((-4)*u1^5+4*u1^4*u2)*u3^8+(10*u1^7+(-10)*u1^4*u2^3+30*u1^5*u2^2+(-30)*u1^6*u2)*u3^6+(4*u1^9+(-4)*u1^4*u2^5+20*u1^5*u2^4+(-40)*u1^6*u2^3+40*u1^7*u2^2+(-20)*u1^8*u2)*u3^4)*u4)*u5^6+(((-1)*u1^4*u3^9+(19*u1^6+19*u1^4*u2^2+(-38)*u1^5*u2)*u3^7+((-2)*u1^8+(-2)*u1^4*u2^4+8*u1^5*u2^3+(-12)*u1^6*u2^2+8*u1^7*u2)*u3^5+((-4)*u1^10+(-4)*u1^4*u2^6+24*u1^5*u2^5+(-60)*u1^6*u2^4+80*u1^7*u2^3+(-60)*u1^8*u2^2+24*u1^9*u2)*u3^3)*u4^2)*u5^5+(((10*u1^5+(-10)*u1^4*u2)*u3^8+((-12)*u1^7+12*u1^4*u2^3+(-36)*u1^5*u2^2+36*u1^6*u2)*u3^6+((-12)*u1^9+12*u1^4*u2^5+(-60)*u1^5*u2^4+120*u1^6*u2^3+(-120)*u1^7*u2^2+60*u1^8*u2)*u3^4)*u4^3)*u5^4+((2*u1^4*u3^9+((-9)*u1^6+(-9)*u1^4*u2^2+18*u1^5*u2)*u3^7+((-21)*u1^8+(-21)*u1^4*u2^4+84*u1^5*u2^3+(-126)*u1^6*u2^2+84*u1^7*u2)*u3^5)*u4^4)*u5^3+((((-4)*u1^5+4*u1^4*u2)*u3^8+((-22)*u1^7+22*u1^4*u2^3+(-66)*u1^5*u2^2+66*u1^6*u2)*u3^6)*u4^5)*u5^2+(((-1)*u1^4*u3^9+((-11)*u1^6+(-11)*u1^4*u2^2+22*u1^5*u2)*u3^7)*u4^6)*u5) *g*i + ((u1^4*u3^9+(u1^6+u1^4*u2^2+(-2)*u1^5*u2)*u3^7)*u5^7+((((-4)*u1^5+4*u1^4*u2)*u3^8+((-4)*u1^7+4*u1^4*u2^3+(-12)*u1^5*u2^2+12*u1^6*u2)*u3^6)*u4)*u5^6+(((-1)*u1^4*u3^9+(3*u1^6+3*u1^4*u2^2+(-6)*u1^5*u2)*u3^7+(4*u1^8+4*u1^4*u2^4+(-16)*u1^5*u2^3+24*u1^6*u2^2+(-16)*u1^7*u2)*u3^5)*u4^2)*u5^5+(((-1)*u1^4*u3^9+(3*u1^6+3*u1^4*u2^2+(-6)*u1^5*u2)*u3^7+(4*u1^8+4*u1^4*u2^4+(-16)*u1^5*u2^3+24*u1^6*u2^2+(-16)*u1^7*u2)*u3^5)*u4^4)*u5^3+(((4*u1^5+(-4)*u1^4*u2)*u3^8+(4*u1^7+(-4)*u1^4*u2^3+12*u1^5*u2^2+(-12)*u1^6*u2)*u3^6)*u4^5)*u5^2+((u1^4*u3^9+(u1^6+u1^4*u2^2+(-2)*u1^5*u2)*u3^7)*u4^6)*u5) *i^2 + (u1^5*u3^9*u4^7+((2*u1^6+(-2)*u1^5*u2)*u3^8+((-1)*u1^8+u1^5*u2^3+(-3)*u1^6*u2^2+3*u1^7*u2)*u3^6)*u5^7+((2*u1^5*u3^9+((-11)*u1^7+(-11)*u1^5*u2^2+22*u1^6*u2)*u3^7+(4*u1^9+4*u1^5*u2^4+(-16)*u1^6*u2^3+24*u1^7*u2^2+(-16)*u1^8*u2)*u3^5)*u4)*u5^6+((((-13)*u1^6+13*u1^5*u2)*u3^8+(22*u1^8+(-22)*u1^5*u2^3+66*u1^6*u2^2+(-66)*u1^7*u2)*u3^6+((-4)*u1^10+4*u1^5*u2^5+(-20)*u1^6*u2^4+40*u1^7*u2^3+(-40)*u1^8*u2^2+20*u1^9*u2)*u3^4)*u4^2)*u5^5+(((-3)*u1^5*u3^9+(26*u1^7+26*u1^5*u2^2+(-52)*u1^6*u2)*u3^7+((-16)*u1^9+(-16)*u1^5*u2^4+64*u1^6*u2^3+(-96)*u1^7*u2^2+64*u1^8*u2)*u3^5)*u4^3)*u5^4+(((8*u1^6+(-8)*u1^5*u2)*u3^8+((-17)*u1^8+17*u1^5*u2^3+(-51)*u1^6*u2^2+51*u1^7*u2)*u3^6)*u4^4)*u5^3+((((-3)*u1^7+(-3)*u1^5*u2^2+6*u1^6*u2)*u3^7)*u4^5)*u5^2+(((3*u1^6+(-3)*u1^5*u2)*u3^8)*u4^6)*u5) *g + ((((-3)*u1^6+3*u1^5*u2)*u3^8+(u1^8+(-1)*u1^5*u2^3+3*u1^6*u2^2+(-3)*u1^7*u2)*u3^6)*u5^7+(((-1)*u1^5*u3^9+(15*u1^7+15*u1^5*u2^2+(-30)*u1^6*u2)*u3^7+((-4)*u1^9+(-4)*u1^5*u2^4+16*u1^6*u2^3+(-24)*u1^7*u2^2+16*u1^8*u2)*u3^5)*u4)*u5^6+(((10*u1^6+(-10)*u1^5*u2)*u3^8+((-26)*u1^8+26*u1^5*u2^3+(-78)*u1^6*u2^2+78*u1^7*u2)*u3^6+(4*u1^10+(-4)*u1^5*u2^5+20*u1^6*u2^4+(-40)*u1^7*u2^3+40*u1^8*u2^2+(-20)*u1^9*u2)*u3^4)*u4^2)*u5^5+((2*u1^5*u3^9+((-22)*u1^7+(-22)*u1^5*u2^2+44*u1^6*u2)*u3^7+(16*u1^9+16*u1^5*u2^4+(-64)*u1^6*u2^3+96*u1^7*u2^2+(-64)*u1^8*u2)*u3^5)*u4^3)*u5^4+((((-7)*u1^6+7*u1^5*u2)*u3^8+(13*u1^8+(-13)*u1^5*u2^3+39*u1^6*u2^2+(-39)*u1^7*u2)*u3^6)*u4^4)*u5^3+(((-1)*u1^5*u3^9+(3*u1^7+3*u1^5*u2^2+(-6)*u1^6*u2)*u3^7)*u4^5)*u5^2) *i + (2*u1^6*u3^9*u5^7+((((-8)*u1^7+8*u1^6*u2)*u3^8)*u4)*u5^6+(((-2)*u1^6*u3^9+(8*u1^8+8*u1^6*u2^2+(-16)*u1^7*u2)*u3^7)*u4^2)*u5^5+(((-2)*u1^6*u3^9+(8*u1^8+8*u1^6*u2^2+(-16)*u1^7*u2)*u3^7)*u4^4)*u5^3+(((8*u1^7+(-8)*u1^6*u2)*u3^8)*u4^5)*u5^2+2*u1^6*u3^9*u4^6*u5) ; 0; (u1^2*u3^10*u4^7+((u1^5+(-1)*u1^2*u2^3+3*u1^3*u2^2+(-3)*u1^4*u2)*u3^7)*u5^7+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^8+((-4)*u1^6+(-4)*u1^2*u2^4+16*u1^3*u2^3+(-24)*u1^4*u2^2+16*u1^5*u2)*u3^6)*u4)*u5^6+(((3*u1^3+(-3)*u1^2*u2)*u3^9+((-14)*u1^5+14*u1^2*u2^3+(-42)*u1^3*u2^2+42*u1^4*u2)*u3^7+(4*u1^7+(-4)*u1^2*u2^5+20*u1^3*u2^4+(-40)*u1^4*u2^3+40*u1^5*u2^2+(-20)*u1^6*u2)*u3^5)*u4^2)*u5^5+((u1^2*u3^10+((-18)*u1^4+(-18)*u1^2*u2^2+36*u1^3*u2)*u3^8+(16*u1^6+16*u1^2*u2^4+(-64)*u1^3*u2^3+96*u1^4*u2^2+(-64)*u1^5*u2)*u3^6)*u4^3)*u5^4+((((-10)*u1^3+10*u1^2*u2)*u3^9+(25*u1^5+(-25)*u1^2*u2^3+75*u1^3*u2^2+(-75)*u1^4*u2)*u3^7)*u4^4)*u5^3+(((-2)*u1^2*u3^10+(19*u1^4+19*u1^2*u2^2+(-38)*u1^3*u2)*u3^8)*u4^5)*u5^2+(((7*u1^3+(-7)*u1^2*u2)*u3^9)*u4^6)*u5) *f*g*h^2 ; 0; 0; 0; 0; 0; 0; 0; 0; (((u1^3+(-1)*u1^2*u2)*u3^8)*u4^8+(((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^6)*u5^8+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^7+(5*u1^6+5*u1^2*u2^4+(-20)*u1^3*u2^3+30*u1^4*u2^2+(-20)*u1^5*u2)*u3^5)*u4)*u5^7+((((-3)*u1^3+3*u1^2*u2)*u3^8+(17*u1^5+(-17)*u1^2*u2^3+51*u1^3*u2^2+(-51)*u1^4*u2)*u3^6+((-8)*u1^7+8*u1^2*u2^5+(-40)*u1^3*u2^4+80*u1^4*u2^3+(-80)*u1^5*u2^2+40*u1^6*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^2*u3^9+(21*u1^4+21*u1^2*u2^2+(-42)*u1^3*u2)*u3^7+((-30)*u1^6+(-30)*u1^2*u2^4+120*u1^3*u2^3+(-180)*u1^4*u2^2+120*u1^5*u2)*u3^5+(4*u1^8+4*u1^2*u2^6+(-24)*u1^3*u2^5+60*u1^4*u2^4+(-80)*u1^5*u2^3+60*u1^6*u2^2+(-24)*u1^7*u2)*u3^3)*u4^3)*u5^5+(((11*u1^3+(-11)*u1^2*u2)*u3^8+((-43)*u1^5+43*u1^2*u2^3+(-129)*u1^3*u2^2+129*u1^4*u2)*u3^6+(16*u1^7+(-16)*u1^2*u2^5+80*u1^3*u2^4+(-160)*u1^4*u2^3+160*u1^5*u2^2+(-80)*u1^6*u2)*u3^4)*u4^4)*u5^4+((2*u1^2*u3^9+((-29)*u1^4+(-29)*u1^2*u2^2+58*u1^3*u2)*u3^7+(25*u1^6+25*u1^2*u2^4+(-100)*u1^3*u2^3+150*u1^4*u2^2+(-100)*u1^5*u2)*u3^5)*u4^5)*u5^3+((((-9)*u1^3+9*u1^2*u2)*u3^8+(19*u1^5+(-19)*u1^2*u2^3+57*u1^3*u2^2+(-57)*u1^4*u2)*u3^6)*u4^6)*u5^2+(((-1)*u1^2*u3^9+(7*u1^4+7*u1^2*u2^2+(-14)*u1^3*u2)*u3^7)*u4^7)*u5) *g^3*h + ((((-1)*u1^4+(-1)*u1^2*u2^2+2*u1^3*u2)*u3^7)*u4^8+((u1^6+u1^2*u2^4+(-4)*u1^3*u2^3+6*u1^4*u2^2+(-4)*u1^5*u2)*u3^5)*u5^8+(((3*u1^5+(-3)*u1^2*u2^3+9*u1^3*u2^2+(-9)*u1^4*u2)*u3^6+((-5)*u1^7+5*u1^2*u2^5+(-25)*u1^3*u2^4+50*u1^4*u2^3+(-50)*u1^5*u2^2+25*u1^6*u2)*u3^4)*u4)*u5^7+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^7+((-17)*u1^6+(-17)*u1^2*u2^4+68*u1^3*u2^3+(-102)*u1^4*u2^2+68*u1^5*u2)*u3^5+(8*u1^8+8*u1^2*u2^6+(-48)*u1^3*u2^5+120*u1^4*u2^4+(-160)*u1^5*u2^3+120*u1^6*u2^2+(-48)*u1^7*u2)*u3^3)*u4^2)*u5^6+(((u1^3+(-1)*u1^2*u2)*u3^8+((-21)*u1^5+21*u1^2*u2^3+(-63)*u1^3*u2^2+63*u1^4*u2)*u3^6+(30*u1^7+(-30)*u1^2*u2^5+150*u1^3*u2^4+(-300)*u1^4*u2^3+300*u1^5*u2^2+(-150)*u1^6*u2)*u3^4+((-4)*u1^9+4*u1^2*u2^7+(-28)*u1^3*u2^6+84*u1^4*u2^5+(-140)*u1^5*u2^4+140*u1^6*u2^3+(-84)*u1^7*u2^2+28*u1^8*u2)*u3^2)*u4^3)*u5^5+((((-11)*u1^4+(-11)*u1^2*u2^2+22*u1^3*u2)*u3^7+(43*u1^6+43*u1^2*u2^4+(-172)*u1^3*u2^3+258*u1^4*u2^2+(-172)*u1^5*u2)*u3^5+((-16)*u1^8+(-16)*u1^2*u2^6+96*u1^3*u2^5+(-240)*u1^4*u2^4+320*u1^5*u2^3+(-240)*u1^6*u2^2+96*u1^7*u2)*u3^3)*u4^4)*u5^4+((((-2)*u1^3+2*u1^2*u2)*u3^8+(29*u1^5+(-29)*u1^2*u2^3+87*u1^3*u2^2+(-87)*u1^4*u2)*u3^6+((-25)*u1^7+25*u1^2*u2^5+(-125)*u1^3*u2^4+250*u1^4*u2^3+(-250)*u1^5*u2^2+125*u1^6*u2)*u3^4)*u4^5)*u5^3+(((9*u1^4+9*u1^2*u2^2+(-18)*u1^3*u2)*u3^7+((-19)*u1^6+(-19)*u1^2*u2^4+76*u1^3*u2^3+(-114)*u1^4*u2^2+76*u1^5*u2)*u3^5)*u4^6)*u5^2+(((u1^3+(-1)*u1^2*u2)*u3^8+((-7)*u1^5+7*u1^2*u2^3+(-21)*u1^3*u2^2+21*u1^4*u2)*u3^6)*u4^7)*u5) *g^3*i + (((u1^4+(-1)*u1^3*u2)*u3^8)*u4^8+(((-2)*u1^6+2*u1^3*u2^3+(-6)*u1^4*u2^2+6*u1^5*u2)*u3^6+((-1)*u1^8+u1^3*u2^5+(-5)*u1^4*u2^4+10*u1^5*u2^3+(-10)*u1^6*u2^2+5*u1^7*u2)*u3^4)*u5^8+((((-6)*u1^5+(-6)*u1^3*u2^2+12*u1^4*u2)*u3^7+(6*u1^7+6*u1^3*u2^4+(-24)*u1^4*u2^3+36*u1^5*u2^2+(-24)*u1^6*u2)*u3^5+(4*u1^9+4*u1^3*u2^6+(-24)*u1^4*u2^5+60*u1^5*u2^4+(-80)*u1^6*u2^3+60*u1^7*u2^2+(-24)*u1^8*u2)*u3^3)*u4)*u5^7+((((-6)*u1^4+6*u1^3*u2)*u3^8+(28*u1^6+(-28)*u1^3*u2^3+84*u1^4*u2^2+(-84)*u1^5*u2)*u3^6+(2*u1^8+(-2)*u1^3*u2^5+10*u1^4*u2^4+(-20)*u1^5*u2^3+20*u1^6*u2^2+(-10)*u1^7*u2)*u3^4+((-4)*u1^10+4*u1^3*u2^7+(-28)*u1^4*u2^6+84*u1^5*u2^5+(-140)*u1^6*u2^4+140*u1^7*u2^3+(-84)*u1^8*u2^2+28*u1^9*u2)*u3^2)*u4^2)*u5^6+(((-2)*u1^3*u3^9+(38*u1^5+38*u1^3*u2^2+(-76)*u1^4*u2)*u3^7+((-28)*u1^7+(-28)*u1^3*u2^4+112*u1^4*u2^3+(-168)*u1^5*u2^2+112*u1^6*u2)*u3^5+((-12)*u1^9+(-12)*u1^3*u2^6+72*u1^4*u2^5+(-180)*u1^5*u2^4+240*u1^6*u2^3+(-180)*u1^7*u2^2+72*u1^8*u2)*u3^3)*u4^3)*u5^5+(((21*u1^4+(-21)*u1^3*u2)*u3^8+((-58)*u1^6+58*u1^3*u2^3+(-174)*u1^4*u2^2+174*u1^5*u2)*u3^6+((-9)*u1^8+9*u1^3*u2^5+(-45)*u1^4*u2^4+90*u1^5*u2^3+(-90)*u1^6*u2^2+45*u1^7*u2)*u3^4)*u4^4)*u5^4+((4*u1^3*u3^9+((-46)*u1^5+(-46)*u1^3*u2^2+92*u1^4*u2)*u3^7+(6*u1^7+6*u1^3*u2^4+(-24)*u1^4*u2^3+36*u1^5*u2^2+(-24)*u1^6*u2)*u3^5)*u4^5)*u5^3+((((-16)*u1^4+16*u1^3*u2)*u3^8+(12*u1^6+(-12)*u1^3*u2^3+36*u1^4*u2^2+(-36)*u1^5*u2)*u3^6)*u4^6)*u5^2+(((-2)*u1^3*u3^9+(6*u1^5+6*u1^3*u2^2+(-12)*u1^4*u2)*u3^7)*u4^7)*u5) *g^3 + ((-1)*u1^3*u3^9*u4^8+((((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^6)*u4)*u5^7+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^7+(4*u1^7+4*u1^3*u2^4+(-16)*u1^4*u2^3+24*u1^5*u2^2+(-16)*u1^6*u2)*u3^5)*u4^2)*u5^6+((((-3)*u1^4+3*u1^3*u2)*u3^8+(14*u1^6+(-14)*u1^3*u2^3+42*u1^4*u2^2+(-42)*u1^5*u2)*u3^6+((-4)*u1^8+4*u1^3*u2^5+(-20)*u1^4*u2^4+40*u1^5*u2^3+(-40)*u1^6*u2^2+20*u1^7*u2)*u3^4)*u4^3)*u5^5+(((-1)*u1^3*u3^9+(18*u1^5+18*u1^3*u2^2+(-36)*u1^4*u2)*u3^7+((-16)*u1^7+(-16)*u1^3*u2^4+64*u1^4*u2^3+(-96)*u1^5*u2^2+64*u1^6*u2)*u3^5)*u4^4)*u5^4+(((10*u1^4+(-10)*u1^3*u2)*u3^8+((-25)*u1^6+25*u1^3*u2^3+(-75)*u1^4*u2^2+75*u1^5*u2)*u3^6)*u4^5)*u5^3+((2*u1^3*u3^9+((-19)*u1^5+(-19)*u1^3*u2^2+38*u1^4*u2)*u3^7)*u4^6)*u5^2+((((-7)*u1^4+7*u1^3*u2)*u3^8)*u4^7)*u5) *g^2*h + (((u1^4+(-1)*u1^3*u2)*u3^8)*u4^8+(((u1^7+u1^3*u2^4+(-4)*u1^4*u2^3+6*u1^5*u2^2+(-4)*u1^6*u2)*u3^5)*u4)*u5^7+(((3*u1^6+(-3)*u1^3*u2^3+9*u1^4*u2^2+(-9)*u1^5*u2)*u3^6+((-4)*u1^8+4*u1^3*u2^5+(-20)*u1^4*u2^4+40*u1^5*u2^3+(-40)*u1^6*u2^2+20*u1^7*u2)*u3^4)*u4^2)*u5^6+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^7+((-14)*u1^7+(-14)*u1^3*u2^4+56*u1^4*u2^3+(-84)*u1^5*u2^2+56*u1^6*u2)*u3^5+(4*u1^9+4*u1^3*u2^6+(-24)*u1^4*u2^5+60*u1^5*u2^4+(-80)*u1^6*u2^3+60*u1^7*u2^2+(-24)*u1^8*u2)*u3^3)*u4^3)*u5^5+(((u1^4+(-1)*u1^3*u2)*u3^8+((-18)*u1^6+18*u1^3*u2^3+(-54)*u1^4*u2^2+54*u1^5*u2)*u3^6+(16*u1^8+(-16)*u1^3*u2^5+80*u1^4*u2^4+(-160)*u1^5*u2^3+160*u1^6*u2^2+(-80)*u1^7*u2)*u3^4)*u4^4)*u5^4+((((-10)*u1^5+(-10)*u1^3*u2^2+20*u1^4*u2)*u3^7+(25*u1^7+25*u1^3*u2^4+(-100)*u1^4*u2^3+150*u1^5*u2^2+(-100)*u1^6*u2)*u3^5)*u4^5)*u5^3+((((-2)*u1^4+2*u1^3*u2)*u3^8+(19*u1^6+(-19)*u1^3*u2^3+57*u1^4*u2^2+(-57)*u1^5*u2)*u3^6)*u4^6)*u5^2+(((7*u1^5+7*u1^3*u2^2+(-14)*u1^4*u2)*u3^7)*u4^7)*u5) *g^2*i + ((-1)*u1^4*u3^9*u4^8+((2*u1^8+2*u1^4*u2^4+(-8)*u1^5*u2^3+12*u1^6*u2^2+(-8)*u1^7*u2)*u3^5)*u5^8+(((5*u1^7+(-5)*u1^4*u2^3+15*u1^5*u2^2+(-15)*u1^6*u2)*u3^6+((-8)*u1^9+8*u1^4*u2^5+(-40)*u1^5*u2^4+80*u1^6*u2^3+(-80)*u1^7*u2^2+40*u1^8*u2)*u3^4)*u4)*u5^7+(((3*u1^6+3*u1^4*u2^2+(-6)*u1^5*u2)*u3^7+((-24)*u1^8+(-24)*u1^4*u2^4+96*u1^5*u2^3+(-144)*u1^6*u2^2+96*u1^7*u2)*u3^5+(8*u1^10+8*u1^4*u2^6+(-48)*u1^5*u2^5+120*u1^6*u2^4+(-160)*u1^7*u2^3+120*u1^8*u2^2+(-48)*u1^9*u2)*u3^3)*u4^2)*u5^6+((((-1)*u1^5+u1^4*u2)*u3^8+((-22)*u1^7+22*u1^4*u2^3+(-66)*u1^5*u2^2+66*u1^6*u2)*u3^6+(28*u1^9+(-28)*u1^4*u2^5+140*u1^5*u2^4+(-280)*u1^6*u2^3+280*u1^7*u2^2+(-140)*u1^8*u2)*u3^4)*u4^3)*u5^5+(((-1)*u1^4*u3^9+((-2)*u1^6+(-2)*u1^4*u2^2+4*u1^5*u2)*u3^7+(34*u1^8+34*u1^4*u2^4+(-136)*u1^5*u2^3+204*u1^6*u2^2+(-136)*u1^7*u2)*u3^5)*u4^4)*u5^4+(((6*u1^5+(-6)*u1^4*u2)*u3^8+(13*u1^7+(-13)*u1^4*u2^3+39*u1^5*u2^2+(-39)*u1^6*u2)*u3^6)*u4^5)*u5^3+((2*u1^4*u3^9+((-5)*u1^6+(-5)*u1^4*u2^2+10*u1^5*u2)*u3^7)*u4^6)*u5^2+((((-5)*u1^5+5*u1^4*u2)*u3^8)*u4^7)*u5) *g^2 + ((((-1)*u1^8+u1^5*u2^3+(-3)*u1^6*u2^2+3*u1^7*u2)*u3^6)*u5^8+((((-3)*u1^7+(-3)*u1^5*u2^2+6*u1^6*u2)*u3^7+(4*u1^9+4*u1^5*u2^4+(-16)*u1^6*u2^3+24*u1^7*u2^2+(-16)*u1^8*u2)*u3^5)*u4)*u5^7+((((-3)*u1^6+3*u1^5*u2)*u3^8+(14*u1^8+(-14)*u1^5*u2^3+42*u1^6*u2^2+(-42)*u1^7*u2)*u3^6+((-4)*u1^10+4*u1^5*u2^5+(-20)*u1^6*u2^4+40*u1^7*u2^3+(-40)*u1^8*u2^2+20*u1^9*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^5*u3^9+(18*u1^7+18*u1^5*u2^2+(-36)*u1^6*u2)*u3^7+((-16)*u1^9+(-16)*u1^5*u2^4+64*u1^6*u2^3+(-96)*u1^7*u2^2+64*u1^8*u2)*u3^5)*u4^3)*u5^5+(((10*u1^6+(-10)*u1^5*u2)*u3^8+((-25)*u1^8+25*u1^5*u2^3+(-75)*u1^6*u2^2+75*u1^7*u2)*u3^6)*u4^4)*u5^4+((2*u1^5*u3^9+((-19)*u1^7+(-19)*u1^5*u2^2+38*u1^6*u2)*u3^7)*u4^5)*u5^3+((((-7)*u1^6+7*u1^5*u2)*u3^8)*u4^6)*u5^2+(-1)*u1^5*u3^9*u4^7*u5) *g ; ((-1)*u1^2*u3^9*u4^8+((((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^6)*u4)*u5^7+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^7+(4*u1^6+4*u1^2*u2^4+(-16)*u1^3*u2^3+24*u1^4*u2^2+(-16)*u1^5*u2)*u3^5)*u4^2)*u5^6+((((-3)*u1^3+3*u1^2*u2)*u3^8+(14*u1^5+(-14)*u1^2*u2^3+42*u1^3*u2^2+(-42)*u1^4*u2)*u3^6+((-4)*u1^7+4*u1^2*u2^5+(-20)*u1^3*u2^4+40*u1^4*u2^3+(-40)*u1^5*u2^2+20*u1^6*u2)*u3^4)*u4^3)*u5^5+(((-1)*u1^2*u3^9+(18*u1^4+18*u1^2*u2^2+(-36)*u1^3*u2)*u3^7+((-16)*u1^6+(-16)*u1^2*u2^4+64*u1^3*u2^3+(-96)*u1^4*u2^2+64*u1^5*u2)*u3^5)*u4^4)*u5^4+(((10*u1^3+(-10)*u1^2*u2)*u3^8+((-25)*u1^5+25*u1^2*u2^3+(-75)*u1^3*u2^2+75*u1^4*u2)*u3^6)*u4^5)*u5^3+((2*u1^2*u3^9+((-19)*u1^4+(-19)*u1^2*u2^2+38*u1^3*u2)*u3^7)*u4^6)*u5^2+((((-7)*u1^3+7*u1^2*u2)*u3^8)*u4^7)*u5) *g^2*h^2 + ((((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^6)*u5^8+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^7+(4*u1^6+4*u1^2*u2^4+(-16)*u1^3*u2^3+24*u1^4*u2^2+(-16)*u1^5*u2)*u3^5)*u4)*u5^7+((((-3)*u1^3+3*u1^2*u2)*u3^8+(14*u1^5+(-14)*u1^2*u2^3+42*u1^3*u2^2+(-42)*u1^4*u2)*u3^6+((-4)*u1^7+4*u1^2*u2^5+(-20)*u1^3*u2^4+40*u1^4*u2^3+(-40)*u1^5*u2^2+20*u1^6*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^2*u3^9+(18*u1^4+18*u1^2*u2^2+(-36)*u1^3*u2)*u3^7+((-16)*u1^6+(-16)*u1^2*u2^4+64*u1^3*u2^3+(-96)*u1^4*u2^2+64*u1^5*u2)*u3^5)*u4^3)*u5^5+(((10*u1^3+(-10)*u1^2*u2)*u3^8+((-25)*u1^5+25*u1^2*u2^3+(-75)*u1^3*u2^2+75*u1^4*u2)*u3^6)*u4^4)*u5^4+((2*u1^2*u3^9+((-19)*u1^4+(-19)*u1^2*u2^2+38*u1^3*u2)*u3^7)*u4^5)*u5^3+((((-7)*u1^3+7*u1^2*u2)*u3^8)*u4^6)*u5^2+(-1)*u1^2*u3^9*u4^7*u5) *f*g*i^2 + (((u1^6+u1^2*u2^4+(-4)*u1^3*u2^3+6*u1^4*u2^2+(-4)*u1^5*u2)*u3^5)*u5^8+(((3*u1^5+(-3)*u1^2*u2^3+9*u1^3*u2^2+(-9)*u1^4*u2)*u3^6+((-4)*u1^7+4*u1^2*u2^5+(-20)*u1^3*u2^4+40*u1^4*u2^3+(-40)*u1^5*u2^2+20*u1^6*u2)*u3^4)*u4)*u5^7+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^7+((-14)*u1^6+(-14)*u1^2*u2^4+56*u1^3*u2^3+(-84)*u1^4*u2^2+56*u1^5*u2)*u3^5+(4*u1^8+4*u1^2*u2^6+(-24)*u1^3*u2^5+60*u1^4*u2^4+(-80)*u1^5*u2^3+60*u1^6*u2^2+(-24)*u1^7*u2)*u3^3)*u4^2)*u5^6+(((u1^3+(-1)*u1^2*u2)*u3^8+((-18)*u1^5+18*u1^2*u2^3+(-54)*u1^3*u2^2+54*u1^4*u2)*u3^6+(16*u1^7+(-16)*u1^2*u2^5+80*u1^3*u2^4+(-160)*u1^4*u2^3+160*u1^5*u2^2+(-80)*u1^6*u2)*u3^4)*u4^3)*u5^5+((((-10)*u1^4+(-10)*u1^2*u2^2+20*u1^3*u2)*u3^7+(25*u1^6+25*u1^2*u2^4+(-100)*u1^3*u2^3+150*u1^4*u2^2+(-100)*u1^5*u2)*u3^5)*u4^4)*u5^4+((((-2)*u1^3+2*u1^2*u2)*u3^8+(19*u1^5+(-19)*u1^2*u2^3+57*u1^3*u2^2+(-57)*u1^4*u2)*u3^6)*u4^5)*u5^3+(((7*u1^4+7*u1^2*u2^2+(-14)*u1^3*u2)*u3^7)*u4^6)*u5^2+(((u1^3+(-1)*u1^2*u2)*u3^8)*u4^7)*u5) *g^2*i^2 + ((((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^6)*u5^8+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^7+(4*u1^7+4*u1^3*u2^4+(-16)*u1^4*u2^3+24*u1^5*u2^2+(-16)*u1^6*u2)*u3^5)*u4)*u5^7+((((-3)*u1^4+3*u1^3*u2)*u3^8+(14*u1^6+(-14)*u1^3*u2^3+42*u1^4*u2^2+(-42)*u1^5*u2)*u3^6+((-4)*u1^8+4*u1^3*u2^5+(-20)*u1^4*u2^4+40*u1^5*u2^3+(-40)*u1^6*u2^2+20*u1^7*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^3*u3^9+(18*u1^5+18*u1^3*u2^2+(-36)*u1^4*u2)*u3^7+((-16)*u1^7+(-16)*u1^3*u2^4+64*u1^4*u2^3+(-96)*u1^5*u2^2+64*u1^6*u2)*u3^5)*u4^3)*u5^5+(((10*u1^4+(-10)*u1^3*u2)*u3^8+((-25)*u1^6+25*u1^3*u2^3+(-75)*u1^4*u2^2+75*u1^5*u2)*u3^6)*u4^4)*u5^4+((2*u1^3*u3^9+((-19)*u1^5+(-19)*u1^3*u2^2+38*u1^4*u2)*u3^7)*u4^5)*u5^3+((((-7)*u1^4+7*u1^3*u2)*u3^8)*u4^6)*u5^2+(-1)*u1^3*u3^9*u4^7*u5) *f*g*h + (((u1^7+u1^3*u2^4+(-4)*u1^4*u2^3+6*u1^5*u2^2+(-4)*u1^6*u2)*u3^5)*u5^8+(((3*u1^6+(-3)*u1^3*u2^3+9*u1^4*u2^2+(-9)*u1^5*u2)*u3^6+((-4)*u1^8+4*u1^3*u2^5+(-20)*u1^4*u2^4+40*u1^5*u2^3+(-40)*u1^6*u2^2+20*u1^7*u2)*u3^4)*u4)*u5^7+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^7+((-14)*u1^7+(-14)*u1^3*u2^4+56*u1^4*u2^3+(-84)*u1^5*u2^2+56*u1^6*u2)*u3^5+(4*u1^9+4*u1^3*u2^6+(-24)*u1^4*u2^5+60*u1^5*u2^4+(-80)*u1^6*u2^3+60*u1^7*u2^2+(-24)*u1^8*u2)*u3^3)*u4^2)*u5^6+(((u1^4+(-1)*u1^3*u2)*u3^8+((-18)*u1^6+18*u1^3*u2^3+(-54)*u1^4*u2^2+54*u1^5*u2)*u3^6+(16*u1^8+(-16)*u1^3*u2^5+80*u1^4*u2^4+(-160)*u1^5*u2^3+160*u1^6*u2^2+(-80)*u1^7*u2)*u3^4)*u4^3)*u5^5+((((-10)*u1^5+(-10)*u1^3*u2^2+20*u1^4*u2)*u3^7+(25*u1^7+25*u1^3*u2^4+(-100)*u1^4*u2^3+150*u1^5*u2^2+(-100)*u1^6*u2)*u3^5)*u4^4)*u5^4+((((-2)*u1^4+2*u1^3*u2)*u3^8+(19*u1^6+(-19)*u1^3*u2^3+57*u1^4*u2^2+(-57)*u1^5*u2)*u3^6)*u4^5)*u5^3+(((7*u1^5+7*u1^3*u2^2+(-14)*u1^4*u2)*u3^7)*u4^6)*u5^2+(((u1^4+(-1)*u1^3*u2)*u3^8)*u4^7)*u5) *g^2*h + (((u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^6)*u5^8+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^7+((-4)*u1^7+(-4)*u1^3*u2^4+16*u1^4*u2^3+(-24)*u1^5*u2^2+16*u1^6*u2)*u3^5)*u4)*u5^7+(((3*u1^4+(-3)*u1^3*u2)*u3^8+((-14)*u1^6+14*u1^3*u2^3+(-42)*u1^4*u2^2+42*u1^5*u2)*u3^6+(4*u1^8+(-4)*u1^3*u2^5+20*u1^4*u2^4+(-40)*u1^5*u2^3+40*u1^6*u2^2+(-20)*u1^7*u2)*u3^4)*u4^2)*u5^6+((u1^3*u3^9+((-18)*u1^5+(-18)*u1^3*u2^2+36*u1^4*u2)*u3^7+(16*u1^7+16*u1^3*u2^4+(-64)*u1^4*u2^3+96*u1^5*u2^2+(-64)*u1^6*u2)*u3^5)*u4^3)*u5^5+((((-10)*u1^4+10*u1^3*u2)*u3^8+(25*u1^6+(-25)*u1^3*u2^3+75*u1^4*u2^2+(-75)*u1^5*u2)*u3^6)*u4^4)*u5^4+(((-2)*u1^3*u3^9+(19*u1^5+19*u1^3*u2^2+(-38)*u1^4*u2)*u3^7)*u4^5)*u5^3+(((7*u1^4+(-7)*u1^3*u2)*u3^8)*u4^6)*u5^2+u1^3*u3^9*u4^7*u5) *f^2*i + ((((-1)*u1^7+(-1)*u1^3*u2^4+4*u1^4*u2^3+(-6)*u1^5*u2^2+4*u1^6*u2)*u3^5)*u5^8+((((-3)*u1^6+3*u1^3*u2^3+(-9)*u1^4*u2^2+9*u1^5*u2)*u3^6+(4*u1^8+(-4)*u1^3*u2^5+20*u1^4*u2^4+(-40)*u1^5*u2^3+40*u1^6*u2^2+(-20)*u1^7*u2)*u3^4)*u4)*u5^7+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^7+(14*u1^7+14*u1^3*u2^4+(-56)*u1^4*u2^3+84*u1^5*u2^2+(-56)*u1^6*u2)*u3^5+((-4)*u1^9+(-4)*u1^3*u2^6+24*u1^4*u2^5+(-60)*u1^5*u2^4+80*u1^6*u2^3+(-60)*u1^7*u2^2+24*u1^8*u2)*u3^3)*u4^2)*u5^6+((((-1)*u1^4+u1^3*u2)*u3^8+(18*u1^6+(-18)*u1^3*u2^3+54*u1^4*u2^2+(-54)*u1^5*u2)*u3^6+((-16)*u1^8+16*u1^3*u2^5+(-80)*u1^4*u2^4+160*u1^5*u2^3+(-160)*u1^6*u2^2+80*u1^7*u2)*u3^4)*u4^3)*u5^5+(((10*u1^5+10*u1^3*u2^2+(-20)*u1^4*u2)*u3^7+((-25)*u1^7+(-25)*u1^3*u2^4+100*u1^4*u2^3+(-150)*u1^5*u2^2+100*u1^6*u2)*u3^5)*u4^4)*u5^4+(((2*u1^4+(-2)*u1^3*u2)*u3^8+((-19)*u1^6+19*u1^3*u2^3+(-57)*u1^4*u2^2+57*u1^5*u2)*u3^6)*u4^5)*u5^3+((((-7)*u1^5+(-7)*u1^3*u2^2+14*u1^4*u2)*u3^7)*u4^6)*u5^2+((((-1)*u1^4+u1^3*u2)*u3^8)*u4^7)*u5) *f*g*i + (((u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^6+(u1^8+(-1)*u1^3*u2^5+5*u1^4*u2^4+(-10)*u1^5*u2^3+10*u1^6*u2^2+(-5)*u1^7*u2)*u3^4)*u5^8+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^7+((-1)*u1^7+(-1)*u1^3*u2^4+4*u1^4*u2^3+(-6)*u1^5*u2^2+4*u1^6*u2)*u3^5+((-4)*u1^9+(-4)*u1^3*u2^6+24*u1^4*u2^5+(-60)*u1^5*u2^4+80*u1^6*u2^3+(-60)*u1^7*u2^2+24*u1^8*u2)*u3^3)*u4)*u5^7+(((3*u1^4+(-3)*u1^3*u2)*u3^8+((-11)*u1^6+11*u1^3*u2^3+(-33)*u1^4*u2^2+33*u1^5*u2)*u3^6+((-10)*u1^8+10*u1^3*u2^5+(-50)*u1^4*u2^4+100*u1^5*u2^3+(-100)*u1^6*u2^2+50*u1^7*u2)*u3^4+(4*u1^10+(-4)*u1^3*u2^7+28*u1^4*u2^6+(-84)*u1^5*u2^5+140*u1^6*u2^4+(-140)*u1^7*u2^3+84*u1^8*u2^2+(-28)*u1^9*u2)*u3^2)*u4^2)*u5^6+((u1^3*u3^9+((-17)*u1^5+(-17)*u1^3*u2^2+34*u1^4*u2)*u3^7+((-2)*u1^7+(-2)*u1^3*u2^4+8*u1^4*u2^3+(-12)*u1^5*u2^2+8*u1^6*u2)*u3^5+(16*u1^9+16*u1^3*u2^6+(-96)*u1^4*u2^5+240*u1^5*u2^4+(-320)*u1^6*u2^3+240*u1^7*u2^2+(-96)*u1^8*u2)*u3^3)*u4^3)*u5^5+((((-10)*u1^4+10*u1^3*u2)*u3^8+(15*u1^6+(-15)*u1^3*u2^3+45*u1^4*u2^2+(-45)*u1^5*u2)*u3^6+(25*u1^8+(-25)*u1^3*u2^5+125*u1^4*u2^4+(-250)*u1^5*u2^3+250*u1^6*u2^2+(-125)*u1^7*u2)*u3^4)*u4^4)*u5^4+(((-2)*u1^3*u3^9+(17*u1^5+17*u1^3*u2^2+(-34)*u1^4*u2)*u3^7+(19*u1^7+19*u1^3*u2^4+(-76)*u1^4*u2^3+114*u1^5*u2^2+(-76)*u1^6*u2)*u3^5)*u4^5)*u5^3+(((7*u1^4+(-7)*u1^3*u2)*u3^8+(7*u1^6+(-7)*u1^3*u2^3+21*u1^4*u2^2+(-21)*u1^5*u2)*u3^6)*u4^6)*u5^2+((u1^3*u3^9+(u1^5+u1^3*u2^2+(-2)*u1^4*u2)*u3^7)*u4^7)*u5) *g^2*i + ((((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^6)*u5^8+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^7+(4*u1^7+4*u1^3*u2^4+(-16)*u1^4*u2^3+24*u1^5*u2^2+(-16)*u1^6*u2)*u3^5)*u4)*u5^7+((((-3)*u1^4+3*u1^3*u2)*u3^8+(14*u1^6+(-14)*u1^3*u2^3+42*u1^4*u2^2+(-42)*u1^5*u2)*u3^6+((-4)*u1^8+4*u1^3*u2^5+(-20)*u1^4*u2^4+40*u1^5*u2^3+(-40)*u1^6*u2^2+20*u1^7*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^3*u3^9+(18*u1^5+18*u1^3*u2^2+(-36)*u1^4*u2)*u3^7+((-16)*u1^7+(-16)*u1^3*u2^4+64*u1^4*u2^3+(-96)*u1^5*u2^2+64*u1^6*u2)*u3^5)*u4^3)*u5^5+(((10*u1^4+(-10)*u1^3*u2)*u3^8+((-25)*u1^6+25*u1^3*u2^3+(-75)*u1^4*u2^2+75*u1^5*u2)*u3^6)*u4^4)*u5^4+((2*u1^3*u3^9+((-19)*u1^5+(-19)*u1^3*u2^2+38*u1^4*u2)*u3^7)*u4^5)*u5^3+((((-7)*u1^4+7*u1^3*u2)*u3^8)*u4^6)*u5^2+(-1)*u1^3*u3^9*u4^7*u5) *g*i^2 + ((((-1)*u1^7+u1^4*u2^3+(-3)*u1^5*u2^2+3*u1^6*u2)*u3^6)*u5^8+((((-3)*u1^6+(-3)*u1^4*u2^2+6*u1^5*u2)*u3^7+(4*u1^8+4*u1^4*u2^4+(-16)*u1^5*u2^3+24*u1^6*u2^2+(-16)*u1^7*u2)*u3^5)*u4)*u5^7+((((-3)*u1^5+3*u1^4*u2)*u3^8+(14*u1^7+(-14)*u1^4*u2^3+42*u1^5*u2^2+(-42)*u1^6*u2)*u3^6+((-4)*u1^9+4*u1^4*u2^5+(-20)*u1^5*u2^4+40*u1^6*u2^3+(-40)*u1^7*u2^2+20*u1^8*u2)*u3^4)*u4^2)*u5^6+(((-1)*u1^4*u3^9+(18*u1^6+18*u1^4*u2^2+(-36)*u1^5*u2)*u3^7+((-16)*u1^8+(-16)*u1^4*u2^4+64*u1^5*u2^3+(-96)*u1^6*u2^2+64*u1^7*u2)*u3^5)*u4^3)*u5^5+(((10*u1^5+(-10)*u1^4*u2)*u3^8+((-25)*u1^7+25*u1^4*u2^3+(-75)*u1^5*u2^2+75*u1^6*u2)*u3^6)*u4^4)*u5^4+((2*u1^4*u3^9+((-19)*u1^6+(-19)*u1^4*u2^2+38*u1^5*u2)*u3^7)*u4^5)*u5^3+((((-7)*u1^5+7*u1^4*u2)*u3^8)*u4^6)*u5^2+(-1)*u1^4*u3^9*u4^7*u5) *g*h + (((u1^7+(-1)*u1^4*u2^3+3*u1^5*u2^2+(-3)*u1^6*u2)*u3^6)*u5^8+(((3*u1^6+3*u1^4*u2^2+(-6)*u1^5*u2)*u3^7+((-4)*u1^8+(-4)*u1^4*u2^4+16*u1^5*u2^3+(-24)*u1^6*u2^2+16*u1^7*u2)*u3^5)*u4)*u5^7+(((3*u1^5+(-3)*u1^4*u2)*u3^8+((-14)*u1^7+14*u1^4*u2^3+(-42)*u1^5*u2^2+42*u1^6*u2)*u3^6+(4*u1^9+(-4)*u1^4*u2^5+20*u1^5*u2^4+(-40)*u1^6*u2^3+40*u1^7*u2^2+(-20)*u1^8*u2)*u3^4)*u4^2)*u5^6+((u1^4*u3^9+((-18)*u1^6+(-18)*u1^4*u2^2+36*u1^5*u2)*u3^7+(16*u1^8+16*u1^4*u2^4+(-64)*u1^5*u2^3+96*u1^6*u2^2+(-64)*u1^7*u2)*u3^5)*u4^3)*u5^5+((((-10)*u1^5+10*u1^4*u2)*u3^8+(25*u1^7+(-25)*u1^4*u2^3+75*u1^5*u2^2+(-75)*u1^6*u2)*u3^6)*u4^4)*u5^4+(((-2)*u1^4*u3^9+(19*u1^6+19*u1^4*u2^2+(-38)*u1^5*u2)*u3^7)*u4^5)*u5^3+(((7*u1^5+(-7)*u1^4*u2)*u3^8)*u4^6)*u5^2+u1^4*u3^9*u4^7*u5) *f*i + ((((-2)*u1^8+(-2)*u1^4*u2^4+8*u1^5*u2^3+(-12)*u1^6*u2^2+8*u1^7*u2)*u3^5)*u5^8+((((-6)*u1^7+6*u1^4*u2^3+(-18)*u1^5*u2^2+18*u1^6*u2)*u3^6+(8*u1^9+(-8)*u1^4*u2^5+40*u1^5*u2^4+(-80)*u1^6*u2^3+80*u1^7*u2^2+(-40)*u1^8*u2)*u3^4)*u4)*u5^7+((((-6)*u1^6+(-6)*u1^4*u2^2+12*u1^5*u2)*u3^7+(28*u1^8+28*u1^4*u2^4+(-112)*u1^5*u2^3+168*u1^6*u2^2+(-112)*u1^7*u2)*u3^5+((-8)*u1^10+(-8)*u1^4*u2^6+48*u1^5*u2^5+(-120)*u1^6*u2^4+160*u1^7*u2^3+(-120)*u1^8*u2^2+48*u1^9*u2)*u3^3)*u4^2)*u5^6+((((-2)*u1^5+2*u1^4*u2)*u3^8+(36*u1^7+(-36)*u1^4*u2^3+108*u1^5*u2^2+(-108)*u1^6*u2)*u3^6+((-32)*u1^9+32*u1^4*u2^5+(-160)*u1^5*u2^4+320*u1^6*u2^3+(-320)*u1^7*u2^2+160*u1^8*u2)*u3^4)*u4^3)*u5^5+(((20*u1^6+20*u1^4*u2^2+(-40)*u1^5*u2)*u3^7+((-50)*u1^8+(-50)*u1^4*u2^4+200*u1^5*u2^3+(-300)*u1^6*u2^2+200*u1^7*u2)*u3^5)*u4^4)*u5^4+(((4*u1^5+(-4)*u1^4*u2)*u3^8+((-38)*u1^7+38*u1^4*u2^3+(-114)*u1^5*u2^2+114*u1^6*u2)*u3^6)*u4^5)*u5^3+((((-14)*u1^6+(-14)*u1^4*u2^2+28*u1^5*u2)*u3^7)*u4^6)*u5^2+((((-2)*u1^5+2*u1^4*u2)*u3^8)*u4^7)*u5) *g*i + (((u1^8+(-1)*u1^5*u2^3+3*u1^6*u2^2+(-3)*u1^7*u2)*u3^6)*u5^8+(((3*u1^7+3*u1^5*u2^2+(-6)*u1^6*u2)*u3^7+((-4)*u1^9+(-4)*u1^5*u2^4+16*u1^6*u2^3+(-24)*u1^7*u2^2+16*u1^8*u2)*u3^5)*u4)*u5^7+(((3*u1^6+(-3)*u1^5*u2)*u3^8+((-14)*u1^8+14*u1^5*u2^3+(-42)*u1^6*u2^2+42*u1^7*u2)*u3^6+(4*u1^10+(-4)*u1^5*u2^5+20*u1^6*u2^4+(-40)*u1^7*u2^3+40*u1^8*u2^2+(-20)*u1^9*u2)*u3^4)*u4^2)*u5^6+((u1^5*u3^9+((-18)*u1^7+(-18)*u1^5*u2^2+36*u1^6*u2)*u3^7+(16*u1^9+16*u1^5*u2^4+(-64)*u1^6*u2^3+96*u1^7*u2^2+(-64)*u1^8*u2)*u3^5)*u4^3)*u5^5+((((-10)*u1^6+10*u1^5*u2)*u3^8+(25*u1^8+(-25)*u1^5*u2^3+75*u1^6*u2^2+(-75)*u1^7*u2)*u3^6)*u4^4)*u5^4+(((-2)*u1^5*u3^9+(19*u1^7+19*u1^5*u2^2+(-38)*u1^6*u2)*u3^7)*u4^5)*u5^3+(((7*u1^6+(-7)*u1^5*u2)*u3^8)*u4^6)*u5^2+u1^5*u3^9*u4^7*u5) *i ; 0; (((u1^4+(-1)*u1*u2^3+3*u1^2*u2^2+(-3)*u1^3*u2)*u3^7)*u5^8+(((3*u1^3+3*u1*u2^2+(-6)*u1^2*u2)*u3^8+((-4)*u1^5+(-4)*u1*u2^4+16*u1^2*u2^3+(-24)*u1^3*u2^2+16*u1^4*u2)*u3^6)*u4)*u5^7+(((3*u1^2+(-3)*u1*u2)*u3^9+((-14)*u1^4+14*u1*u2^3+(-42)*u1^2*u2^2+42*u1^3*u2)*u3^7+(4*u1^6+(-4)*u1*u2^5+20*u1^2*u2^4+(-40)*u1^3*u2^3+40*u1^4*u2^2+(-20)*u1^5*u2)*u3^5)*u4^2)*u5^6+((u1*u3^10+((-18)*u1^3+(-18)*u1*u2^2+36*u1^2*u2)*u3^8+(16*u1^5+16*u1*u2^4+(-64)*u1^2*u2^3+96*u1^3*u2^2+(-64)*u1^4*u2)*u3^6)*u4^3)*u5^5+((((-10)*u1^2+10*u1*u2)*u3^9+(25*u1^4+(-25)*u1*u2^3+75*u1^2*u2^2+(-75)*u1^3*u2)*u3^7)*u4^4)*u5^4+(((-2)*u1*u3^10+(19*u1^3+19*u1*u2^2+(-38)*u1^2*u2)*u3^8)*u4^5)*u5^3+(((7*u1^2+(-7)*u1*u2)*u3^9)*u4^6)*u5^2+u1*u3^10*u4^7*u5) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
((u1*u3^6+(2*u1^3+2*u1*u2^2+(-4)*u1^2*u2)*u3^4)*u4^3+((u1^4+(-1)*u1*u2^3+3*u1^2*u2^2+(-3)*u1^3*u2)*u3^3+(2*u1^6+(-2)*u1*u2^5+10*u1^2*u2^4+(-20)*u1^3*u2^3+20*u1^4*u2^2+(-10)*u1^5*u2)*u3)*u5^3+(((3*u1^3+3*u1*u2^2+(-6)*u1^2*u2)*u3^4+(6*u1^5+6*u1*u2^4+(-24)*u1^2*u2^3+36*u1^3*u2^2+(-24)*u1^4*u2)*u3^2)*u4)*u5^2+(((3*u1^2+(-3)*u1*u2)*u3^5+(6*u1^4+(-6)*u1*u2^3+18*u1^2*u2^2+(-18)*u1^3*u2)*u3^3)*u4^2)*u5) *g^2*i^2 + ((((-2)*u1^3+2*u1^2*u2)*u3^5)*u4^3+(u1^8+u1^2*u2^6+(-6)*u1^3*u2^5+15*u1^4*u2^4+(-20)*u1^5*u2^3+15*u1^6*u2^2+(-6)*u1^7*u2+(u1^4+u1^2*u2^2+(-2)*u1^3*u2)*u3^4)*u5^3+(((2*u1^3+(-2)*u1^2*u2)*u3^5+((-2)*u1^5+2*u1^2*u2^3+(-6)*u1^3*u2^2+6*u1^4*u2)*u3^3+(2*u1^7+(-2)*u1^2*u2^5+10*u1^3*u2^4+(-20)*u1^4*u2^3+20*u1^5*u2^2+(-10)*u1^6*u2)*u3)*u4)*u5^2+((u1^2*u3^6+((-4)*u1^4+(-4)*u1^2*u2^2+8*u1^3*u2)*u3^4+(u1^6+u1^2*u2^4+(-4)*u1^3*u2^3+6*u1^4*u2^2+(-4)*u1^5*u2)*u3^2)*u4^2)*u5) *g^2*i + ((((-2)*u1^3+2*u1^2*u2)*u3^5)*u4^3+(((-2)*u1^6+(-2)*u1^2*u2^4+8*u1^3*u2^3+(-12)*u1^4*u2^2+8*u1^5*u2)*u3^2)*u5^3+((((-6)*u1^5+6*u1^2*u2^3+(-18)*u1^3*u2^2+18*u1^4*u2)*u3^3)*u4)*u5^2+((((-6)*u1^4+(-6)*u1^2*u2^2+12*u1^3*u2)*u3^4)*u4^2)*u5) *g*i^2 + ((2*u1^3*u3^6+(u1^5+u1^3*u2^2+(-2)*u1^4*u2)*u3^4)*u4^3+(((-1)*u1^8+u1^3*u2^5+(-5)*u1^4*u2^4+10*u1^5*u2^3+(-10)*u1^6*u2^2+5*u1^7*u2)*u3)*u5^3+(((2*u1^5+2*u1^3*u2^2+(-4)*u1^4*u2)*u3^4+((-1)*u1^7+(-1)*u1^3*u2^4+4*u1^4*u2^3+(-6)*u1^5*u2^2+4*u1^6*u2)*u3^2)*u4)*u5^2+(((4*u1^4+(-4)*u1^3*u2)*u3^5+(u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^3)*u4^2)*u5) *g^2 + (((-1)*u1^3*u3^6+((-1)*u1^5+(-1)*u1^3*u2^2+2*u1^4*u2)*u3^4)*u4^3+((u1^4+(-1)*u1^3*u2)*u3^5+((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^3+((-2)*u1^8+2*u1^3*u2^5+(-10)*u1^4*u2^4+20*u1^5*u2^3+(-20)*u1^6*u2^2+10*u1^7*u2)*u3)*u5^3+((u1^3*u3^6+((-5)*u1^5+(-5)*u1^3*u2^2+10*u1^4*u2)*u3^4+((-6)*u1^7+(-6)*u1^3*u2^4+24*u1^4*u2^3+(-36)*u1^5*u2^2+24*u1^6*u2)*u3^2)*u4)*u5^2+((((-5)*u1^4+5*u1^3*u2)*u3^5+((-5)*u1^6+5*u1^3*u2^3+(-15)*u1^4*u2^2+15*u1^5*u2)*u3^3)*u4^2)*u5) *g*i + (u1^3*u3^6*u4^3+((u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^3)*u5^3+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^4)*u4)*u5^2+(((3*u1^4+(-3)*u1^3*u2)*u3^5)*u4^2)*u5) *i^2 + ((((-2)*u1^5+2*u1^4*u2)*u3^5)*u4^3+((2*u1^8+2*u1^4*u2^4+(-8)*u1^5*u2^3+12*u1^6*u2^2+(-8)*u1^7*u2)*u3^2)*u5^3+(((2*u1^5+(-2)*u1^4*u2)*u3^5+(4*u1^7+(-4)*u1^4*u2^3+12*u1^5*u2^2+(-12)*u1^6*u2)*u3^3)*u4)*u5^2+2*u1^4*u3^6*u4^2*u5) *g + (((2*u1^5+(-2)*u1^4*u2)*u3^5)*u4^3+(u1^4*u3^6+(u1^8+u1^4*u2^4+(-4)*u1^5*u2^3+6*u1^6*u2^2+(-4)*u1^7*u2)*u3^2)*u5^3+((((-2)*u1^5+2*u1^4*u2)*u3^5+(4*u1^7+(-4)*u1^4*u2^3+12*u1^5*u2^2+(-12)*u1^6*u2)*u3^3)*u4)*u5^2+(((6*u1^6+6*u1^4*u2^2+(-12)*u1^5*u2)*u3^4)*u4^2)*u5) *i + (u1^5*u3^6*u4^3+(((-1)*u1^8+u1^5*u2^3+(-3)*u1^6*u2^2+3*u1^7*u2)*u3^3)*u5^3+((2*u1^5*u3^6+((-3)*u1^7+(-3)*u1^5*u2^2+6*u1^6*u2)*u3^4)*u4)*u5^2+((((-3)*u1^6+3*u1^5*u2)*u3^5)*u4^2)*u5) ; 0; ((-1)*u1*u3^7*u4^3+(((-1)*u1^4+u1*u2^3+(-3)*u1^2*u2^2+3*u1^3*u2)*u3^4)*u5^3+((((-3)*u1^3+(-3)*u1*u2^2+6*u1^2*u2)*u3^5)*u4)*u5^2+((((-3)*u1^2+3*u1*u2)*u3^6)*u4^2)*u5) *f^2*h^2 ; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)*u1*u3^6*u4^4+(((-1)*u1^5+(-1)*u1*u2^4+4*u1^2*u2^3+(-6)*u1^3*u2^2+4*u1^4*u2)*u3^2)*u5^4+((((-4)*u1^4+4*u1*u2^3+(-12)*u1^2*u2^2+12*u1^3*u2)*u3^3)*u4)*u5^3+((((-6)*u1^3+(-6)*u1*u2^2+12*u1^2*u2)*u3^4)*u4^2)*u5^2+((((-4)*u1^2+4*u1*u2)*u3^5)*u4^3)*u5) *g^3*h + (((u1^2+(-1)*u1*u2)*u3^5)*u4^4+((u1^6+(-1)*u1*u2^5+5*u1^2*u2^4+(-10)*u1^3*u2^3+10*u1^4*u2^2+(-5)*u1^5*u2)*u3)*u5^4+(((4*u1^5+4*u1*u2^4+(-16)*u1^2*u2^3+24*u1^3*u2^2+(-16)*u1^4*u2)*u3^2)*u4)*u5^3+(((6*u1^4+(-6)*u1*u2^3+18*u1^2*u2^2+(-18)*u1^3*u2)*u3^3)*u4^2)*u5^2+(((4*u1^3+4*u1*u2^2+(-8)*u1^2*u2)*u3^4)*u4^3)*u5) *g^3*i + (((-2)*u1^2*u3^6+((-1)*u1^4+(-1)*u1^2*u2^2+2*u1^3*u2)*u3^4)*u4^4+(u1^8+u1^2*u2^6+(-6)*u1^3*u2^5+15*u1^4*u2^4+(-20)*u1^5*u2^3+15*u1^6*u2^2+(-6)*u1^7*u2)*u5^4+((((-2)*u1^5+2*u1^2*u2^3+(-6)*u1^3*u2^2+6*u1^4*u2)*u3^3+(2*u1^7+(-2)*u1^2*u2^5+10*u1^3*u2^4+(-20)*u1^4*u2^3+20*u1^5*u2^2+(-10)*u1^6*u2)*u3)*u4)*u5^3+((((-6)*u1^4+(-6)*u1^2*u2^2+12*u1^3*u2)*u3^4)*u4^2)*u5^2+((((-6)*u1^3+6*u1^2*u2)*u3^5+((-2)*u1^5+2*u1^2*u2^3+(-6)*u1^3*u2^2+6*u1^4*u2)*u3^3)*u4^3)*u5) *g^3 + (((u1^5+(-1)*u1^2*u2^3+3*u1^3*u2^2+(-3)*u1^4*u2)*u3^3)*u5^4+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^4)*u4)*u5^3+(((3*u1^3+(-3)*u1^2*u2)*u3^5)*u4^2)*u5^2+u1^2*u3^6*u4^3*u5) *g^2*h + ((((-1)*u1^6+(-1)*u1^2*u2^4+4*u1^3*u2^3+(-6)*u1^4*u2^2+4*u1^5*u2)*u3^2)*u5^4+((((-3)*u1^5+3*u1^2*u2^3+(-9)*u1^3*u2^2+9*u1^4*u2)*u3^3)*u4)*u5^3+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^4)*u4^2)*u5^2+((((-1)*u1^3+u1^2*u2)*u3^5)*u4^3)*u5) *g^2*i + (((2*u1^4+(-2)*u1^3*u2)*u3^5)*u4^4+(((-3)*u1^8+3*u1^3*u2^5+(-15)*u1^4*u2^4+30*u1^5*u2^3+(-30)*u1^6*u2^2+15*u1^7*u2)*u3)*u5^4+((((-7)*u1^7+(-7)*u1^3*u2^4+28*u1^4*u2^3+(-42)*u1^5*u2^2+28*u1^6*u2)*u3^2)*u4)*u5^3+((((-3)*u1^6+3*u1^3*u2^3+(-9)*u1^4*u2^2+9*u1^5*u2)*u3^3)*u4^2)*u5^2+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^4)*u4^3)*u5) *g^2 + ((-1)*u1^4*u3^6*u4^4+((3*u1^8+3*u1^4*u2^4+(-12)*u1^5*u2^3+18*u1^6*u2^2+(-12)*u1^7*u2)*u3^2)*u5^4+(((8*u1^7+(-8)*u1^4*u2^3+24*u1^5*u2^2+(-24)*u1^6*u2)*u3^3)*u4)*u5^3+(((6*u1^6+6*u1^4*u2^2+(-12)*u1^5*u2)*u3^4)*u4^2)*u5^2) *g + ((((-1)*u1^8+u1^5*u2^3+(-3)*u1^6*u2^2+3*u1^7*u2)*u3^3)*u5^4+((((-3)*u1^7+(-3)*u1^5*u2^2+6*u1^6*u2)*u3^4)*u4)*u5^3+((((-3)*u1^6+3*u1^5*u2)*u3^5)*u4^2)*u5^2+(-1)*u1^5*u3^6*u4^3*u5) ; (((u1^4+(-1)*u1*u2^3+3*u1^2*u2^2+(-3)*u1^3*u2)*u3^3)*u5^4+(((3*u1^3+3*u1*u2^2+(-6)*u1^2*u2)*u3^4)*u4)*u5^3+(((3*u1^2+(-3)*u1*u2)*u3^5)*u4^2)*u5^2+u1*u3^6*u4^3*u5) *g^2*h^2 + (((u1^4+(-1)*u1*u2^3+3*u1^2*u2^2+(-3)*u1^3*u2)*u3^3)*u5^4+(((3*u1^3+3*u1*u2^2+(-6)*u1^2*u2)*u3^4)*u4)*u5^3+(((3*u1^2+(-3)*u1*u2)*u3^5)*u4^2)*u5^2+u1*u3^6*u4^3*u5) *f^2*i^2 + ((-1)*u1*u3^6*u4^4+(((-1)*u1^5+(-1)*u1*u2^4+4*u1^2*u2^3+(-6)*u1^3*u2^2+4*u1^4*u2)*u3^2)*u5^4+((((-4)*u1^4+4*u1*u2^3+(-12)*u1^2*u2^2+12*u1^3*u2)*u3^3)*u4)*u5^3+((((-6)*u1^3+(-6)*u1*u2^2+12*u1^2*u2)*u3^4)*u4^2)*u5^2+((((-4)*u1^2+4*u1*u2)*u3^5)*u4^3)*u5) *f*g*i^2 + (((u1^2+(-1)*u1*u2)*u3^5)*u4^4+((u1^4+(-1)*u1*u2^3+3*u1^2*u2^2+(-3)*u1^3*u2)*u3^3+(u1^6+(-1)*u1*u2^5+5*u1^2*u2^4+(-10)*u1^3*u2^3+10*u1^4*u2^2+(-5)*u1^5*u2)*u3)*u5^4+(((3*u1^3+3*u1*u2^2+(-6)*u1^2*u2)*u3^4+(4*u1^5+4*u1*u2^4+(-16)*u1^2*u2^3+24*u1^3*u2^2+(-16)*u1^4*u2)*u3^2)*u4)*u5^3+(((3*u1^2+(-3)*u1*u2)*u3^5+(6*u1^4+(-6)*u1*u2^3+18*u1^2*u2^2+(-18)*u1^3*u2)*u3^3)*u4^2)*u5^2+((u1*u3^6+(4*u1^3+4*u1*u2^2+(-8)*u1^2*u2)*u3^4)*u4^3)*u5) *g^2*i^2 + ((((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^3)*u5^4+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^4)*u4)*u5^3+((((-3)*u1^3+3*u1^2*u2)*u3^5)*u4^2)*u5^2+(-1)*u1^2*u3^6*u4^3*u5) *f^2*h + ((-1)*u1^2*u3^6*u4^4+((u1^6+u1^2*u2^4+(-4)*u1^3*u2^3+6*u1^4*u2^2+(-4)*u1^5*u2)*u3^2)*u5^4+(((2*u1^5+(-2)*u1^2*u2^3+6*u1^3*u2^2+(-6)*u1^4*u2)*u3^3)*u4)*u5^3+((((-2)*u1^3+2*u1^2*u2)*u3^5)*u4^3)*u5) *f*g*h + (((u1^3+(-1)*u1^2*u2)*u3^5)*u4^4+(((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^3+((-1)*u1^7+u1^2*u2^5+(-5)*u1^3*u2^4+10*u1^4*u2^3+(-10)*u1^5*u2^2+5*u1^6*u2)*u3)*u5^4+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^4+((-2)*u1^6+(-2)*u1^2*u2^4+8*u1^3*u2^3+(-12)*u1^4*u2^2+8*u1^5*u2)*u3^2)*u4)*u5^3+((((-3)*u1^3+3*u1^2*u2)*u3^5)*u4^2)*u5^2+(((-1)*u1^2*u3^6+(2*u1^4+2*u1^2*u2^2+(-4)*u1^3*u2)*u3^4)*u4^3)*u5) *g^2*h + (u1^2*u3^6*u4^4+(((u1^5+(-1)*u1^2*u2^3+3*u1^3*u2^2+(-3)*u1^4*u2)*u3^3)*u4)*u5^3+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^4)*u4^2)*u5^2+(((3*u1^3+(-3)*u1^2*u2)*u3^5)*u4^3)*u5) *f^2*i + ((((-1)*u1^3+u1^2*u2)*u3^5)*u4^4+(((-1)*u1^5+u1^2*u2^3+(-3)*u1^3*u2^2+3*u1^4*u2)*u3^3)*u5^4+((((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^4+((-1)*u1^6+(-1)*u1^2*u2^4+4*u1^3*u2^3+(-6)*u1^4*u2^2+4*u1^5*u2)*u3^2)*u4)*u5^3+((((-3)*u1^3+3*u1^2*u2)*u3^5+((-3)*u1^5+3*u1^2*u2^3+(-9)*u1^3*u2^2+9*u1^4*u2)*u3^3)*u4^2)*u5^2+(((-1)*u1^2*u3^6+((-3)*u1^4+(-3)*u1^2*u2^2+6*u1^3*u2)*u3^4)*u4^3)*u5) *f*g*i + ((u1^2*u3^6+(u1^4+u1^2*u2^2+(-2)*u1^3*u2)*u3^4)*u4^4+((u1^6+u1^2*u2^4+(-4)*u1^3*u2^3+6*u1^4*u2^2+(-4)*u1^5*u2)*u3^2)*u5^4+(((4*u1^5+(-4)*u1^2*u2^3+12*u1^3*u2^2+(-12)*u1^4*u2)*u3^3+(u1^7+(-1)*u1^2*u2^5+5*u1^3*u2^4+(-10)*u1^4*u2^3+10*u1^5*u2^2+(-5)*u1^6*u2)*u3)*u4)*u5^3+(((6*u1^4+6*u1^2*u2^2+(-12)*u1^3*u2)*u3^4+(3*u1^6+3*u1^2*u2^4+(-12)*u1^3*u2^3+18*u1^4*u2^2+(-12)*u1^5*u2)*u3^2)*u4^2)*u5^2+(((4*u1^3+(-4)*u1^2*u2)*u3^5+(3*u1^5+(-3)*u1^2*u2^3+9*u1^3*u2^2+(-9)*u1^4*u2)*u3^3)*u4^3)*u5) *g^2*i + (((u1^5+(-1)*u1^2*u2^3+3*u1^3*u2^2+(-3)*u1^4*u2)*u3^3)*u5^4+(((3*u1^4+3*u1^2*u2^2+(-6)*u1^3*u2)*u3^4)*u4)*u5^3+(((3*u1^3+(-3)*u1^2*u2)*u3^5)*u4^2)*u5^2+u1^2*u3^6*u4^3*u5) *f*i^2 + ((-1)*u1^2*u3^6*u4^4+(((-2)*u1^6+(-2)*u1^2*u2^4+8*u1^3*u2^3+(-12)*u1^4*u2^2+8*u1^5*u2)*u3^2)*u5^4+((((-7)*u1^5+7*u1^2*u2^3+(-21)*u1^3*u2^2+21*u1^4*u2)*u3^3)*u4)*u5^3+((((-9)*u1^4+(-9)*u1^2*u2^2+18*u1^3*u2)*u3^4)*u4^2)*u5^2+((((-5)*u1^3+5*u1^2*u2)*u3^5)*u4^3)*u5) *g*i^2 + ((((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^3)*u5^4+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^4)*u4)*u5^3+((((-3)*u1^4+3*u1^3*u2)*u3^5)*u4^2)*u5^2+(-1)*u1^3*u3^6*u4^3*u5) *f*h + ((-1)*u1^3*u3^6*u4^4+((2*u1^7+2*u1^3*u2^4+(-8)*u1^4*u2^3+12*u1^5*u2^2+(-8)*u1^6*u2)*u3^2)*u5^4+(((5*u1^6+(-5)*u1^3*u2^3+15*u1^4*u2^2+(-15)*u1^5*u2)*u3^3)*u4)*u5^3+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^4)*u4^2)*u5^2+((((-1)*u1^4+u1^3*u2)*u3^5)*u4^3)*u5) *g*h + (u1^3*u3^6*u4^4+(((u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^3)*u4)*u5^3+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^4)*u4^2)*u5^2+(((3*u1^4+(-3)*u1^3*u2)*u3^5)*u4^3)*u5) *f*i + ((((-2)*u1^4+2*u1^3*u2)*u3^5)*u4^4+(((-1)*u1^6+u1^3*u2^3+(-3)*u1^4*u2^2+3*u1^5*u2)*u3^3)*u5^4+((((-3)*u1^5+(-3)*u1^3*u2^2+6*u1^4*u2)*u3^4+((-2)*u1^7+(-2)*u1^3*u2^4+8*u1^4*u2^3+(-12)*u1^5*u2^2+8*u1^6*u2)*u3^2)*u4)*u5^3+((((-3)*u1^4+3*u1^3*u2)*u3^5+((-6)*u1^6+6*u1^3*u2^3+(-18)*u1^4*u2^2+18*u1^5*u2)*u3^3)*u4^2)*u5^2+(((-1)*u1^3*u3^6+((-6)*u1^5+(-6)*u1^3*u2^2+12*u1^4*u2)*u3^4)*u4^3)*u5) *g*i + (((u1^6+(-1)*u1^3*u2^3+3*u1^4*u2^2+(-3)*u1^5*u2)*u3^3)*u5^4+(((3*u1^5+3*u1^3*u2^2+(-6)*u1^4*u2)*u3^4)*u4)*u5^3+(((3*u1^4+(-3)*u1^3*u2)*u3^5)*u4^2)*u5^2+u1^3*u3^6*u4^3*u5) *i^2 + ((((-1)*u1^7+u1^4*u2^3+(-3)*u1^5*u2^2+3*u1^6*u2)*u3^3)*u5^4+((((-3)*u1^6+(-3)*u1^4*u2^2+6*u1^5*u2)*u3^4)*u4)*u5^3+((((-3)*u1^5+3*u1^4*u2)*u3^5)*u4^2)*u5^2+(-1)*u1^4*u3^6*u4^3*u5) *h + (u1^4*u3^6*u4^4+(((u1^7+(-1)*u1^4*u2^3+3*u1^5*u2^2+(-3)*u1^6*u2)*u3^3)*u4)*u5^3+(((3*u1^6+3*u1^4*u2^2+(-6)*u1^5*u2)*u3^4)*u4^2)*u5^2+(((3*u1^5+(-3)*u1^4*u2)*u3^5)*u4^3)*u5) *i ; ((((-1)*u1^3+u2^3+(-3)*u1*u2^2+3*u1^2*u2)*u3^4)*u5^4+((((-3)*u1^2+(-3)*u2^2+6*u1*u2)*u3^5)*u4)*u5^3+((((-3)*u1+3*u2)*u3^6)*u4^2)*u5^2+(-1)*u3^7*u4^3*u5) ; (u3^7*u4^4+(((u1^3+(-1)*u2^3+3*u1*u2^2+(-3)*u1^2*u2)*u3^4)*u4)*u5^3+(((3*u1^2+3*u2^2+(-6)*u1*u2)*u3^5)*u4^2)*u5^2+(((3*u1+(-3)*u2)*u3^6)*u4^3)*u5) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; ((-1)*u3) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)*u5) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
];
c:=
1;
p:= (((-4)*u1^7*u3^10+...*u3^3+...)*u5^8+...) *r*t + ((2*u1^7*u3^10+...*u3^3+...)*u5^8+...) *t^2 + (((-4)*u1^7*u3^10+...*u3^3+...)*u5^8+...) *s*u + ((2*u1^7*u3^10+...*u3^3+...)*u5^8+...) *u^2 + (((4*u1^7*u3^10+...*u3^4+...)*u4)*u5^8+...) *r + ((4*u1^7*u3^10+...*u3^3+...)*u5^9+...) *s + (((-2)*u1^7*u3^10+...*u3^3+...)*u5^10+...)
F:=[
(u3) *n^2*p^3 + 50 termes
((-1)*u1+u2) *n^2*p^3 + 50 termes
(u3) *n^3*p^2 + 45 termes
((-1)*u2) *n^3*p^2 + 40 termes
((-1)*u1) *j^2*l^2*m + 22 termes
(u1) *j^2*l^3 + 22 termes
((-1)*u3) *j^3*l^2 + 46 termes
((-1)*u1+u2) *j^3*l^2 + 44 termes
((-1)*u3) *f^2*h^3 + 12 termes
((-1)*u2) *f^2*h^3 + 12 termes
(u1) *f^2*g*h^2 + (u1) *g^3*h^2 + (u1) *f^2*g*i^2 + (u1) *g^3*i^2 + (u1^2) *f^2*g*h + (u1^2) *g^3*h + ((-1)*u1^2) *f^3*i + ((-1)*u1^2) *f*g^2*i
(u1) *f^3*h^2 + (u1) *f*g^2*h^2 + (u1) *f^3*i^2 + (u1) *f*g^2*i^2 + ((-1)*u1^2) *f^3*h + ((-1)*u1^2) *f*g^2*h + ((-1)*u1^2) *f^2*g*i + ((-1)*u1^2) *g^3*i
(u3) *f + (u1+(-1)*u2) *g + ((-1)*u1*u3)
(u3) *h + (u1+(-1)*u2) *i + ((-1)*u1*u3)
(u3) *j + ((-1)*u2) *k
(u3) *l + ((-1)*u2) *m
((-1)*u1) *o
((-1)*u1) *q
(1) *k*r + ((-1)) *j*s + ((-1)*u1) *k + (u1) *s
(1) *q*r + ((-1)) *p*s + (u3) *p + ((-1)*u2) *q + ((-1)*u3) *r + (u2) *s
(1) *i*t + ((-1)) *h*u
(1) *o*t + ((-1)) *n*u + (u3) *n + ((-1)*u2) *o + ((-1)*u3) *t + (u2) *u
((-1)*u5) *f + (u4) *g
((-1)*u5) *l + ((-1)*u1+u4) *m + (u1*u5)
];