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);