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;