Segments of chords

Geogebra sheet

Coq statement

Lemma segments_of_chords: forall A B C D M O:point,
  equaldistance O A O B ->
  equaldistance O A O C ->
  equaldistance O A O D ->
  collinear A B M ->
  collinear C D M ->
  (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D)
  \/ parallel A B C D.
Proof. geo_begin. tzR. Qed.

Algebraic version

p:=  ((-2)) *a^2*b*c*d*g +  ((-2)) *b^3*c*d*g +  (1) *a^2*c^2*d*g +  (1) *b^2*c^2*d*g +  ((-2)) *a^3*d^2*g +  ((-2)) *a*b^2*d^2*g +  (1) *a^2*d^3*g +  (1) *b^2*d^3*g +  ((-2)) *a^2*b*d*e*g +  ((-2)) *b^3*d*e*g +  (4) *b^2*c*d*e*g +  ((-2)) *b*c^2*d*e*g +  (4) *a*b*d^2*e*g +  ((-2)) *b*d^3*e*g +  (1) *a^2*d*e^2*g +  (1) *b^2*d*e^2*g +  ((-2)) *b*c*d*e^2*g +  (1) *c^2*d*e^2*g +  ((-2)) *a*d^2*e^2*g +  (1) *d^3*e^2*g +  (2) *a^2*b*c*f*g +  (2) *b^3*c*f*g +  ((-1)) *a^2*c^2*f*g +  ((-1)) *b^2*c^2*f*g +  (4) *a*b*c*d*f*g +  ((-2)) *a*c^2*d*f*g +  (3) *a^2*d^2*f*g +  ((-1)) *b^2*d^2*f*g +  ((-2)) *a*d^3*f*g +  (2) *a^2*b*e*f*g +  (2) *b^3*e*f*g +  ((-4)) *b^2*c*e*f*g +  (2) *b*c^2*e*f*g +  ((-4)) *a*b*d*e*f*g +  (2) *b*d^2*e*f*g +  ((-1)) *a^2*e^2*f*g +  ((-1)) *b^2*e^2*f*g +  (2) *b*c*e^2*f*g +  ((-1)) *c^2*e^2*f*g +  (2) *a*d*e^2*f*g +  ((-1)) *d^2*e^2*f*g +  (2) *a^3*f^2*g +  (2) *a*b^2*f^2*g +  ((-4)) *a*b*c*f^2*g +  (2) *a*c^2*f^2*g +  ((-3)) *a^2*d*f^2*g +  (1) *b^2*d*f^2*g +  ((-2)) *b*c*d*f^2*g +  (1) *c^2*d*f^2*g +  (1) *d^3*f^2*g +  ((-1)) *a^2*f^3*g +  ((-1)) *b^2*f^3*g +  (2) *b*c*f^3*g +  ((-1)) *c^2*f^3*g +  (2) *a*d*f^3*g +  ((-1)) *d^2*f^3*g +  (2) *a^2*b*d*g^2 +  (2) *b^3*d*g^2 +  ((-2)) *a^2*b*f*g^2 +  ((-2)) *b^3*f*g^2 +  ((-1)) *a^2*d*g^3 +  ((-1)) *b^2*d*g^3 +  (1) *a^2*f*g^3 +  (1) *b^2*f*g^3 +  (2) *a^2*b*c^2*h +  (2) *b^3*c^2*h +  ((-1)) *a^2*c^3*h +  ((-1)) *b^2*c^3*h +  (2) *a^3*c*d*h +  (2) *a*b^2*c*d*h +  ((-1)) *a^2*c*d^2*h +  ((-1)) *b^2*c*d^2*h +  (1) *a^2*c^2*e*h +  ((-3)) *b^2*c^2*e*h +  (2) *b*c^3*e*h +  ((-2)) *a^3*d*e*h +  ((-2)) *a*b^2*d*e*h +  ((-4)) *a*b*c*d*e*h +  (1) *a^2*d^2*e*h +  (1) *b^2*d^2*e*h +  (2) *b*c*d^2*e*h +  ((-2)) *a^2*b*e^2*h +  ((-2)) *b^3*e^2*h +  ((-1)) *a^2*c*e^2*h +  (3) *b^2*c*e^2*h +  ((-1)) *c^3*e^2*h +  (4) *a*b*d*e^2*h +  (2) *a*c*d*e^2*h +  ((-2)) *b*d^2*e^2*h +  ((-1)) *c*d^2*e^2*h +  (1) *a^2*e^3*h +  (1) *b^2*e^3*h +  ((-2)) *b*c*e^3*h +  (1) *c^2*e^3*h +  ((-2)) *a*d*e^3*h +  (1) *d^2*e^3*h +  (2) *a^3*c*f*h +  (2) *a*b^2*c*f*h +  ((-4)) *a*b*c^2*f*h +  (2) *a*c^3*f*h +  ((-4)) *a^2*c*d*f*h +  (2) *a*c*d^2*f*h +  ((-2)) *a^3*e*f*h +  ((-2)) *a*b^2*e*f*h +  (4) *a*b*c*e*f*h +  ((-2)) *a*c^2*e*f*h +  (4) *a^2*d*e*f*h +  ((-2)) *a*d^2*e*f*h +  ((-1)) *a^2*c*f^2*h +  ((-1)) *b^2*c*f^2*h +  (2) *b*c^2*f^2*h +  ((-1)) *c^3*f^2*h +  (2) *a*c*d*f^2*h +  ((-1)) *c*d^2*f^2*h +  (1) *a^2*e*f^2*h +  (1) *b^2*e*f^2*h +  ((-2)) *b*c*e*f^2*h +  (1) *c^2*e*f^2*h +  ((-2)) *a*d*e*f^2*h +  (1) *d^2*e*f^2*h +  ((-2)) *a^2*b*c*g*h +  ((-2)) *b^3*c*g*h +  (2) *a^3*d*g*h +  (2) *a*b^2*d*g*h +  (2) *a^2*b*e*g*h +  (2) *b^3*e*g*h +  ((-2)) *a^3*f*g*h +  ((-2)) *a*b^2*f*g*h +  (1) *a^2*c*g^2*h +  (1) *b^2*c*g^2*h +  ((-1)) *a^2*e*g^2*h +  ((-1)) *b^2*e*g^2*h +  ((-2)) *a^3*c*h^2 +  ((-2)) *a*b^2*c*h^2 +  (2) *a^3*e*h^2 +  (2) *a*b^2*e*h^2 +  ((-1)) *a^2*d*g*h^2 +  ((-1)) *b^2*d*g*h^2 +  (1) *a^2*f*g*h^2 +  (1) *b^2*f*g*h^2 +  (1) *a^2*c*h^3 +  (1) *b^2*c*h^3 +  ((-1)) *a^2*e*h^3 +  ((-1)) *b^2*e*h^3 +  (2) *a^2*b*c*d*j +  (2) *b^3*c*d*j +  ((-1)) *a^2*c^2*d*j +  ((-1)) *b^2*c^2*d*j +  (2) *a^3*d^2*j +  (2) *a*b^2*d^2*j +  ((-1)) *a^2*d^3*j +  ((-1)) *b^2*d^3*j +  (2) *a^2*b*d*e*j +  (2) *b^3*d*e*j +  ((-4)) *b^2*c*d*e*j +  (2) *b*c^2*d*e*j +  ((-4)) *a*b*d^2*e*j +  (2) *b*d^3*e*j +  ((-1)) *a^2*d*e^2*j +  ((-1)) *b^2*d*e^2*j +  (2) *b*c*d*e^2*j +  ((-1)) *c^2*d*e^2*j +  (2) *a*d^2*e^2*j +  ((-1)) *d^3*e^2*j +  ((-2)) *a^2*b*c*f*j +  ((-2)) *b^3*c*f*j +  (1) *a^2*c^2*f*j +  (1) *b^2*c^2*f*j +  ((-4)) *a*b*c*d*f*j +  (2) *a*c^2*d*f*j +  ((-3)) *a^2*d^2*f*j +  (1) *b^2*d^2*f*j +  (2) *a*d^3*f*j +  ((-2)) *a^2*b*e*f*j +  ((-2)) *b^3*e*f*j +  (4) *b^2*c*e*f*j +  ((-2)) *b*c^2*e*f*j +  (4) *a*b*d*e*f*j +  ((-2)) *b*d^2*e*f*j +  (1) *a^2*e^2*f*j +  (1) *b^2*e^2*f*j +  ((-2)) *b*c*e^2*f*j +  (1) *c^2*e^2*f*j +  ((-2)) *a*d*e^2*f*j +  (1) *d^2*e^2*f*j +  ((-2)) *a^3*f^2*j +  ((-2)) *a*b^2*f^2*j +  (4) *a*b*c*f^2*j +  ((-2)) *a*c^2*f^2*j +  (3) *a^2*d*f^2*j +  ((-1)) *b^2*d*f^2*j +  (2) *b*c*d*f^2*j +  ((-1)) *c^2*d*f^2*j +  ((-1)) *d^3*f^2*j +  (1) *a^2*f^3*j +  (1) *b^2*f^3*j +  ((-2)) *b*c*f^3*j +  (1) *c^2*f^3*j +  ((-2)) *a*d*f^3*j +  (1) *d^2*f^3*j +  (1) *a^2*d*g^2*j +  ((-3)) *b^2*d*g^2*j +  ((-1)) *a^2*f*g^2*j +  (3) *b^2*f*g^2*j +  (2) *b*d*g^3*j +  ((-2)) *b*f*g^3*j +  ((-2)) *a^2*b*c*h*j +  ((-2)) *b^3*c*h*j +  ((-2)) *a^3*d*h*j +  ((-2)) *a*b^2*d*h*j +  (2) *a^2*b*e*h*j +  (2) *b^3*e*h*j +  (2) *a^3*f*h*j +  (2) *a*b^2*f*h*j +  (4) *b^2*c*g*h*j +  ((-4)) *a*b*d*g*h*j +  ((-4)) *b^2*e*g*h*j +  (4) *a*b*f*g*h*j +  ((-2)) *b*c*g^2*h*j +  (2) *b*e*g^2*h*j +  (4) *a*b*c*h^2*j +  (1) *a^2*d*h^2*j +  (1) *b^2*d*h^2*j +  ((-4)) *a*b*e*h^2*j +  ((-1)) *a^2*f*h^2*j +  ((-1)) *b^2*f*h^2*j +  (2) *b*d*g*h^2*j +  ((-2)) *b*f*g*h^2*j +  ((-2)) *b*c*h^3*j +  (2) *b*e*h^3*j +  ((-2)) *a^2*b*d*j^2 +  ((-2)) *b^3*d*j^2 +  (2) *a^2*b*f*j^2 +  (2) *b^3*f*j^2 +  ((-1)) *a^2*d*g*j^2 +  (3) *b^2*d*g*j^2 +  (1) *a^2*f*g*j^2 +  ((-3)) *b^2*f*g*j^2 +  ((-1)) *d*g^3*j^2 +  (1) *f*g^3*j^2 +  (1) *a^2*c*h*j^2 +  (1) *b^2*c*h*j^2 +  (4) *a*b*d*h*j^2 +  ((-1)) *a^2*e*h*j^2 +  ((-1)) *b^2*e*h*j^2 +  ((-4)) *a*b*f*h*j^2 +  ((-2)) *b*c*g*h*j^2 +  (2) *a*d*g*h*j^2 +  (2) *b*e*g*h*j^2 +  ((-2)) *a*f*g*h*j^2 +  (1) *c*g^2*h*j^2 +  ((-1)) *e*g^2*h*j^2 +  ((-2)) *a*c*h^2*j^2 +  ((-2)) *b*d*h^2*j^2 +  (2) *a*e*h^2*j^2 +  (2) *b*f*h^2*j^2 +  ((-1)) *d*g*h^2*j^2 +  (1) *f*g*h^2*j^2 +  (1) *c*h^3*j^2 +  ((-1)) *e*h^3*j^2 +  (1) *a^2*d*j^3 +  (1) *b^2*d*j^3 +  ((-1)) *a^2*f*j^3 +  ((-1)) *b^2*f*j^3 +  ((-2)) *b*d*g*j^3 +  (2) *b*f*g*j^3 +  (1) *d*g^2*j^3 +  ((-1)) *f*g^2*j^3 +  ((-2)) *a*d*h*j^3 +  (2) *a*f*h*j^3 +  (1) *d*h^2*j^3 +  ((-1)) *f*h^2*j^3 +  ((-2)) *a^2*b*c^2*l +  ((-2)) *b^3*c^2*l +  (1) *a^2*c^3*l +  (1) *b^2*c^3*l +  ((-2)) *a^3*c*d*l +  ((-2)) *a*b^2*c*d*l +  (1) *a^2*c*d^2*l +  (1) *b^2*c*d^2*l +  ((-1)) *a^2*c^2*e*l +  (3) *b^2*c^2*e*l +  ((-2)) *b*c^3*e*l +  (2) *a^3*d*e*l +  (2) *a*b^2*d*e*l +  (4) *a*b*c*d*e*l +  ((-1)) *a^2*d^2*e*l +  ((-1)) *b^2*d^2*e*l +  ((-2)) *b*c*d^2*e*l +  (2) *a^2*b*e^2*l +  (2) *b^3*e^2*l +  (1) *a^2*c*e^2*l +  ((-3)) *b^2*c*e^2*l +  (1) *c^3*e^2*l +  ((-4)) *a*b*d*e^2*l +  ((-2)) *a*c*d*e^2*l +  (2) *b*d^2*e^2*l +  (1) *c*d^2*e^2*l +  ((-1)) *a^2*e^3*l +  ((-1)) *b^2*e^3*l +  (2) *b*c*e^3*l +  ((-1)) *c^2*e^3*l +  (2) *a*d*e^3*l +  ((-1)) *d^2*e^3*l +  ((-2)) *a^3*c*f*l +  ((-2)) *a*b^2*c*f*l +  (4) *a*b*c^2*f*l +  ((-2)) *a*c^3*f*l +  (4) *a^2*c*d*f*l +  ((-2)) *a*c*d^2*f*l +  (2) *a^3*e*f*l +  (2) *a*b^2*e*f*l +  ((-4)) *a*b*c*e*f*l +  (2) *a*c^2*e*f*l +  ((-4)) *a^2*d*e*f*l +  (2) *a*d^2*e*f*l +  (1) *a^2*c*f^2*l +  (1) *b^2*c*f^2*l +  ((-2)) *b*c^2*f^2*l +  (1) *c^3*f^2*l +  ((-2)) *a*c*d*f^2*l +  (1) *c*d^2*f^2*l +  ((-1)) *a^2*e*f^2*l +  ((-1)) *b^2*e*f^2*l +  (2) *b*c*e*f^2*l +  ((-1)) *c^2*e*f^2*l +  (2) *a*d*e*f^2*l +  ((-1)) *d^2*e*f^2*l +  (2) *a^2*b*c*g*l +  (2) *b^3*c*g*l +  (2) *a^3*d*g*l +  (2) *a*b^2*d*g*l +  ((-2)) *a^2*b*e*g*l +  ((-2)) *b^3*e*g*l +  ((-2)) *a^3*f*g*l +  ((-2)) *a*b^2*f*g*l +  ((-1)) *a^2*c*g^2*l +  ((-1)) *b^2*c*g^2*l +  ((-4)) *a*b*d*g^2*l +  (1) *a^2*e*g^2*l +  (1) *b^2*e*g^2*l +  (4) *a*b*f*g^2*l +  (2) *a*d*g^3*l +  ((-2)) *a*f*g^3*l +  (4) *a*b*c*g*h*l +  ((-4)) *a^2*d*g*h*l +  ((-4)) *a*b*e*g*h*l +  (4) *a^2*f*g*h*l +  ((-2)) *a*c*g^2*h*l +  (2) *a*e*g^2*h*l +  (3) *a^2*c*h^2*l +  ((-1)) *b^2*c*h^2*l +  ((-3)) *a^2*e*h^2*l +  (1) *b^2*e*h^2*l +  (2) *a*d*g*h^2*l +  ((-2)) *a*f*g*h^2*l +  ((-2)) *a*c*h^3*l +  (2) *a*e*h^3*l +  (2) *a^2*b*c*j*l +  (2) *b^3*c*j*l +  ((-2)) *a^3*d*j*l +  ((-2)) *a*b^2*d*j*l +  ((-2)) *a^2*b*e*j*l +  ((-2)) *b^3*e*j*l +  (2) *a^3*f*j*l +  (2) *a*b^2*f*j*l +  ((-4)) *b^2*c*g*j*l +  (4) *a*b*d*g*j*l +  (4) *b^2*e*g*j*l +  ((-4)) *a*b*f*g*j*l +  (2) *b*c*g^2*j*l +  ((-2)) *a*d*g^2*j*l +  ((-2)) *b*e*g^2*j*l +  (2) *a*f*g^2*j*l +  ((-4)) *a*b*c*h*j*l +  (4) *a^2*d*h*j*l +  (4) *a*b*e*h*j*l +  ((-4)) *a^2*f*h*j*l +  (2) *b*c*h^2*j*l +  ((-2)) *a*d*h^2*j*l +  ((-2)) *b*e*h^2*j*l +  (2) *a*f*h^2*j*l +  ((-1)) *a^2*c*j^2*l +  ((-1)) *b^2*c*j^2*l +  (1) *a^2*e*j^2*l +  (1) *b^2*e*j^2*l +  (2) *b*c*g*j^2*l +  ((-2)) *b*e*g*j^2*l +  ((-1)) *c*g^2*j^2*l +  (1) *e*g^2*j^2*l +  (2) *a*c*h*j^2*l +  ((-2)) *a*e*h*j^2*l +  ((-1)) *c*h^2*j^2*l +  (1) *e*h^2*j^2*l +  (2) *a^3*c*l^2 +  (2) *a*b^2*c*l^2 +  ((-2)) *a^3*e*l^2 +  ((-2)) *a*b^2*e*l^2 +  ((-4)) *a*b*c*g*l^2 +  ((-1)) *a^2*d*g*l^2 +  ((-1)) *b^2*d*g*l^2 +  (4) *a*b*e*g*l^2 +  (1) *a^2*f*g*l^2 +  (1) *b^2*f*g*l^2 +  (2) *a*c*g^2*l^2 +  (2) *b*d*g^2*l^2 +  ((-2)) *a*e*g^2*l^2 +  ((-2)) *b*f*g^2*l^2 +  ((-1)) *d*g^3*l^2 +  (1) *f*g^3*l^2 +  ((-3)) *a^2*c*h*l^2 +  (1) *b^2*c*h*l^2 +  (3) *a^2*e*h*l^2 +  ((-1)) *b^2*e*h*l^2 +  ((-2)) *b*c*g*h*l^2 +  (2) *a*d*g*h*l^2 +  (2) *b*e*g*h*l^2 +  ((-2)) *a*f*g*h*l^2 +  (1) *c*g^2*h*l^2 +  ((-1)) *e*g^2*h*l^2 +  ((-1)) *d*g*h^2*l^2 +  (1) *f*g*h^2*l^2 +  (1) *c*h^3*l^2 +  ((-1)) *e*h^3*l^2 +  (1) *a^2*d*j*l^2 +  (1) *b^2*d*j*l^2 +  ((-1)) *a^2*f*j*l^2 +  ((-1)) *b^2*f*j*l^2 +  ((-2)) *b*d*g*j*l^2 +  (2) *b*f*g*j*l^2 +  (1) *d*g^2*j*l^2 +  ((-1)) *f*g^2*j*l^2 +  ((-2)) *a*d*h*j*l^2 +  (2) *a*f*h*j*l^2 +  (1) *d*h^2*j*l^2 +  ((-1)) *f*h^2*j*l^2 +  ((-1)) *a^2*c*l^3 +  ((-1)) *b^2*c*l^3 +  (1) *a^2*e*l^3 +  (1) *b^2*e*l^3 +  (2) *b*c*g*l^3 +  ((-2)) *b*e*g*l^3 +  ((-1)) *c*g^2*l^3 +  (1) *e*g^2*l^3 +  (2) *a*c*h*l^3 +  ((-2)) *a*e*h*l^3 +  ((-1)) *c*h^2*l^3 +  (1) *e*h^2*l^3 
F:= [
 ((-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)) *c^2 +  ((-1)) *d^2 +  (2) *c*i +  ((-2)) *i*j +  (1) *j^2 +  (2) *d*k +  ((-2)) *k*l +  (1) *l^2 ;
 (1) *a*g +  ((-1)) *b*h +  ((-1)) *a*j +  (1) *h*j +  (1) *b*l +  ((-1)) *g*l ;
 (1) *a*c +  ((-1)) *b*d +  ((-1)) *a*e +  (1) *d*e +  (1) *b*f +  ((-1)) *c*f ;
];

Certificate

CR:=[
 (2) *f +  ((-2)) *k ;  (2) *b*d +  ((-2)) *d*e +  ((-2)) *b*f +  ((-2)) *d*i +  (2) *f*i +  (2) *d*j +  ((-2)) *f*j +  (2) *e*k ;  (2) *b*h +  (2) *e*h +  ((-2)) *h*i +  ((-2)) *h*j +  ((-2)) *b*l +  ((-2)) *e*l +  (2) *i*l +  (2) *j*l ;  ((-2)) *b^2*e +  ((-2)) *b*d*f +  (4) *b^2*i +  (2) *b*e*i +  (2) *d*f*i +  ((-4)) *b*i^2 +  ((-4)) *b*i*j +  (4) *i^2*j +  (2) *b*j^2 +  ((-2)) *i*j^2 +  (2) *b*d*k +  ((-2)) *d*e*k +  (2) *b*f*k +  (2) *d*e*l +  ((-2)) *d*i*l +  ((-2)) *f*i*l +  ((-4)) *b*k*l +  (2) *e*k*l +  (2) *b*l^2 +  ((-2)) *e*l^2 +  (2) *i*l^2 ;  (2) *b^2*g +  ((-2)) *b*e*g +  ((-4)) *b*f*h +  ((-2)) *b*g*i +  (2) *e*g*i +  (2) *f*h*i +  ((-2)) *b^2*j +  (2) *b*e*j +  (2) *f*h*j +  (2) *b*i*j +  ((-2)) *e*i*j +  (2) *f*g*k +  ((-2)) *e*h*k +  ((-2)) *f*j*k +  (2) *h*j*k +  (4) *b*f*l +  ((-2)) *f*g*l +  (2) *b*h*l +  ((-2)) *f*i*l +  ((-2)) *h*j*l +  (2) *e*k*l +  ((-2)) *g*k*l +  ((-2)) *b*l^2 +  (2) *g*l^2 ;  (2) *b^2*c +  ((-2)) *b^2*e +  ((-2)) *b*c*i +  (2) *b*e*i +  ((-2)) *b*c*j +  (2) *b*e*j +  (2) *c*i*j +  ((-2)) *e*i*j +  (2) *b*d*k +  ((-2)) *b*f*k +  ((-2)) *d*j*k +  (2) *f*j*k +  ((-4)) *b*d*l +  (2) *d*e*l +  (4) *b*f*l +  ((-2)) *c*f*l +  (2) *d*i*l +  ((-2)) *f*i*l +  (2) *c*k*l +  ((-2)) *e*k*l ;  (2) *a^2*d*h +  (2) *a*b*e*h +  ((-6)) *b*d*e*h +  (2) *a^2*f*h +  (2) *b^2*f*h +  ((-2)) *a*d*f*h +  ((-2)) *a^2*h^2 +  ((-2)) *b^2*h^2 +  ((-2)) *a*f*h^2 +  (2) *b*d*h*i +  ((-2)) *a*e*h*i +  (2) *d*e*h*i +  ((-2)) *b^2*e*j +  ((-2)) *b*d*f*j +  ((-4)) *a*b*h*j +  (2) *b*d*h*j +  ((-2)) *a*e*h*j +  (2) *d*e*h*j +  (4) *b*h^2*j +  (4) *b^2*i*j +  (2) *b*e*i*j +  (2) *d*f*i*j +  (4) *a*h*i*j +  ((-2)) *d*h*i*j +  ((-2)) *f*h*i*j +  ((-4)) *b*i^2*j +  (2) *a*h*j^2 +  ((-2)) *h^2*j^2 +  ((-4)) *b*i*j^2 +  (4) *i^2*j^2 +  (2) *b*j^3 +  ((-2)) *i*j^3 +  ((-4)) *b^2*h*k +  ((-2)) *a*d*h*k +  ((-2)) *a*f*h*k +  (2) *d*f*h*k +  (2) *a*h^2*k +  (8) *b*h*i*k +  (2) *b*d*j*k +  ((-2)) *d*e*j*k +  (2) *b*f*j*k +  (2) *e*h*j*k +  ((-8)) *h*i*j*k +  (2) *h*j^2*k +  (4) *a*h*k^2 +  ((-2)) *a^2*d*l +  ((-2)) *a*b*e*l +  (6) *b*d*e*l +  ((-2)) *a^2*f*l +  ((-2)) *b^2*f*l +  (2) *a*d*f*l +  (4) *b^2*h*l +  (2) *b*e*h*l +  (4) *a*h^2*l +  ((-2)) *b*d*i*l +  (2) *a*e*i*l +  ((-2)) *d*e*i*l +  ((-8)) *b*h*i*l +  (4) *a*b*j*l +  ((-2)) *b*d*j*l +  (2) *a*e*j*l +  ((-4)) *b*h*j*l +  ((-2)) *e*h*j*l +  ((-4)) *a*i*j*l +  (8) *h*i*j*l +  ((-2)) *a*j^2*l +  (4) *b^2*k*l +  (2) *a*d*k*l +  (2) *a*f*k*l +  ((-2)) *d*f*k*l +  ((-4)) *a*h*k*l +  ((-8)) *b*i*k*l +  ((-4)) *b*j*k*l +  (8) *i*j*k*l +  ((-2)) *j^2*k*l +  ((-4)) *a*k^2*l +  ((-4)) *h*k^2*l +  (2) *a^2*l^2 +  ((-2)) *b^2*l^2 +  ((-2)) *b*e*l^2 +  ((-2)) *a*h*l^2 +  ((-2)) *h^2*l^2 +  (8) *b*i*l^2 +  (2) *b*j*l^2 +  ((-6)) *i*j*l^2 +  (2) *j^2*l^2 +  (4) *a*k*l^2 +  (6) *h*k*l^2 +  (4) *k^2*l^2 +  ((-2)) *a*l^3 +  ((-6)) *k*l^3 +  (2) *l^4 ;  ((-2)) *a*b*c*d +  ((-2)) *a^2*d^2 +  (2) *b^2*c*e +  ((-2)) *a*b*d*e +  (2) *b*d^2*e +  (2) *a*b*c*f +  (4) *b*c*d*f +  (4) *a*d^2*f +  (2) *a*b*e*f +  ((-2)) *b*d*e*f +  (2) *a^2*f^2 +  ((-2)) *b*c*f^2 +  ((-4)) *a*d*f^2 +  ((-2)) *a*b*c*h +  (2) *a^2*d*h +  (2) *b^2*d*h +  (2) *a*b*e*h +  ((-2)) *a^2*f*h +  ((-2)) *b^2*f*h +  ((-8)) *b^2*c*i +  (2) *a*c*d*i +  ((-2)) *b*d^2*i +  (4) *b^2*e*i +  ((-2)) *b*c*e*i +  (6) *a*d*e*i +  ((-2)) *d^2*e*i +  ((-6)) *a*c*f*i +  ((-4)) *c*d*f*i +  ((-2)) *a*e*f*i +  (2) *d*e*f*i +  (2) *b*f^2*i +  (2) *c*f^2*i +  (2) *a*c*h*i +  ((-2)) *a*e*h*i +  (8) *b*c*i^2 +  ((-4)) *b*e*i^2 +  (2) *b^2*c*j +  (2) *a*b*d*j +  ((-2)) *b^2*e*j +  ((-2)) *a*d*e*j +  ((-2)) *a*b*f*j +  (2) *a*c*f*j +  ((-6)) *b*d*h*j +  (2) *d*e*h*j +  (6) *b*f*h*j +  ((-2)) *c*f*h*j +  (6) *b*c*i*j +  ((-6)) *a*d*i*j +  (4) *d^2*i*j +  ((-2)) *b*e*i*j +  (6) *a*f*i*j +  ((-4)) *f^2*i*j +  (2) *d*h*i*j +  ((-2)) *f*h*i*j +  ((-8)) *c*i^2*j +  (4) *e*i^2*j +  ((-4)) *b*c*j^2 +  (2) *a*d*j^2 +  ((-2)) *d^2*j^2 +  (2) *b*e*j^2 +  ((-2)) *a*f*j^2 +  (2) *f^2*j^2 +  (4) *c*i*j^2 +  ((-2)) *e*i*j^2 +  ((-4)) *b^2*d*k +  (2) *a*d^2*k +  (2) *b*d*e*k +  (4) *b^2*f*k +  ((-4)) *b*c*f*k +  ((-6)) *d^2*f*k +  ((-2)) *b*e*f*k +  (2) *c*e*f*k +  ((-2)) *a*f^2*k +  (6) *d*f^2*k +  ((-2)) *a*d*h*k +  (2) *a*f*h*k +  (4) *a*c*i*k +  ((-4)) *a*e*i*k +  ((-2)) *a*c*j*k +  (2) *b*d*j*k +  (2) *a*e*j*k +  ((-2)) *b*f*j*k +  (2) *c*h*j*k +  ((-2)) *e*h*j*k +  (2) *a*b*c*l +  (2) *a^2*d*l +  ((-2)) *b*c*d*l +  ((-2)) *a*d^2*l +  ((-2)) *a*b*e*l +  ((-2)) *a^2*f*l +  (2) *d^2*f*l +  (2) *b*e*f*l +  ((-2)) *c*e*f*l +  (2) *a*f^2*l +  ((-2)) *d*f^2*l +  (2) *b*c*h*l +  ((-2)) *a*d*h*l +  ((-2)) *b*e*h*l +  (2) *a*f*h*l +  ((-2)) *a*c*i*l +  (6) *b*d*i*l +  (2) *c*d*i*l +  (2) *a*e*i*l +  ((-4)) *d*e*i*l +  ((-6)) *b*f*i*l +  (6) *c*f*i*l +  ((-2)) *c*h*i*l +  (2) *e*h*i*l +  ((-4)) *d*i*j*l +  (4) *f*i*j*l +  (2) *d*j^2*l +  ((-2)) *f*j^2*l +  (6) *b*c*k*l +  ((-2)) *a*d*k*l +  (4) *d^2*k*l +  ((-2)) *b*e*k*l +  ((-2)) *c*e*k*l +  (2) *a*f*k*l +  ((-4)) *f^2*k*l +  (2) *d*h*k*l +  ((-2)) *f*h*k*l +  ((-4)) *c*i*k*l +  (4) *e*i*k*l +  ((-4)) *b*c*l^2 +  (2) *a*d*l^2 +  ((-2)) *d^2*l^2 +  (2) *b*e*l^2 +  (2) *c*e*l^2 +  ((-2)) *a*f*l^2 +  (2) *f^2*l^2 +  ((-2)) *e*i*l^2 +  ((-4)) *d*k*l^2 +  (4) *f*k*l^2 +  (2) *d*l^3 +  ((-2)) *f*l^3 ;  ((-1)) *a^2*d*g +  ((-1)) *b^2*d*g +  (2) *b*d*e*g +  (1) *a^2*f*g +  ((-1)) *b^2*f*g +  (2) *a*d*f*g +  ((-2)) *a*f^2*g +  ((-2)) *a^2*b*h +  ((-2)) *b^3*h +  (1) *a^2*c*h +  (1) *b^2*c*h +  ((-1)) *a^2*e*h +  (3) *b^2*e*h +  ((-2)) *b*c*e*h +  (2) *a*b*f*h +  ((-2)) *a*c*f*h +  (2) *b*f^2*h +  ((-2)) *d*e*g*i +  (2) *b*f*g*i +  (2) *a^2*h*i +  (2) *b^2*h*i +  ((-4)) *b*e*h*i +  (2) *c*e*h*i +  ((-2)) *a*f*h*i +  (1) *a^2*d*j +  (1) *b^2*d*j +  ((-2)) *b*d*e*j +  ((-1)) *a^2*f*j +  (1) *b^2*f*j +  ((-2)) *a*d*f*j +  (2) *a*f^2*j +  (2) *a*f*h*j +  ((-2)) *f^2*h*j +  (2) *d*e*i*j +  ((-2)) *b*f*i*j +  (2) *d*g*i*j +  ((-2)) *f*g*i*j +  ((-2)) *c*h*i*j +  (2) *e*h*i*j +  ((-1)) *d*g*j^2 +  (1) *f*g*j^2 +  (1) *c*h*j^2 +  ((-1)) *e*h*j^2 +  ((-2)) *d*i*j^2 +  (2) *f*i*j^2 +  (1) *d*j^3 +  ((-1)) *f*j^3 +  ((-2)) *d*f*g*k +  (2) *c*f*h*k +  (2) *d*f*j*k +  ((-2)) *f*h*j*k +  (2) *a^2*b*l +  (2) *b^3*l +  ((-1)) *a^2*c*l +  ((-1)) *b^2*c*l +  (1) *a^2*e*l +  ((-3)) *b^2*e*l +  (2) *b*c*e*l +  ((-2)) *a*b*f*l +  (2) *a*c*f*l +  ((-2)) *b*f^2*l +  (2) *f^2*g*l +  ((-2)) *b*f*h*l +  ((-2)) *a^2*i*l +  ((-2)) *b^2*i*l +  (4) *b*e*i*l +  ((-2)) *c*e*i*l +  (2) *a*f*i*l +  ((-2)) *a*f*j*l +  (2) *f*h*j*l +  (2) *c*i*j*l +  ((-2)) *e*i*j*l +  ((-1)) *c*j^2*l +  (1) *e*j^2*l +  ((-2)) *c*f*k*l +  (2) *d*g*k*l +  ((-2)) *c*h*k*l +  (2) *e*h*k*l +  ((-2)) *d*j*k*l +  (2) *f*j*k*l +  (2) *b*f*l^2 +  ((-1)) *d*g*l^2 +  ((-1)) *f*g*l^2 +  (1) *c*h*l^2 +  ((-1)) *e*h*l^2 +  (1) *d*j*l^2 +  ((-1)) *f*j*l^2 +  (2) *c*k*l^2 +  ((-2)) *e*k*l^2 +  ((-1)) *c*l^3 +  (1) *e*l^3 ;  ((-2)) *a*b^2*g +  (2) *a*b*c*g +  ((-1)) *a^2*d*g +  (1) *b^2*d*g +  ((-1)) *c^2*d*g +  (2) *a*d^2*g +  ((-1)) *d^3*g +  (1) *a^2*f*g +  (1) *b^2*f*g +  ((-2)) *b*c*f*g +  (1) *c^2*f*g +  ((-2)) *a*d*f*g +  (1) *d^2*f*g +  (2) *b^3*h +  ((-1)) *a^2*c*h +  ((-3)) *b^2*c*h +  (1) *c^3*h +  (2) *a*b*d*h +  ((-2)) *b*d^2*h +  (1) *c*d^2*h +  ((-1)) *a^2*e*h +  ((-1)) *b^2*e*h +  (2) *b*c*e*h +  ((-1)) *c^2*e*h +  (2) *a*d*e*h +  ((-1)) *d^2*e*h +  (2) *a*b*g*i +  ((-2)) *a*c*g*i +  ((-2)) *b*d*g*i +  (2) *c*d*g*i +  ((-2)) *b^2*h*i +  (4) *b*c*h*i +  ((-2)) *c^2*h*i +  (2) *a*b^2*j +  ((-2)) *a*b*c*j +  (1) *a^2*d*j +  ((-1)) *b^2*d*j +  (1) *c^2*d*j +  ((-2)) *a*d^2*j +  (1) *d^3*j +  ((-1)) *a^2*f*j +  ((-1)) *b^2*f*j +  (2) *b*c*f*j +  ((-1)) *c^2*f*j +  (2) *a*d*f*j +  ((-1)) *d^2*f*j +  (2) *a^2*h*j +  ((-4)) *a*d*h*j +  (2) *d^2*h*j +  ((-2)) *a*b*i*j +  (2) *a*c*i*j +  (2) *b*d*i*j +  ((-2)) *c*d*i*j +  ((-2)) *a*d*g*k +  (2) *d^2*g*k +  (2) *a*c*h*k +  ((-2)) *c*d*h*k +  (2) *a*d*j*k +  ((-2)) *d^2*j*k +  ((-2)) *a*h*j*k +  (2) *d*h*j*k +  ((-2)) *b^3*l +  (1) *a^2*c*l +  (3) *b^2*c*l +  ((-1)) *c^3*l +  ((-2)) *a*b*d*l +  (2) *b*d^2*l +  ((-1)) *c*d^2*l +  (1) *a^2*e*l +  (1) *b^2*e*l +  ((-2)) *b*c*e*l +  (1) *c^2*e*l +  ((-2)) *a*d*e*l +  (1) *d^2*e*l +  (2) *a*d*g*l +  ((-2)) *d^2*g*l +  ((-2)) *a*b*h*l +  (2) *b*d*h*l +  (2) *b^2*i*l +  ((-4)) *b*c*i*l +  (2) *c^2*i*l +  ((-2)) *a^2*j*l +  (2) *a*d*j*l +  (2) *a*h*j*l +  ((-2)) *d*h*j*l +  ((-2)) *a*c*k*l +  (2) *c*d*k*l +  (2) *a*g*k*l +  ((-2)) *d*g*k*l +  (2) *a*b*l^2 +  ((-2)) *b*d*l^2 +  ((-2)) *a*g*l^2 +  (2) *d*g*l^2 ;  ((-2)) *a^2*b*d +  ((-2)) *b^3*d +  (2) *a^2*b*f +  (2) *b^3*f +  (1) *a^2*d*g +  (1) *b^2*d*g +  ((-1)) *a^2*f*g +  ((-1)) *b^2*f*g +  ((-1)) *a^2*c*h +  ((-1)) *b^2*c*h +  (1) *a^2*e*h +  (1) *b^2*e*h +  (2) *a^2*d*i +  (2) *b^2*d*i +  ((-2)) *a^2*f*i +  ((-2)) *b^2*f*i +  ((-1)) *a^2*d*j +  (3) *b^2*d*j +  (1) *a^2*f*j +  ((-3)) *b^2*f*j +  ((-2)) *b*d*g*j +  (2) *b*f*g*j +  (2) *b*c*h*j +  ((-2)) *b*e*h*j +  ((-4)) *b*d*i*j +  (4) *b*f*i*j +  (1) *d*g*j^2 +  ((-1)) *f*g*j^2 +  ((-1)) *c*h*j^2 +  (1) *e*h*j^2 +  (2) *d*i*j^2 +  ((-2)) *f*i*j^2 +  ((-1)) *d*j^3 +  (1) *f*j^3 +  (1) *a^2*c*l +  ((-1)) *b^2*c*l +  (2) *a*b*d*l +  ((-1)) *a^2*e*l +  (1) *b^2*e*l +  (2) *a*d*e*l +  ((-2)) *a*b*f*l +  ((-2)) *a*c*f*l +  ((-2)) *a*d*g*l +  (2) *a*f*g*l +  (2) *a*c*h*l +  ((-2)) *a*e*h*l +  (2) *b*c*i*l +  ((-2)) *a*d*i*l +  ((-2)) *b*e*i*l +  (2) *a*f*i*l +  ((-2)) *c*i*j*l +  (2) *e*i*j*l +  (1) *c*j^2*l +  ((-1)) *e*j^2*l +  (2) *a*c*k*l +  ((-2)) *b*d*k*l +  ((-2)) *a*e*k*l +  (2) *b*f*k*l +  (2) *d*j*k*l +  ((-2)) *f*j*k*l +  ((-2)) *a*c*l^2 +  (2) *b*d*l^2 +  (2) *a*e*l^2 +  ((-2)) *d*e*l^2 +  ((-2)) *b*f*l^2 +  (2) *c*f*l^2 +  (1) *d*g*l^2 +  ((-1)) *f*g*l^2 +  ((-1)) *c*h*l^2 +  (1) *e*h*l^2 +  ((-1)) *d*j*l^2 +  (1) *f*j*l^2 +  ((-2)) *c*k*l^2 +  (2) *e*k*l^2 +  (1) *c*l^3 +  ((-1)) *e*l^3 ; ];

C:=[
[
 (2) *f +  ((-2)) *k ;  (2) *b*d +  ((-2)) *d*e +  ((-2)) *b*f +  ((-2)) *d*i +  (2) *f*i +  (2) *d*j +  ((-2)) *f*j +  (2) *e*k ;  (2) *b*h +  (2) *e*h +  ((-2)) *h*i +  ((-2)) *h*j +  ((-2)) *b*l +  ((-2)) *e*l +  (2) *i*l +  (2) *j*l ;  ((-2)) *b^2*e +  ((-2)) *b*d*f +  (4) *b^2*i +  (2) *b*e*i +  (2) *d*f*i +  ((-4)) *b*i^2 +  ((-4)) *b*i*j +  (4) *i^2*j +  (2) *b*j^2 +  ((-2)) *i*j^2 +  (2) *b*d*k +  ((-2)) *d*e*k +  (2) *b*f*k +  (2) *d*e*l +  ((-2)) *d*i*l +  ((-2)) *f*i*l +  ((-4)) *b*k*l +  (2) *e*k*l +  (2) *b*l^2 +  ((-2)) *e*l^2 +  (2) *i*l^2 ;  (2) *b^2*g +  ((-2)) *b*e*g +  ((-4)) *b*f*h +  ((-2)) *b*g*i +  (2) *e*g*i +  (2) *f*h*i +  ((-2)) *b^2*j +  (2) *b*e*j +  (2) *f*h*j +  (2) *b*i*j +  ((-2)) *e*i*j +  (2) *f*g*k +  ((-2)) *e*h*k +  ((-2)) *f*j*k +  (2) *h*j*k +  (4) *b*f*l +  ((-2)) *f*g*l +  (2) *b*h*l +  ((-2)) *f*i*l +  ((-2)) *h*j*l +  (2) *e*k*l +  ((-2)) *g*k*l +  ((-2)) *b*l^2 +  (2) *g*l^2 ;  (2) *b^2*c +  ((-2)) *b^2*e +  ((-2)) *b*c*i +  (2) *b*e*i +  ((-2)) *b*c*j +  (2) *b*e*j +  (2) *c*i*j +  ((-2)) *e*i*j +  (2) *b*d*k +  ((-2)) *b*f*k +  ((-2)) *d*j*k +  (2) *f*j*k +  ((-4)) *b*d*l +  (2) *d*e*l +  (4) *b*f*l +  ((-2)) *c*f*l +  (2) *d*i*l +  ((-2)) *f*i*l +  (2) *c*k*l +  ((-2)) *e*k*l ;  (2) *a^2*d*h +  (2) *a*b*e*h +  ((-6)) *b*d*e*h +  (2) *a^2*f*h +  (2) *b^2*f*h +  ((-2)) *a*d*f*h +  ((-2)) *a^2*h^2 +  ((-2)) *b^2*h^2 +  ((-2)) *a*f*h^2 +  (2) *b*d*h*i +  ((-2)) *a*e*h*i +  (2) *d*e*h*i +  ((-2)) *b^2*e*j +  ((-2)) *b*d*f*j +  ((-4)) *a*b*h*j +  (2) *b*d*h*j +  ((-2)) *a*e*h*j +  (2) *d*e*h*j +  (4) *b*h^2*j +  (4) *b^2*i*j +  (2) *b*e*i*j +  (2) *d*f*i*j +  (4) *a*h*i*j +  ((-2)) *d*h*i*j +  ((-2)) *f*h*i*j +  ((-4)) *b*i^2*j +  (2) *a*h*j^2 +  ((-2)) *h^2*j^2 +  ((-4)) *b*i*j^2 +  (4) *i^2*j^2 +  (2) *b*j^3 +  ((-2)) *i*j^3 +  ((-4)) *b^2*h*k +  ((-2)) *a*d*h*k +  ((-2)) *a*f*h*k +  (2) *d*f*h*k +  (2) *a*h^2*k +  (8) *b*h*i*k +  (2) *b*d*j*k +  ((-2)) *d*e*j*k +  (2) *b*f*j*k +  (2) *e*h*j*k +  ((-8)) *h*i*j*k +  (2) *h*j^2*k +  (4) *a*h*k^2 +  ((-2)) *a^2*d*l +  ((-2)) *a*b*e*l +  (6) *b*d*e*l +  ((-2)) *a^2*f*l +  ((-2)) *b^2*f*l +  (2) *a*d*f*l +  (4) *b^2*h*l +  (2) *b*e*h*l +  (4) *a*h^2*l +  ((-2)) *b*d*i*l +  (2) *a*e*i*l +  ((-2)) *d*e*i*l +  ((-8)) *b*h*i*l +  (4) *a*b*j*l +  ((-2)) *b*d*j*l +  (2) *a*e*j*l +  ((-4)) *b*h*j*l +  ((-2)) *e*h*j*l +  ((-4)) *a*i*j*l +  (8) *h*i*j*l +  ((-2)) *a*j^2*l +  (4) *b^2*k*l +  (2) *a*d*k*l +  (2) *a*f*k*l +  ((-2)) *d*f*k*l +  ((-4)) *a*h*k*l +  ((-8)) *b*i*k*l +  ((-4)) *b*j*k*l +  (8) *i*j*k*l +  ((-2)) *j^2*k*l +  ((-4)) *a*k^2*l +  ((-4)) *h*k^2*l +  (2) *a^2*l^2 +  ((-2)) *b^2*l^2 +  ((-2)) *b*e*l^2 +  ((-2)) *a*h*l^2 +  ((-2)) *h^2*l^2 +  (8) *b*i*l^2 +  (2) *b*j*l^2 +  ((-6)) *i*j*l^2 +  (2) *j^2*l^2 +  (4) *a*k*l^2 +  (6) *h*k*l^2 +  (4) *k^2*l^2 +  ((-2)) *a*l^3 +  ((-6)) *k*l^3 +  (2) *l^4 ;  ((-2)) *a*b*c*d +  ((-2)) *a^2*d^2 +  (2) *b^2*c*e +  ((-2)) *a*b*d*e +  (2) *b*d^2*e +  (2) *a*b*c*f +  (4) *b*c*d*f +  (4) *a*d^2*f +  (2) *a*b*e*f +  ((-2)) *b*d*e*f +  (2) *a^2*f^2 +  ((-2)) *b*c*f^2 +  ((-4)) *a*d*f^2 +  ((-2)) *a*b*c*h +  (2) *a^2*d*h +  (2) *b^2*d*h +  (2) *a*b*e*h +  ((-2)) *a^2*f*h +  ((-2)) *b^2*f*h +  ((-8)) *b^2*c*i +  (2) *a*c*d*i +  ((-2)) *b*d^2*i +  (4) *b^2*e*i +  ((-2)) *b*c*e*i +  (6) *a*d*e*i +  ((-2)) *d^2*e*i +  ((-6)) *a*c*f*i +  ((-4)) *c*d*f*i +  ((-2)) *a*e*f*i +  (2) *d*e*f*i +  (2) *b*f^2*i +  (2) *c*f^2*i +  (2) *a*c*h*i +  ((-2)) *a*e*h*i +  (8) *b*c*i^2 +  ((-4)) *b*e*i^2 +  (2) *b^2*c*j +  (2) *a*b*d*j +  ((-2)) *b^2*e*j +  ((-2)) *a*d*e*j +  ((-2)) *a*b*f*j +  (2) *a*c*f*j +  ((-6)) *b*d*h*j +  (2) *d*e*h*j +  (6) *b*f*h*j +  ((-2)) *c*f*h*j +  (6) *b*c*i*j +  ((-6)) *a*d*i*j +  (4) *d^2*i*j +  ((-2)) *b*e*i*j +  (6) *a*f*i*j +  ((-4)) *f^2*i*j +  (2) *d*h*i*j +  ((-2)) *f*h*i*j +  ((-8)) *c*i^2*j +  (4) *e*i^2*j +  ((-4)) *b*c*j^2 +  (2) *a*d*j^2 +  ((-2)) *d^2*j^2 +  (2) *b*e*j^2 +  ((-2)) *a*f*j^2 +  (2) *f^2*j^2 +  (4) *c*i*j^2 +  ((-2)) *e*i*j^2 +  ((-4)) *b^2*d*k +  (2) *a*d^2*k +  (2) *b*d*e*k +  (4) *b^2*f*k +  ((-4)) *b*c*f*k +  ((-6)) *d^2*f*k +  ((-2)) *b*e*f*k +  (2) *c*e*f*k +  ((-2)) *a*f^2*k +  (6) *d*f^2*k +  ((-2)) *a*d*h*k +  (2) *a*f*h*k +  (4) *a*c*i*k +  ((-4)) *a*e*i*k +  ((-2)) *a*c*j*k +  (2) *b*d*j*k +  (2) *a*e*j*k +  ((-2)) *b*f*j*k +  (2) *c*h*j*k +  ((-2)) *e*h*j*k +  (2) *a*b*c*l +  (2) *a^2*d*l +  ((-2)) *b*c*d*l +  ((-2)) *a*d^2*l +  ((-2)) *a*b*e*l +  ((-2)) *a^2*f*l +  (2) *d^2*f*l +  (2) *b*e*f*l +  ((-2)) *c*e*f*l +  (2) *a*f^2*l +  ((-2)) *d*f^2*l +  (2) *b*c*h*l +  ((-2)) *a*d*h*l +  ((-2)) *b*e*h*l +  (2) *a*f*h*l +  ((-2)) *a*c*i*l +  (6) *b*d*i*l +  (2) *c*d*i*l +  (2) *a*e*i*l +  ((-4)) *d*e*i*l +  ((-6)) *b*f*i*l +  (6) *c*f*i*l +  ((-2)) *c*h*i*l +  (2) *e*h*i*l +  ((-4)) *d*i*j*l +  (4) *f*i*j*l +  (2) *d*j^2*l +  ((-2)) *f*j^2*l +  (6) *b*c*k*l +  ((-2)) *a*d*k*l +  (4) *d^2*k*l +  ((-2)) *b*e*k*l +  ((-2)) *c*e*k*l +  (2) *a*f*k*l +  ((-4)) *f^2*k*l +  (2) *d*h*k*l +  ((-2)) *f*h*k*l +  ((-4)) *c*i*k*l +  (4) *e*i*k*l +  ((-4)) *b*c*l^2 +  (2) *a*d*l^2 +  ((-2)) *d^2*l^2 +  (2) *b*e*l^2 +  (2) *c*e*l^2 +  ((-2)) *a*f*l^2 +  (2) *f^2*l^2 +  ((-2)) *e*i*l^2 +  ((-4)) *d*k*l^2 +  (4) *f*k*l^2 +  (2) *d*l^3 +  ((-2)) *f*l^3 ;  ((-1)) *a^2*d*g +  ((-1)) *b^2*d*g +  (2) *b*d*e*g +  (1) *a^2*f*g +  ((-1)) *b^2*f*g +  (2) *a*d*f*g +  ((-2)) *a*f^2*g +  ((-2)) *a^2*b*h +  ((-2)) *b^3*h +  (1) *a^2*c*h +  (1) *b^2*c*h +  ((-1)) *a^2*e*h +  (3) *b^2*e*h +  ((-2)) *b*c*e*h +  (2) *a*b*f*h +  ((-2)) *a*c*f*h +  (2) *b*f^2*h +  ((-2)) *d*e*g*i +  (2) *b*f*g*i +  (2) *a^2*h*i +  (2) *b^2*h*i +  ((-4)) *b*e*h*i +  (2) *c*e*h*i +  ((-2)) *a*f*h*i +  (1) *a^2*d*j +  (1) *b^2*d*j +  ((-2)) *b*d*e*j +  ((-1)) *a^2*f*j +  (1) *b^2*f*j +  ((-2)) *a*d*f*j +  (2) *a*f^2*j +  (2) *a*f*h*j +  ((-2)) *f^2*h*j +  (2) *d*e*i*j +  ((-2)) *b*f*i*j +  (2) *d*g*i*j +  ((-2)) *f*g*i*j +  ((-2)) *c*h*i*j +  (2) *e*h*i*j +  ((-1)) *d*g*j^2 +  (1) *f*g*j^2 +  (1) *c*h*j^2 +  ((-1)) *e*h*j^2 +  ((-2)) *d*i*j^2 +  (2) *f*i*j^2 +  (1) *d*j^3 +  ((-1)) *f*j^3 +  ((-2)) *d*f*g*k +  (2) *c*f*h*k +  (2) *d*f*j*k +  ((-2)) *f*h*j*k +  (2) *a^2*b*l +  (2) *b^3*l +  ((-1)) *a^2*c*l +  ((-1)) *b^2*c*l +  (1) *a^2*e*l +  ((-3)) *b^2*e*l +  (2) *b*c*e*l +  ((-2)) *a*b*f*l +  (2) *a*c*f*l +  ((-2)) *b*f^2*l +  (2) *f^2*g*l +  ((-2)) *b*f*h*l +  ((-2)) *a^2*i*l +  ((-2)) *b^2*i*l +  (4) *b*e*i*l +  ((-2)) *c*e*i*l +  (2) *a*f*i*l +  ((-2)) *a*f*j*l +  (2) *f*h*j*l +  (2) *c*i*j*l +  ((-2)) *e*i*j*l +  ((-1)) *c*j^2*l +  (1) *e*j^2*l +  ((-2)) *c*f*k*l +  (2) *d*g*k*l +  ((-2)) *c*h*k*l +  (2) *e*h*k*l +  ((-2)) *d*j*k*l +  (2) *f*j*k*l +  (2) *b*f*l^2 +  ((-1)) *d*g*l^2 +  ((-1)) *f*g*l^2 +  (1) *c*h*l^2 +  ((-1)) *e*h*l^2 +  (1) *d*j*l^2 +  ((-1)) *f*j*l^2 +  (2) *c*k*l^2 +  ((-2)) *e*k*l^2 +  ((-1)) *c*l^3 +  (1) *e*l^3 ;  ((-2)) *a*b^2*g +  (2) *a*b*c*g +  ((-1)) *a^2*d*g +  (1) *b^2*d*g +  ((-1)) *c^2*d*g +  (2) *a*d^2*g +  ((-1)) *d^3*g +  (1) *a^2*f*g +  (1) *b^2*f*g +  ((-2)) *b*c*f*g +  (1) *c^2*f*g +  ((-2)) *a*d*f*g +  (1) *d^2*f*g +  (2) *b^3*h +  ((-1)) *a^2*c*h +  ((-3)) *b^2*c*h +  (1) *c^3*h +  (2) *a*b*d*h +  ((-2)) *b*d^2*h +  (1) *c*d^2*h +  ((-1)) *a^2*e*h +  ((-1)) *b^2*e*h +  (2) *b*c*e*h +  ((-1)) *c^2*e*h +  (2) *a*d*e*h +  ((-1)) *d^2*e*h +  (2) *a*b*g*i +  ((-2)) *a*c*g*i +  ((-2)) *b*d*g*i +  (2) *c*d*g*i +  ((-2)) *b^2*h*i +  (4) *b*c*h*i +  ((-2)) *c^2*h*i +  (2) *a*b^2*j +  ((-2)) *a*b*c*j +  (1) *a^2*d*j +  ((-1)) *b^2*d*j +  (1) *c^2*d*j +  ((-2)) *a*d^2*j +  (1) *d^3*j +  ((-1)) *a^2*f*j +  ((-1)) *b^2*f*j +  (2) *b*c*f*j +  ((-1)) *c^2*f*j +  (2) *a*d*f*j +  ((-1)) *d^2*f*j +  (2) *a^2*h*j +  ((-4)) *a*d*h*j +  (2) *d^2*h*j +  ((-2)) *a*b*i*j +  (2) *a*c*i*j +  (2) *b*d*i*j +  ((-2)) *c*d*i*j +  ((-2)) *a*d*g*k +  (2) *d^2*g*k +  (2) *a*c*h*k +  ((-2)) *c*d*h*k +  (2) *a*d*j*k +  ((-2)) *d^2*j*k +  ((-2)) *a*h*j*k +  (2) *d*h*j*k +  ((-2)) *b^3*l +  (1) *a^2*c*l +  (3) *b^2*c*l +  ((-1)) *c^3*l +  ((-2)) *a*b*d*l +  (2) *b*d^2*l +  ((-1)) *c*d^2*l +  (1) *a^2*e*l +  (1) *b^2*e*l +  ((-2)) *b*c*e*l +  (1) *c^2*e*l +  ((-2)) *a*d*e*l +  (1) *d^2*e*l +  (2) *a*d*g*l +  ((-2)) *d^2*g*l +  ((-2)) *a*b*h*l +  (2) *b*d*h*l +  (2) *b^2*i*l +  ((-4)) *b*c*i*l +  (2) *c^2*i*l +  ((-2)) *a^2*j*l +  (2) *a*d*j*l +  (2) *a*h*j*l +  ((-2)) *d*h*j*l +  ((-2)) *a*c*k*l +  (2) *c*d*k*l +  (2) *a*g*k*l +  ((-2)) *d*g*k*l +  (2) *a*b*l^2 +  ((-2)) *b*d*l^2 +  ((-2)) *a*g*l^2 +  (2) *d*g*l^2 ;  ((-2)) *a^2*b*d +  ((-2)) *b^3*d +  (2) *a^2*b*f +  (2) *b^3*f +  (1) *a^2*d*g +  (1) *b^2*d*g +  ((-1)) *a^2*f*g +  ((-1)) *b^2*f*g +  ((-1)) *a^2*c*h +  ((-1)) *b^2*c*h +  (1) *a^2*e*h +  (1) *b^2*e*h +  (2) *a^2*d*i +  (2) *b^2*d*i +  ((-2)) *a^2*f*i +  ((-2)) *b^2*f*i +  ((-1)) *a^2*d*j +  (3) *b^2*d*j +  (1) *a^2*f*j +  ((-3)) *b^2*f*j +  ((-2)) *b*d*g*j +  (2) *b*f*g*j +  (2) *b*c*h*j +  ((-2)) *b*e*h*j +  ((-4)) *b*d*i*j +  (4) *b*f*i*j +  (1) *d*g*j^2 +  ((-1)) *f*g*j^2 +  ((-1)) *c*h*j^2 +  (1) *e*h*j^2 +  (2) *d*i*j^2 +  ((-2)) *f*i*j^2 +  ((-1)) *d*j^3 +  (1) *f*j^3 +  (1) *a^2*c*l +  ((-1)) *b^2*c*l +  (2) *a*b*d*l +  ((-1)) *a^2*e*l +  (1) *b^2*e*l +  (2) *a*d*e*l +  ((-2)) *a*b*f*l +  ((-2)) *a*c*f*l +  ((-2)) *a*d*g*l +  (2) *a*f*g*l +  (2) *a*c*h*l +  ((-2)) *a*e*h*l +  (2) *b*c*i*l +  ((-2)) *a*d*i*l +  ((-2)) *b*e*i*l +  (2) *a*f*i*l +  ((-2)) *c*i*j*l +  (2) *e*i*j*l +  (1) *c*j^2*l +  ((-1)) *e*j^2*l +  (2) *a*c*k*l +  ((-2)) *b*d*k*l +  ((-2)) *a*e*k*l +  (2) *b*f*k*l +  (2) *d*j*k*l +  ((-2)) *f*j*k*l +  ((-2)) *a*c*l^2 +  (2) *b*d*l^2 +  (2) *a*e*l^2 +  ((-2)) *d*e*l^2 +  ((-2)) *b*f*l^2 +  (2) *c*f*l^2 +  (1) *d*g*l^2 +  ((-1)) *f*g*l^2 +  ((-1)) *c*h*l^2 +  (1) *e*h*l^2 +  ((-1)) *d*j*l^2 +  (1) *f*j*l^2 +  ((-2)) *c*k*l^2 +  (2) *e*k*l^2 +  (1) *c*l^3 +  ((-1)) *e*l^3 ; ];

[
 (1) *c ; 0; 0; 0; 0;  (1) *a*h^2 ; 0; 0; 0; 0; ];

[
0; 0; 0;  (1) *a ; 0;  (1) *b*h ; 0; 0; 0; ];

[
0;  (1) *a ; 0;  (1) *b*d ; 0; 0; 0; 0; ];

[
0; 0;  ((-1)) *g ;  (1) *c ; 0; 0; 0; ];

[
0;  (1) *c ; 0;  (1) *a ; 0; 0; ];

[
0;  (1) *g ; 0; 0;  (1) *a ; ];

];

c:=
1;