Feuerbach
Geogebra sheet
Coq statement
Lemma Feuerbach: forall A B C A1 B1 C1 O A2 B2 C2 O2:point,
forall r r2:R,
X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0->
middle A B C1 -> middle B C A1 -> middle C A B1 ->
distance2 O A1 = distance2 O B1 ->
distance2 O A1 = distance2 O C1 ->
collinear A B C2 -> orthogonal A B O2 C2 ->
collinear B C A2 -> orthogonal B C O2 A2 ->
collinear A C B2 -> orthogonal A C O2 B2 ->
distance2 O2 A2 = distance2 O2 B2 ->
distance2 O2 A2 = distance2 O2 C2 ->
r^2 = distance2 O A1 ->
r2^2 = distance2 O2 A2 ->
distance2 O O2 = (r + r2)^2
\/ distance2 O O2 = (r - r2)^2
\/ collinear A B C.
Proof. geo_begin. tzR. Qed.
Algebraic version
p:= ((-1)) *a*c^4 + (2) *a*c^2*d^2 + ((-1)) *a*d^4 + (2) *a*c^2*i^2 + (2) *a*d^2*i^2 + ((-1)) *a*i^4 + (2) *a*c^2*k^2 + (2) *a*d^2*k^2 + ((-2)) *a*i^2*k^2 + ((-1)) *a*k^4 + ((-4)) *a*c^2*i*q + ((-4)) *a*d^2*i*q + (4) *a*i^3*q + (4) *a*i*k^2*q + (2) *a*c^2*q^2 + (2) *a*d^2*q^2 + ((-6)) *a*i^2*q^2 + ((-2)) *a*k^2*q^2 + (4) *a*i*q^3 + ((-1)) *a*q^4 + ((-4)) *a*c^2*k*s + ((-4)) *a*d^2*k*s + (4) *a*i^2*k*s + (4) *a*k^3*s + ((-8)) *a*i*k*q*s + (4) *a*k*q^2*s + (2) *a*c^2*s^2 + (2) *a*d^2*s^2 + ((-2)) *a*i^2*s^2 + ((-6)) *a*k^2*s^2 + (4) *a*i*q*s^2 + ((-2)) *a*q^2*s^2 + (4) *a*k*s^3 + ((-1)) *a*s^4
F:= [
((-1)) *o^2 + ((-1)) *p^2 + (2) *o*q + ((-2)) *q*r + (1) *r^2 + (2) *p*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *m^2 + ((-1)) *n^2 + (2) *m*q + ((-2)) *q*r + (1) *r^2 + (2) *n*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *g^2 + ((-1)) *h^2 + (2) *g*i + ((-2)) *i*j + (1) *j^2 + (2) *h*k + ((-2)) *k*l + (1) *l^2 ;
((-1)) *e^2 + ((-1)) *f^2 + (2) *e*i + ((-2)) *i*j + (1) *j^2 + (2) *f*k + ((-2)) *k*l + (1) *l^2 ;
(1) *d^2 + ((-1)) *q^2 + (2) *q*r + ((-1)) *r^2 + ((-1)) *s^2 + (2) *s*t + ((-1)) *t^2 ;
(1) *c^2 + ((-1)) *i^2 + (2) *i*j + ((-1)) *j^2 + ((-1)) *k^2 + (2) *k*l + ((-1)) *l^2 ;
((-1)) *b + (2) *p ;
((-1)) *a + (2) *o ;
((-1)) *b + (2) *t + ((-1)) ;
((-1)) *a + (2) *r ;
(2) *n + ((-1)) ;
(2) *m ;
((-1)) *e ;
(1) *f + ((-1)) *k ;
((-1)) *b*j + (1) *a*l + ((-1)) *a + (1) *j ;
((-1)) *a*i + (1) *a*j + ((-1)) *b*k + (1) *b*l + (1) *k + ((-1)) *l ;
((-1)) *b*g + (1) *a*h ;
(1) *a*g + (1) *b*h + ((-1)) *a*i + ((-1)) *b*k ;
];
Certificate
CR:=[
(2) ; (4) ; (4) *k + ((-8)) ; ((-4)) *r ; ((-2)) *k + ((-2)) *l + (8) ; 0; 0; (4) *l + ((-12)) *t + ((-8)) ; ((-2)) *l + (8) *t + (6) ; 0; 0; (2) *l^2 + ((-2)) *k + ((-6)) *l ; ((-4)) *r ; 0; (4) *k^2 + (2) *k*l + (8) *l^2 + ((-4)) *k*t + ((-20)) *l*t + ((-20)) *k + (4) *l + (4) *t + ((-16)) ; ((-8)) *k + (8) *l + ((-4)) ; 0; (6) *k^2 + (2) *l^2 + ((-16)) *k + ((-12)) ; 0; ((-4)) *j ; (2) *j*k + (8) *j*t + ((-24)) *j ; ((-6)) *k^2 + (4) *k*l + ((-8)) *k*t + (8) *l*t + (24) *t^2 + (4) *k + ((-32)) *l + ((-84)) *t + (69) ; 0; 0; 0; ((-2)) *j*k + ((-8)) *j*t + (12) *j ; 0; (4) *k*t + ((-24)) *t^2 + (14) *k + (44) *t + ((-23)) ; (4) *k^2*r + ((-4)) *j*k*t + ((-8)) *k*r*t + (24) *j*t^2 + (2) *j*k + ((-16)) *k*r + ((-8)) *j*t + (16) *r*t + ((-10)) *j + (8) *r ; ((-4)) *k^2*r + (8) *g*k*t + ((-24)) *k*r*t + (16) *i*t^2 + ((-8)) *g*k + (36) *k*r + ((-32)) *g*t + ((-24)) *i*t + (24) *r*t + (16) *g + (9) *i + ((-30)) *r ; ((-8)) *i*k*r + (4) *j*k*r + ((-4)) *k^2*t + (16) *j*r*t + ((-48)) *k*t^2 + (4) *j^2 + (34) *k^2 + (24) *i*r + ((-36)) *j*r + (8) *r^2 + (124) *k*t + ((-76)) *k ; ((-2)) *g*j*k + ((-6)) *h*k^2 + (6) *k^3 + (2) *h*k*l + ((-2)) *k^2*l + ((-8)) *i*k*r + (4) *j*k*r + ((-8)) *g*j*t + ((-8)) *h*k*t + (12) *k^2*t + ((-4)) *l^2*t + ((-8)) *g*r*t + (8) *j*r*t + (24) *h*t^2 + (8) *l*t^2 + ((-4)) *g*i + (4) *i^2 + (10) *g*j + (5) *j^2 + (16) *h*k + ((-33)) *k^2 + ((-12)) *h*l + (10) *k*l + (7) *l^2 + (12) *g*r + (20) *i*r + ((-32)) *j*r + ((-36)) *h*t + ((-36)) *k*t + ((-12)) *l*t + ((-4)) *t^2 + (24) *h + (26) *k + (4) *l + (4) *t + ((-1)) ; ((-16)) *i*j*r + (8) *j^2*r + ((-8)) *k^2*r + ((-24)) *k*l*r + (8) *l^2*r + (16) *i*r^2 + ((-8)) *r^3 + (2) *j*k*t + (44) *k*r*t + ((-16)) *i*t^2 + (8) *j*t^2 + (16) *q*t^2 + ((-4)) *j*k + ((-8)) *g*l + (4) *i*l + (4) *j*l + ((-32)) *k*q + (48) *l*q + (8) *h*r + (14) *k*r + ((-10)) *l*r + (12) *g*t + (20) *i*t + ((-38)) *j*t + ((-24)) *q*t + ((-24)) *r*t + (12) *g + ((-8)) *i + (22) *j + (1) *r ; (16) *i^2*j + ((-8)) *i*j^2 + (16) *i*k*l + ((-8)) *i*l^2 + ((-16)) *i*j*q + (8) *j^2*q + (8) *k^2*q + ((-16)) *k*l*q + (8) *l^2*q + ((-16)) *i^2*r + (8) *i*j*r + ((-4)) *j^2*r + ((-12)) *k^2*r + (8) *k*l*r + ((-4)) *l^2*r + (16) *i*q*r + ((-8)) *q*r^2 + (4) *r^3 + ((-16)) *i*k*t + (16) *k*r*t + ((-4)) *r*t^2 + (20) *i*k + ((-8)) *j*k + ((-24)) *i*l + (12) *j*l + ((-4)) *k*r + (8) *i*t + ((-2)) *r*t + ((-2)) *j + (2) *r ; (16) *i*j*k*r + ((-8)) *j^2*k*r + (16) *k^2*l*r + ((-8)) *k*l^2*r + ((-16)) *i*k*q*r + (16) *k*q*r^2 + ((-8)) *k*r^3 + (8) *i^2*r*s + ((-16)) *i*j*r*s + (8) *j^2*r*s + ((-16)) *k*l*r*s + (8) *l^2*r*s + ((-16)) *i^2*j*t + (8) *i*j^2*t + ((-8)) *i*k*l*t + ((-4)) *j*k*l*t + (16) *i*l^2*t + ((-4)) *j*l^2*t + (16) *i*j*q*t + ((-8)) *j^2*q*t + ((-8)) *k^2*q*t + (16) *k*l*q*t + ((-8)) *l^2*q*t + (8) *i^2*r*t + ((-8)) *i*j*r*t + (4) *j^2*r*t + ((-4)) *k^2*r*t + ((-8)) *k*l*r*t + (4) *l^2*r*t + ((-8)) *q*r^2*t + (4) *r^3*t + (16) *k*r*s*t + (16) *i*k*t^2 + ((-16)) *i*l*t^2 + (8) *j*l*t^2 + ((-8)) *k*r*t^2 + ((-8)) *r*s*t^2 + (4) *r*t^3 + (8) *i^2*j + ((-4)) *i*j^2 + ((-4)) *i*k^2 + (4) *j*k^2 + (6) *i*k*l + ((-4)) *j*k*l + ((-2)) *i*l^2 + (2) *j*l^2 + ((-8)) *i*j*q + (4) *j^2*q + (4) *k^2*q + ((-8)) *k*l*q + (4) *l^2*q + ((-8)) *g*i*r + ((-10)) *i^2*r + (4) *g*j*r + (16) *i*j*r + ((-8)) *j^2*r + ((-4)) *h*k*r + ((-14)) *k^2*r + (8) *h*l*r + (12) *k*l*r + ((-4)) *l^2*r + (8) *i*q*r + ((-4)) *q*r^2 + (2) *r^3 + ((-28)) *i*k*t + (8) *j*k*t + (24) *i*l*t + ((-12)) *j*l*t + (8) *k*r*t + ((-4)) *j*t^2 + (2) *r*t^2 + (9) *i*k + ((-3)) *j*k + ((-9)) *i*l + (4) *j*l + ((-2)) *k*r + (4) *j*t + ((-3)) *r*t + ((-1)) *j + (1) *r ; ((-16)) *i^2*j^2 + (16) *i*j^3 + ((-4)) *j^4 + ((-32)) *i*j*k*l + (16) *j^2*k*l + (16) *i*j*l^2 + ((-8)) *j^2*l^2 + ((-16)) *k^2*l^2 + (16) *k*l^3 + ((-4)) *l^4 + (32) *i^2*j*q + ((-16)) *i*j^2*q + (32) *i*k*l*q + ((-16)) *i*l^2*q + ((-32)) *i*j*q^2 + (16) *j^2*q^2 + (16) *k^2*q^2 + ((-32)) *k*l*q^2 + (16) *l^2*q^2 + (8) *h*i*k*r + ((-4)) *h*j*k*r + ((-4)) *g*k^2*r + ((-8)) *i*k^2*r + (4) *j*k^2*r + (8) *i*k*l*r + ((-4)) *j*k*l*r + ((-32)) *i^2*q*r + (32) *i*j*q*r + ((-16)) *j^2*q*r + ((-32)) *k^2*q*r + (32) *k*l*q*r + ((-16)) *l^2*q*r + (32) *i*q^2*r + (16) *i^2*r^2 + ((-16)) *i*j*r^2 + (8) *j^2*r^2 + (16) *k^2*r^2 + ((-16)) *k*l*r^2 + (8) *l^2*r^2 + ((-16)) *i*q*r^2 + ((-16)) *q^2*r^2 + (16) *q*r^3 + ((-4)) *r^4 + (32) *i*j*k*s + ((-16)) *j^2*k*s + (32) *k^2*l*s + ((-16)) *k*l^2*s + ((-32)) *i*k*q*s + (32) *k*q*r*s + ((-16)) *k*r^2*s + (16) *i^2*s^2 + ((-32)) *i*j*s^2 + (16) *j^2*s^2 + ((-32)) *k*l*s^2 + (16) *l^2*s^2 + (8) *h*k^2*t + ((-16)) *k^3*t + ((-4)) *h*k*l*t + (4) *k^2*l*t + ((-8)) *k*l^2*t + (8) *l^3*t + (8) *g*k*r*t + ((-16)) *i*k*r*t + (8) *j*k*r*t + ((-32)) *i^2*s*t + (32) *i*j*s*t + ((-16)) *j^2*s*t + ((-32)) *k^2*s*t + (32) *k*l*s*t + ((-16)) *l^2*s*t + (32) *i*q*s*t + ((-32)) *q*r*s*t + (16) *r^2*s*t + (32) *k*s^2*t + (16) *i^2*t^2 + ((-16)) *i*j*t^2 + (8) *j^2*t^2 + (16) *k^2*t^2 + ((-24)) *h*l*t^2 + (56) *k*l*t^2 + ((-32)) *l^2*t^2 + ((-16)) *i*q*t^2 + (16) *q*r*t^2 + ((-8)) *r^2*t^2 + ((-16)) *k*s*t^2 + ((-16)) *s^2*t^2 + (16) *s*t^3 + ((-4)) *t^4 + ((-4)) *g*i*k + (2) *g*j*k + (8) *i*j*k + ((-4)) *j^2*k + ((-6)) *h*k^2 + (6) *k^3 + (4) *g*i*l + ((-4)) *i^2*l + ((-2)) *g*j*l + (2) *i*j*l + (2) *h*k*l + (4) *k^2*l + (2) *h*l^2 + (2) *k*l^2 + ((-6)) *l^3 + (32) *i*k*q + ((-16)) *j*k*q + ((-48)) *i*l*q + (24) *j*l*q + ((-24)) *h*i*r + (20) *h*j*r + (12) *g*k*r + ((-20)) *j*k*r + (4) *i*l*r + (12) *j*l*r + ((-8)) *h*r^2 + ((-8)) *g*i*t + (4) *g*j*t + (24) *i*j*t + ((-12)) *j^2*t + ((-16)) *h*k*t + (36) *k^2*t + (36) *h*l*t + ((-112)) *k*l*t + (60) *l^2*t + ((-8)) *g*r*t + (32) *i*r*t + ((-24)) *j*r*t + ((-16)) *h*t^2 + (20) *k*t^2 + ((-16)) *l*t^2 + (4) *g*i + ((-2)) *g*j + ((-34)) *i*j + (17) *j^2 + (20) *h*k + ((-23)) *k^2 + ((-24)) *h*l + (38) *k*l + ((-15)) *l^2 + (8) *i*q + ((-4)) *j*q + ((-12)) *g*r + ((-22)) *i*r + (32) *j*r + ((-38)) *k*t + (46) *l*t + (4) *t^2 + (4) *h + (24) *k + ((-29)) *l + ((-4)) *t + (1) ; ((-16)) *g*i*r*t + (8) *g*j*r*t + (16) *i*j*r*t + ((-8)) *j^2*r*t + ((-8)) *h*k*r*t + ((-16)) *k^2*r*t + (16) *h*l*r*t + (8) *k*l*r*t + (8) *g*i*r + ((-4)) *g*j*r + ((-8)) *i*j*r + (4) *j^2*r + (4) *h*k*r + (8) *k^2*r + ((-8)) *h*l*r + ((-4)) *k*l*r ; 0; 0; 0; 0; (16) *i*j*k*r + ((-8)) *j^2*k*r + (8) *k^3*r + (24) *k^2*l*r + ((-8)) *k*l^2*r + ((-16)) *i*k*r^2 + (8) *k*r^3 + ((-4)) *j*k^2*t + ((-48)) *k^2*r*t + (16) *i*k*t^2 + ((-16)) *j*k*t^2 + ((-16)) *k*q*t^2 + (24) *k*r*t^2 + (4) *j*k^2 + (8) *g*k*l + ((-4)) *i*k*l + ((-4)) *j*k*l + (32) *k^2*q + ((-48)) *k*l*q + ((-8)) *h*k*r + ((-28)) *k^2*r + (10) *k*l*r + ((-12)) *g*k*t + ((-20)) *i*k*t + (62) *j*k*t + (24) *k*q*t + ((-20)) *k*r*t + ((-12)) *g*k + (8) *i*k + ((-22)) *j*k + (22) *k*r ; 0; 0; ((-32)) *i^2*j*s + (16) *i*j^2*s + ((-32)) *i*k*l*s + (16) *i*l^2*s + (32) *i*j*q*s + ((-16)) *j^2*q*s + ((-16)) *k^2*q*s + (32) *k*l*q*s + ((-16)) *l^2*q*s + (32) *i^2*r*s + ((-16)) *i*j*r*s + (8) *j^2*r*s + (24) *k^2*r*s + ((-16)) *k*l*r*s + (8) *l^2*r*s + ((-32)) *i*q*r*s + (16) *q*r^2*s + ((-8)) *r^3*s + (32) *i*k*s*t + ((-32)) *k*r*s*t + (8) *r*s*t^2 + (8) *i^2*j + ((-4)) *i*j^2 + ((-4)) *i*k^2 + (4) *j*k^2 + (6) *i*k*l + ((-4)) *j*k*l + ((-2)) *i*l^2 + (2) *j*l^2 + ((-8)) *i*j*q + (4) *j^2*q + (4) *k^2*q + ((-8)) *k*l*q + (4) *l^2*q + ((-8)) *i^2*r + (4) *i*j*r + ((-2)) *j^2*r + ((-6)) *k^2*r + (4) *k*l*r + ((-2)) *l^2*r + (8) *i*q*r + ((-4)) *q*r^2 + (2) *r^3 + ((-40)) *i*k*s + (16) *j*k*s + (48) *i*l*s + ((-24)) *j*l*s + (8) *k*r*s + ((-8)) *i*k*t + (8) *i*l*t + ((-4)) *j*l*t + (8) *k*r*t + ((-16)) *i*s*t + (4) *r*s*t + ((-2)) *r*t^2 + (9) *i*k + ((-3)) *j*k + ((-9)) *i*l + (4) *j*l + ((-2)) *k*r + (4) *j*s + ((-4)) *r*s + (2) *j*t + ((-1)) *r*t + ((-1)) *j + (1) *r ; 0; 0; ((-16)) *i^2*j^2 + (16) *i*j^3 + ((-4)) *j^4 + ((-32)) *i*j*k*l + (16) *j^2*k*l + (16) *i*j*l^2 + ((-8)) *j^2*l^2 + ((-16)) *k^2*l^2 + (16) *k*l^3 + ((-4)) *l^4 + (32) *i^2*j*q + ((-16)) *i*j^2*q + (32) *i*k*l*q + ((-16)) *i*l^2*q + ((-32)) *i*j*q^2 + (16) *j^2*q^2 + (16) *k^2*q^2 + ((-32)) *k*l*q^2 + (16) *l^2*q^2 + (8) *i*k*l*r + ((-4)) *j*k*l*r + ((-32)) *i^2*q*r + (32) *i*j*q*r + ((-16)) *j^2*q*r + ((-32)) *k^2*q*r + (32) *k*l*q*r + ((-16)) *l^2*q*r + (32) *i*q^2*r + (16) *i^2*r^2 + ((-16)) *i*j*r^2 + (8) *j^2*r^2 + (16) *k^2*r^2 + ((-16)) *k*l*r^2 + (8) *l^2*r^2 + ((-16)) *i*q*r^2 + ((-16)) *q^2*r^2 + (16) *q*r^3 + ((-4)) *r^4 + (32) *i*j*k*s + ((-16)) *j^2*k*s + (32) *k^2*l*s + ((-16)) *k*l^2*s + ((-32)) *i*k*q*s + (32) *k*q*r*s + ((-16)) *k*r^2*s + (16) *i^2*s^2 + ((-32)) *i*j*s^2 + (16) *j^2*s^2 + ((-32)) *k*l*s^2 + (16) *l^2*s^2 + ((-8)) *k*l^2*t + (8) *l^3*t + ((-32)) *i^2*s*t + (32) *i*j*s*t + ((-16)) *j^2*s*t + ((-32)) *k^2*s*t + (32) *k*l*s*t + ((-16)) *l^2*s*t + (32) *i*q*s*t + ((-32)) *q*r*s*t + (16) *r^2*s*t + (32) *k*s^2*t + (16) *i^2*t^2 + ((-16)) *i*j*t^2 + (8) *j^2*t^2 + (16) *k^2*t^2 + (16) *k*l*t^2 + ((-40)) *l^2*t^2 + ((-16)) *i*q*t^2 + (16) *q*r*t^2 + ((-8)) *r^2*t^2 + ((-16)) *k*s*t^2 + ((-16)) *s^2*t^2 + (16) *s*t^3 + ((-4)) *t^4 + (4) *i*j*k + ((-2)) *j^2*k + (6) *h*k^2 + (2) *k^3 + (8) *g*i*l + ((-4)) *i^2*l + ((-4)) *g*j*l + ((-2)) *i*j*l + (2) *j^2*l + (2) *h*k*l + (16) *k^2*l + (4) *h*l^2 + ((-6)) *l^3 + (32) *i*k*q + ((-16)) *j*k*q + ((-48)) *i*l*q + (24) *j*l*q + ((-8)) *h*i*r + (12) *h*j*r + (4) *g*k*r + ((-16)) *i*k*r + ((-12)) *j*k*r + ((-8)) *g*l*r + (20) *i*l*r + (4) *j*l*r + ((-16)) *h*r^2 + (16) *k*r^2 + ((-8)) *g*i*t + (4) *g*j*t + (24) *i*j*t + ((-12)) *j^2*t + (8) *h*k*t + ((-12)) *k^2*t + ((-16)) *h*l*t + (36) *k*l*t + (8) *l^2*t + ((-8)) *g*r*t + (32) *i*r*t + ((-24)) *j*r*t + ((-24)) *h*t^2 + (48) *k*t^2 + ((-24)) *l*t^2 + ((-12)) *g*i + (10) *g*j + ((-26)) *i*j + (13) *j^2 + ((-16)) *h*k + ((-15)) *k^2 + ((-4)) *h*l + ((-14)) *k*l + (5) *l^2 + (8) *i*q + ((-4)) *j*q + ((-12)) *g*r + ((-22)) *i*r + (32) *j*r + (36) *h*t + ((-110)) *k*t + (82) *l*t + (4) *t^2 + ((-24)) *h + (56) *k + ((-45)) *l + ((-4)) *t + (1) ; 0; (4) *a*c^2 + ((-4)) *a*i^2 + ((-8)) *a*i*j + (4) *a*j^2 + ((-4)) *a*k^2 + ((-8)) *a*k*l + (4) *a*l^2 + (16) *a*i*q + ((-16)) *a*q^2 + (16) *a*q*r + ((-8)) *a*r^2 + (16) *a*k*s + ((-16)) *a*s^2 + (16) *a*s*t + ((-8)) *a*t^2 ; ((-8)) *a*c^2 + (4) *a*d^2 + ((-8)) *a*i^2 + ((-8)) *a*k^2 + (16) *a*i*q + ((-4)) *a*q^2 + ((-8)) *a*q*r + (4) *a*r^2 + (16) *a*k*s + ((-4)) *a*s^2 + ((-8)) *a*s*t + (4) *a*t^2 ; 0; ((-8)) *k*l*r + (16) *l*r ; 0; 0; ];
C:=[
[
(2) ; (4) ; (4) *k + ((-8)) ; ((-4)) *r ; ((-2)) *k + ((-2)) *l + (8) ; 0; 0; (4) *l + ((-12)) *t + ((-8)) ; ((-2)) *l + (8) *t + (6) ; 0; 0; (2) *l^2 + ((-2)) *k + ((-6)) *l ; ((-4)) *r ; 0; (4) *k^2 + (2) *k*l + (8) *l^2 + ((-4)) *k*t + ((-20)) *l*t + ((-20)) *k + (4) *l + (4) *t + ((-16)) ; ((-8)) *k + (8) *l + ((-4)) ; 0; (6) *k^2 + (2) *l^2 + ((-16)) *k + ((-12)) ; 0; ((-4)) *j ; (2) *j*k + (8) *j*t + ((-24)) *j ; ((-6)) *k^2 + (4) *k*l + ((-8)) *k*t + (8) *l*t + (24) *t^2 + (4) *k + ((-32)) *l + ((-84)) *t + (69) ; 0; 0; 0; ((-2)) *j*k + ((-8)) *j*t + (12) *j ; 0; (4) *k*t + ((-24)) *t^2 + (14) *k + (44) *t + ((-23)) ; (4) *k^2*r + ((-4)) *j*k*t + ((-8)) *k*r*t + (24) *j*t^2 + (2) *j*k + ((-16)) *k*r + ((-8)) *j*t + (16) *r*t + ((-10)) *j + (8) *r ; ((-4)) *k^2*r + (8) *g*k*t + ((-24)) *k*r*t + (16) *i*t^2 + ((-8)) *g*k + (36) *k*r + ((-32)) *g*t + ((-24)) *i*t + (24) *r*t + (16) *g + (9) *i + ((-30)) *r ; ((-8)) *i*k*r + (4) *j*k*r + ((-4)) *k^2*t + (16) *j*r*t + ((-48)) *k*t^2 + (4) *j^2 + (34) *k^2 + (24) *i*r + ((-36)) *j*r + (8) *r^2 + (124) *k*t + ((-76)) *k ; ((-2)) *g*j*k + ((-6)) *h*k^2 + (6) *k^3 + (2) *h*k*l + ((-2)) *k^2*l + ((-8)) *i*k*r + (4) *j*k*r + ((-8)) *g*j*t + ((-8)) *h*k*t + (12) *k^2*t + ((-4)) *l^2*t + ((-8)) *g*r*t + (8) *j*r*t + (24) *h*t^2 + (8) *l*t^2 + ((-4)) *g*i + (4) *i^2 + (10) *g*j + (5) *j^2 + (16) *h*k + ((-33)) *k^2 + ((-12)) *h*l + (10) *k*l + (7) *l^2 + (12) *g*r + (20) *i*r + ((-32)) *j*r + ((-36)) *h*t + ((-36)) *k*t + ((-12)) *l*t + ((-4)) *t^2 + (24) *h + (26) *k + (4) *l + (4) *t + ((-1)) ; ((-16)) *i*j*r + (8) *j^2*r + ((-8)) *k^2*r + ((-24)) *k*l*r + (8) *l^2*r + (16) *i*r^2 + ((-8)) *r^3 + (2) *j*k*t + (44) *k*r*t + ((-16)) *i*t^2 + (8) *j*t^2 + (16) *q*t^2 + ((-4)) *j*k + ((-8)) *g*l + (4) *i*l + (4) *j*l + ((-32)) *k*q + (48) *l*q + (8) *h*r + (14) *k*r + ((-10)) *l*r + (12) *g*t + (20) *i*t + ((-38)) *j*t + ((-24)) *q*t + ((-24)) *r*t + (12) *g + ((-8)) *i + (22) *j + (1) *r ; (16) *i^2*j + ((-8)) *i*j^2 + (16) *i*k*l + ((-8)) *i*l^2 + ((-16)) *i*j*q + (8) *j^2*q + (8) *k^2*q + ((-16)) *k*l*q + (8) *l^2*q + ((-16)) *i^2*r + (8) *i*j*r + ((-4)) *j^2*r + ((-12)) *k^2*r + (8) *k*l*r + ((-4)) *l^2*r + (16) *i*q*r + ((-8)) *q*r^2 + (4) *r^3 + ((-16)) *i*k*t + (16) *k*r*t + ((-4)) *r*t^2 + (20) *i*k + ((-8)) *j*k + ((-24)) *i*l + (12) *j*l + ((-4)) *k*r + (8) *i*t + ((-2)) *r*t + ((-2)) *j + (2) *r ; (16) *i*j*k*r + ((-8)) *j^2*k*r + (16) *k^2*l*r + ((-8)) *k*l^2*r + ((-16)) *i*k*q*r + (16) *k*q*r^2 + ((-8)) *k*r^3 + (8) *i^2*r*s + ((-16)) *i*j*r*s + (8) *j^2*r*s + ((-16)) *k*l*r*s + (8) *l^2*r*s + ((-16)) *i^2*j*t + (8) *i*j^2*t + ((-8)) *i*k*l*t + ((-4)) *j*k*l*t + (16) *i*l^2*t + ((-4)) *j*l^2*t + (16) *i*j*q*t + ((-8)) *j^2*q*t + ((-8)) *k^2*q*t + (16) *k*l*q*t + ((-8)) *l^2*q*t + (8) *i^2*r*t + ((-8)) *i*j*r*t + (4) *j^2*r*t + ((-4)) *k^2*r*t + ((-8)) *k*l*r*t + (4) *l^2*r*t + ((-8)) *q*r^2*t + (4) *r^3*t + (16) *k*r*s*t + (16) *i*k*t^2 + ((-16)) *i*l*t^2 + (8) *j*l*t^2 + ((-8)) *k*r*t^2 + ((-8)) *r*s*t^2 + (4) *r*t^3 + (8) *i^2*j + ((-4)) *i*j^2 + ((-4)) *i*k^2 + (4) *j*k^2 + (6) *i*k*l + ((-4)) *j*k*l + ((-2)) *i*l^2 + (2) *j*l^2 + ((-8)) *i*j*q + (4) *j^2*q + (4) *k^2*q + ((-8)) *k*l*q + (4) *l^2*q + ((-8)) *g*i*r + ((-10)) *i^2*r + (4) *g*j*r + (16) *i*j*r + ((-8)) *j^2*r + ((-4)) *h*k*r + ((-14)) *k^2*r + (8) *h*l*r + (12) *k*l*r + ((-4)) *l^2*r + (8) *i*q*r + ((-4)) *q*r^2 + (2) *r^3 + ((-28)) *i*k*t + (8) *j*k*t + (24) *i*l*t + ((-12)) *j*l*t + (8) *k*r*t + ((-4)) *j*t^2 + (2) *r*t^2 + (9) *i*k + ((-3)) *j*k + ((-9)) *i*l + (4) *j*l + ((-2)) *k*r + (4) *j*t + ((-3)) *r*t + ((-1)) *j + (1) *r ; ((-16)) *i^2*j^2 + (16) *i*j^3 + ((-4)) *j^4 + ((-32)) *i*j*k*l + (16) *j^2*k*l + (16) *i*j*l^2 + ((-8)) *j^2*l^2 + ((-16)) *k^2*l^2 + (16) *k*l^3 + ((-4)) *l^4 + (32) *i^2*j*q + ((-16)) *i*j^2*q + (32) *i*k*l*q + ((-16)) *i*l^2*q + ((-32)) *i*j*q^2 + (16) *j^2*q^2 + (16) *k^2*q^2 + ((-32)) *k*l*q^2 + (16) *l^2*q^2 + (8) *h*i*k*r + ((-4)) *h*j*k*r + ((-4)) *g*k^2*r + ((-8)) *i*k^2*r + (4) *j*k^2*r + (8) *i*k*l*r + ((-4)) *j*k*l*r + ((-32)) *i^2*q*r + (32) *i*j*q*r + ((-16)) *j^2*q*r + ((-32)) *k^2*q*r + (32) *k*l*q*r + ((-16)) *l^2*q*r + (32) *i*q^2*r + (16) *i^2*r^2 + ((-16)) *i*j*r^2 + (8) *j^2*r^2 + (16) *k^2*r^2 + ((-16)) *k*l*r^2 + (8) *l^2*r^2 + ((-16)) *i*q*r^2 + ((-16)) *q^2*r^2 + (16) *q*r^3 + ((-4)) *r^4 + (32) *i*j*k*s + ((-16)) *j^2*k*s + (32) *k^2*l*s + ((-16)) *k*l^2*s + ((-32)) *i*k*q*s + (32) *k*q*r*s + ((-16)) *k*r^2*s + (16) *i^2*s^2 + ((-32)) *i*j*s^2 + (16) *j^2*s^2 + ((-32)) *k*l*s^2 + (16) *l^2*s^2 + (8) *h*k^2*t + ((-16)) *k^3*t + ((-4)) *h*k*l*t + (4) *k^2*l*t + ((-8)) *k*l^2*t + (8) *l^3*t + (8) *g*k*r*t + ((-16)) *i*k*r*t + (8) *j*k*r*t + ((-32)) *i^2*s*t + (32) *i*j*s*t + ((-16)) *j^2*s*t + ((-32)) *k^2*s*t + (32) *k*l*s*t + ((-16)) *l^2*s*t + (32) *i*q*s*t + ((-32)) *q*r*s*t + (16) *r^2*s*t + (32) *k*s^2*t + (16) *i^2*t^2 + ((-16)) *i*j*t^2 + (8) *j^2*t^2 + (16) *k^2*t^2 + ((-24)) *h*l*t^2 + (56) *k*l*t^2 + ((-32)) *l^2*t^2 + ((-16)) *i*q*t^2 + (16) *q*r*t^2 + ((-8)) *r^2*t^2 + ((-16)) *k*s*t^2 + ((-16)) *s^2*t^2 + (16) *s*t^3 + ((-4)) *t^4 + ((-4)) *g*i*k + (2) *g*j*k + (8) *i*j*k + ((-4)) *j^2*k + ((-6)) *h*k^2 + (6) *k^3 + (4) *g*i*l + ((-4)) *i^2*l + ((-2)) *g*j*l + (2) *i*j*l + (2) *h*k*l + (4) *k^2*l + (2) *h*l^2 + (2) *k*l^2 + ((-6)) *l^3 + (32) *i*k*q + ((-16)) *j*k*q + ((-48)) *i*l*q + (24) *j*l*q + ((-24)) *h*i*r + (20) *h*j*r + (12) *g*k*r + ((-20)) *j*k*r + (4) *i*l*r + (12) *j*l*r + ((-8)) *h*r^2 + ((-8)) *g*i*t + (4) *g*j*t + (24) *i*j*t + ((-12)) *j^2*t + ((-16)) *h*k*t + (36) *k^2*t + (36) *h*l*t + ((-112)) *k*l*t + (60) *l^2*t + ((-8)) *g*r*t + (32) *i*r*t + ((-24)) *j*r*t + ((-16)) *h*t^2 + (20) *k*t^2 + ((-16)) *l*t^2 + (4) *g*i + ((-2)) *g*j + ((-34)) *i*j + (17) *j^2 + (20) *h*k + ((-23)) *k^2 + ((-24)) *h*l + (38) *k*l + ((-15)) *l^2 + (8) *i*q + ((-4)) *j*q + ((-12)) *g*r + ((-22)) *i*r + (32) *j*r + ((-38)) *k*t + (46) *l*t + (4) *t^2 + (4) *h + (24) *k + ((-29)) *l + ((-4)) *t + (1) ; ((-16)) *g*i*r*t + (8) *g*j*r*t + (16) *i*j*r*t + ((-8)) *j^2*r*t + ((-8)) *h*k*r*t + ((-16)) *k^2*r*t + (16) *h*l*r*t + (8) *k*l*r*t + (8) *g*i*r + ((-4)) *g*j*r + ((-8)) *i*j*r + (4) *j^2*r + (4) *h*k*r + (8) *k^2*r + ((-8)) *h*l*r + ((-4)) *k*l*r ; 0; 0; 0; 0; (16) *i*j*k*r + ((-8)) *j^2*k*r + (8) *k^3*r + (24) *k^2*l*r + ((-8)) *k*l^2*r + ((-16)) *i*k*r^2 + (8) *k*r^3 + ((-4)) *j*k^2*t + ((-48)) *k^2*r*t + (16) *i*k*t^2 + ((-16)) *j*k*t^2 + ((-16)) *k*q*t^2 + (24) *k*r*t^2 + (4) *j*k^2 + (8) *g*k*l + ((-4)) *i*k*l + ((-4)) *j*k*l + (32) *k^2*q + ((-48)) *k*l*q + ((-8)) *h*k*r + ((-28)) *k^2*r + (10) *k*l*r + ((-12)) *g*k*t + ((-20)) *i*k*t + (62) *j*k*t + (24) *k*q*t + ((-20)) *k*r*t + ((-12)) *g*k + (8) *i*k + ((-22)) *j*k + (22) *k*r ; 0; 0; ((-32)) *i^2*j*s + (16) *i*j^2*s + ((-32)) *i*k*l*s + (16) *i*l^2*s + (32) *i*j*q*s + ((-16)) *j^2*q*s + ((-16)) *k^2*q*s + (32) *k*l*q*s + ((-16)) *l^2*q*s + (32) *i^2*r*s + ((-16)) *i*j*r*s + (8) *j^2*r*s + (24) *k^2*r*s + ((-16)) *k*l*r*s + (8) *l^2*r*s + ((-32)) *i*q*r*s + (16) *q*r^2*s + ((-8)) *r^3*s + (32) *i*k*s*t + ((-32)) *k*r*s*t + (8) *r*s*t^2 + (8) *i^2*j + ((-4)) *i*j^2 + ((-4)) *i*k^2 + (4) *j*k^2 + (6) *i*k*l + ((-4)) *j*k*l + ((-2)) *i*l^2 + (2) *j*l^2 + ((-8)) *i*j*q + (4) *j^2*q + (4) *k^2*q + ((-8)) *k*l*q + (4) *l^2*q + ((-8)) *i^2*r + (4) *i*j*r + ((-2)) *j^2*r + ((-6)) *k^2*r + (4) *k*l*r + ((-2)) *l^2*r + (8) *i*q*r + ((-4)) *q*r^2 + (2) *r^3 + ((-40)) *i*k*s + (16) *j*k*s + (48) *i*l*s + ((-24)) *j*l*s + (8) *k*r*s + ((-8)) *i*k*t + (8) *i*l*t + ((-4)) *j*l*t + (8) *k*r*t + ((-16)) *i*s*t + (4) *r*s*t + ((-2)) *r*t^2 + (9) *i*k + ((-3)) *j*k + ((-9)) *i*l + (4) *j*l + ((-2)) *k*r + (4) *j*s + ((-4)) *r*s + (2) *j*t + ((-1)) *r*t + ((-1)) *j + (1) *r ; 0; 0; ((-16)) *i^2*j^2 + (16) *i*j^3 + ((-4)) *j^4 + ((-32)) *i*j*k*l + (16) *j^2*k*l + (16) *i*j*l^2 + ((-8)) *j^2*l^2 + ((-16)) *k^2*l^2 + (16) *k*l^3 + ((-4)) *l^4 + (32) *i^2*j*q + ((-16)) *i*j^2*q + (32) *i*k*l*q + ((-16)) *i*l^2*q + ((-32)) *i*j*q^2 + (16) *j^2*q^2 + (16) *k^2*q^2 + ((-32)) *k*l*q^2 + (16) *l^2*q^2 + (8) *i*k*l*r + ((-4)) *j*k*l*r + ((-32)) *i^2*q*r + (32) *i*j*q*r + ((-16)) *j^2*q*r + ((-32)) *k^2*q*r + (32) *k*l*q*r + ((-16)) *l^2*q*r + (32) *i*q^2*r + (16) *i^2*r^2 + ((-16)) *i*j*r^2 + (8) *j^2*r^2 + (16) *k^2*r^2 + ((-16)) *k*l*r^2 + (8) *l^2*r^2 + ((-16)) *i*q*r^2 + ((-16)) *q^2*r^2 + (16) *q*r^3 + ((-4)) *r^4 + (32) *i*j*k*s + ((-16)) *j^2*k*s + (32) *k^2*l*s + ((-16)) *k*l^2*s + ((-32)) *i*k*q*s + (32) *k*q*r*s + ((-16)) *k*r^2*s + (16) *i^2*s^2 + ((-32)) *i*j*s^2 + (16) *j^2*s^2 + ((-32)) *k*l*s^2 + (16) *l^2*s^2 + ((-8)) *k*l^2*t + (8) *l^3*t + ((-32)) *i^2*s*t + (32) *i*j*s*t + ((-16)) *j^2*s*t + ((-32)) *k^2*s*t + (32) *k*l*s*t + ((-16)) *l^2*s*t + (32) *i*q*s*t + ((-32)) *q*r*s*t + (16) *r^2*s*t + (32) *k*s^2*t + (16) *i^2*t^2 + ((-16)) *i*j*t^2 + (8) *j^2*t^2 + (16) *k^2*t^2 + (16) *k*l*t^2 + ((-40)) *l^2*t^2 + ((-16)) *i*q*t^2 + (16) *q*r*t^2 + ((-8)) *r^2*t^2 + ((-16)) *k*s*t^2 + ((-16)) *s^2*t^2 + (16) *s*t^3 + ((-4)) *t^4 + (4) *i*j*k + ((-2)) *j^2*k + (6) *h*k^2 + (2) *k^3 + (8) *g*i*l + ((-4)) *i^2*l + ((-4)) *g*j*l + ((-2)) *i*j*l + (2) *j^2*l + (2) *h*k*l + (16) *k^2*l + (4) *h*l^2 + ((-6)) *l^3 + (32) *i*k*q + ((-16)) *j*k*q + ((-48)) *i*l*q + (24) *j*l*q + ((-8)) *h*i*r + (12) *h*j*r + (4) *g*k*r + ((-16)) *i*k*r + ((-12)) *j*k*r + ((-8)) *g*l*r + (20) *i*l*r + (4) *j*l*r + ((-16)) *h*r^2 + (16) *k*r^2 + ((-8)) *g*i*t + (4) *g*j*t + (24) *i*j*t + ((-12)) *j^2*t + (8) *h*k*t + ((-12)) *k^2*t + ((-16)) *h*l*t + (36) *k*l*t + (8) *l^2*t + ((-8)) *g*r*t + (32) *i*r*t + ((-24)) *j*r*t + ((-24)) *h*t^2 + (48) *k*t^2 + ((-24)) *l*t^2 + ((-12)) *g*i + (10) *g*j + ((-26)) *i*j + (13) *j^2 + ((-16)) *h*k + ((-15)) *k^2 + ((-4)) *h*l + ((-14)) *k*l + (5) *l^2 + (8) *i*q + ((-4)) *j*q + ((-12)) *g*r + ((-22)) *i*r + (32) *j*r + (36) *h*t + ((-110)) *k*t + (82) *l*t + (4) *t^2 + ((-24)) *h + (56) *k + ((-45)) *l + ((-4)) *t + (1) ; 0; (4) *a*c^2 + ((-4)) *a*i^2 + ((-8)) *a*i*j + (4) *a*j^2 + ((-4)) *a*k^2 + ((-8)) *a*k*l + (4) *a*l^2 + (16) *a*i*q + ((-16)) *a*q^2 + (16) *a*q*r + ((-8)) *a*r^2 + (16) *a*k*s + ((-16)) *a*s^2 + (16) *a*s*t + ((-8)) *a*t^2 ; ((-8)) *a*c^2 + (4) *a*d^2 + ((-8)) *a*i^2 + ((-8)) *a*k^2 + (16) *a*i*q + ((-4)) *a*q^2 + ((-8)) *a*q*r + (4) *a*r^2 + (16) *a*k*s + ((-4)) *a*s^2 + ((-8)) *a*s*t + (4) *a*t^2 ; 0; ((-8)) *k*l*r + (16) *l*r ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *t ; 0; 0; 0; (1) ; 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; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; ((-1)) *r ; (2) *t ; ((-1)) *t ; 0; 0; 0; 0; 0; 0; (1) *l ; 0; 0; 0; 0; 0; (4) *l*t ; 0; 0; 0; 0; 0; 0; (2) *k*r*t ; (2) *k*r*t ; 0; ((-2)) *k^2*t + (4) *h*l*t + ((-2)) *k*l*t + (4) *g*r*t + ((-8)) *i*r*t + (4) *j*r*t ; 0; 0; 0; ((-2)) *g*k*r*t + (4) *i*k*r*t + ((-2)) *j*k*r*t + ((-4)) *g*l*r*t + (8) *i*l*r*t + ((-4)) *j*l*r*t ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-4)) *k*l*t^2 + (8) *l^2*t^2 ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; (1) *r ; 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) *k^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; ];
[
((-1)) *a ; 0; 0; 0; 0; 0; (1) *k ; 0; (1) *k ; 0; 0; 0; 0; 0; 0; 0; (3) *k ; (1) *j ; 0; 0; 0; ((-1)) *k ; 0; ((-2)) *r ; (2) *j*r ; (2) *k^2 + ((-4)) *g*r ; 0; (1) *h*j + ((-1)) *j*k + (1) *g*l + ((-4)) *h*r + (4) *k*r + ((-2)) *l*r ; (2) *r^2 + (1) *k*t ; 0; 0; (2) *i*k^2 + ((-1)) *h*j*l + ((-1)) *g*k*l + (1) *j*k*l + ((-1)) *g*l^2 + ((-8)) *g*i*q + (4) *g*j*q + (8) *i*j*q + ((-4)) *j^2*q + ((-4)) *h*k*q + ((-8)) *k^2*q + (8) *h*l*q + (4) *k*l*q + ((-2)) *h*k*r + (4) *k^2*r + ((-2)) *k*l*r ; ((-2)) *h*k^2 + (2) *k^3 + (4) *g*i*p + ((-2)) *g*j*p + ((-4)) *i*j*p + (2) *j^2*p + (2) *h*k*p + (4) *k^2*p + ((-4)) *h*l*p + ((-2)) *k*l*p + ((-8)) *g*i*s + (4) *g*j*s + (8) *i*j*s + ((-4)) *j^2*s + ((-4)) *h*k*s + ((-8)) *k^2*s + (8) *h*l*s + (4) *k*l*s ; ((-2)) *k^2 ; 0; 0; 0; ((-4)) *k^2*t ; 0; 0; 0; 0; 0; (2) *i*k^2 + (2) *a*h*l + ((-1)) *h*j*l + (1) *a*k*l + ((-1)) *g*k*l + (1) *j*k*l + ((-1)) *g*l^2 + ((-4)) *g*i*o + (2) *g*j*o + (4) *i*j*o + ((-2)) *j^2*o + ((-2)) *h*k*o + ((-4)) *k^2*o + (4) *h*l*o + (2) *k*l*o + ((-2)) *k*l*r ; ((-2)) *h*k^2 + (2) *k^3 ; 0; 0; 0; 0; 0; ((-8)) *g*i + (4) *g*j + (8) *i*j + ((-4)) *j^2 + ((-4)) *h*k + ((-8)) *k^2 + (8) *h*l + (4) *k*l ; ];
[
0; 0; (2) ; 0; ((-1)) ; 0; (2) *k + (2) *l ; 0; 0; (2) *k + (4) *l ; 0; 0; (3) *k ; 0; 0; 0; (2) *h + ((-2)) *k + (2) *l ; 0; (2) *h + (2) *l ; ((-2)) *g + (4) *i ; 0; 0; 0; 0; 0; 0; 0; ((-4)) *g*t + (4) *i*t + ((-2)) *g + (2) *i ; 0; 0; 0; 0; 0; 0; 0; 0; (4) *g*k*t + ((-4)) *i*k*t + (2) *g*k + ((-2)) *i*k + ((-1)) *j*k ; 0; 0; 0; 0; 0; ((-8)) *k*l*t + (4) *g*i + ((-4)) *i^2 + ((-2)) *g*j + (2) *i*j + (4) *h*k + (2) *k^2 ; 0; 0; 0; 0; (4) *i*t + ((-2)) *g + (2) *i ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; 0; 0; 0; 0; (1) *k ; ((-2)) *k + (2) *l ; (2) *i + ((-2)) *j ; 0; ((-2)) *j ; ((-2)) *l ; ((-2)) *k ; 0; 0; 0; 0; 0; 0; (2) *k*t + ((-2)) *l*t + (2) *k ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *k^2 ; 0; 0; 0; 0; 0; ((-2)) *g*k + (4) *i*k ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; ((-1)) *k + ((-2)) *l ; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *h + ((-1)) *l ; (1) *j ; 0; 0; 0; (1) *l ; 0; 0; 0; 0; 0; 0; ((-1)) *l*t ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *h*k*t + (2) *k*l*t ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
(1) ; 0; 0; ((-1)) *l ; 0; 0; ((-1)) *k + ((-2)) *l ; 0; 0; 0; 0; 0; (2) *g + ((-1)) *j ; ((-1)) *l ; 0; 0; 0; (1) *j ; 0; 0; 0; 0; 0; 0; ((-1)) *j*t ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *g*k*t + (2) *j*k*t ; 0; 0; 0; 0; 0; (4) *k*l*t ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; ((-1)) *k ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *i + (1) *j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *j*t ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *i*k*t + ((-2)) *j*k*t ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *i + ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *g + (2) *i + ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *g*k + ((-2)) *i*k ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; (1) ; 0; 0; 0; 0; ((-1)) ; 0; 0; 0; 0; ((-1)) *j ; 0; ((-1)) *t ; 0; 0; (1) *h*j ; ((-2)) *i*j + (1) *j^2 + (1) *h*k + ((-1)) *h*l + ((-1)) *k*l + (1) *l^2 + ((-2)) *g*o + (4) *i*o + ((-2)) *j*o ; 0; (1) *j ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *h*j ; ((-2)) *i*j + (1) *j^2 + (1) *h*k + ((-1)) *h*l + ((-1)) *k*l + (1) *l^2 + ((-2)) *g*o + (4) *i*o + ((-2)) *j*o ; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; ((-2)) ; 0; 0; ((-2)) *g ; 0; 0; (2) *t + ((-4)) ; 0; (2) *t + ((-2)) ; ((-8)) *q ; 0; ((-2)) *h + ((-2)) *k ; (4) *t ; ((-4)) *j*t + (2) *j ; (4) *g*t + ((-2)) *g + (2) *r ; (4) *k*t + (2) *k ; ((-2)) *k ; ((-8)) *q*t + ((-4)) *q + (2) *r ; (4) *i + ((-2)) *j ; ((-2)) *h*i*t + (2) *g*k*t + ((-2)) *i*k*t + (1) *h*i + ((-1)) *g*k + (1) *j*k + ((-1)) *i*l ; (8) *i*q + ((-4)) *j*q + ((-2)) *i*r ; 0; 0; 0; 0; 0; (8) *k*q*t + ((-4)) *k*r*t + (4) *k*q + ((-2)) *k*r ; 0; 0; (1) *h*i + ((-1)) *g*k + (1) *j*k + ((-1)) *i*l + ((-8)) *i*s + (4) *j*s ; 0; 0; (8) *i*q + ((-4)) *j*q + ((-2)) *i*r + (6) *k*t ; 0; 0; 0; 0; ((-8)) *q*t + (4) *r*t + ((-4)) *q + ((-2)) *r ; 0; 0; ];
[
0; 0; 0; 0; (2) *r ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *k ; ((-1)) *k ; ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (4) *k*r ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; (2) *i + ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *h ; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *h*k ; 0; 0; 0; 0; 0; (4) *i*k ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; ((-1)) *b ; 0; 0; 0; (1) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *h ; 0; 0; 0; ((-1)) *h*l ; (1) *g*k + (1) *j*k + ((-1)) *g*l + (2) *h*o + ((-4)) *k*o + (2) *l*o ; 0; 0; 0; ((-1)) *h ; 0; 0; 0; 0; 0; 0; ((-1)) *h*l + ((-4)) *k*p + (2) *l*p ; ((-2)) *a*k + (1) *g*k + (1) *j*k + (1) *a*l + ((-1)) *g*l + (2) *h*o ; 0; 0; 0; 0; 0; 0; ];
[
((-1)) *i ; 0; 0; 0; ((-2)) *q ; ((-1)) *t ; (1) *k ; 0; 0; 0; 0; (1) *t ; 0; 0; (2) *k*t ; ((-1)) *k*t ; ((-2)) *q*t + (1) *r*t ; 0; ((-1)) *i*k*t + (1) *j*k*t + ((-1)) *i*l*t ; 0; 0; 0; 0; 0; 0; (4) *k*q*t + ((-2)) *k*r*t ; 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; 0; ((-2)) *q + (1) *r ; 0; ((-1)) *l ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *l*s ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; (1) ; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *l ; (1) *h ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *h ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *q + (1) *r ; 0; 0; ((-1)) *h ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *h*s ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
((-1)) ; 0; 0; 0; (1) ; (1) ; 0; 0; 0; ((-1)) *h ; ((-1)) *i + (1) *j ; 0; (1) *t ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *g + ((-2)) *i + (1) *j ; 0; 0; 0; 0; (1) ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *l ; 0; ((-1)) *i + (1) *j ; (1) *t ; 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; 0; (1) ; 0; (1) *j ; (2) *k ; ((-2)) *k + (1) *l ; ((-1)) *r ; 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; 0; 0; ((-2)) *q + (1) *r ; 0; 0; 0; (1) *i + ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *i*s + (2) *j*s ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; (1) *i + ((-1)) *j ; (1) *g + ((-1)) *i ; 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; 0; 0; ((-1)) *h ; 0; (1) *g + ((-1)) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *t ; 0; 0; ];
[
0; 0; (1) *l ; 0; 0; ((-1)) *g + (1) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
0; (2) *q + ((-1)) *r ; 0; 0; 0; 0; (1) *g + ((-1)) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *g*s + (2) *i*s ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
((-1)) *g + (1) *j ; ((-1)) *g ; ((-1)) *h ; 0; (1) *r ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *r ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *i ; (1) *h + ((-1)) *k ; (1) ; 0; 0; 0; 0; 0; 0; 0; (1) *g ; 0; ((-1)) *i ; (1) *h + ((-1)) *k ; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; (1) *j ; ((-1)) *k + (1) *l ; 0; 0; (1) ; 0; 0; 0; 0; 0; ((-1)) *i ; 0; (1) *j ; ((-1)) *k + (1) *l ; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; (1) *h ; 0; 0; (1) ; 0; 0; 0; 0; 0; 0; 0; ((-1)) *g ; (1) *h ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; (1) *l ; 0; 0; 0; 0; (1) ; 0; 0; 0; 0; 0; ((-1)) *j ; (1) *l ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *f ; ((-1)) *e + (2) *i ; 0; 0; 0; 0; 0; 0; 0; 0; (1) ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *m + ((-2)) *q ; (1) *n ; 0; 0; 0; 0; 0; 0; 0; 0; (2) ; 0; ];
[
((-2)) *o + (4) *q + ((-2)) *r ; ((-2)) *p + (4) *s + ((-2)) *t + (1) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (4) ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) ; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) ; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; ];
];
c:=
(-4);