Altitudes
Geogebra sheet
Coq statement
Lemma altitudes: forall A B C A1 B1 C1 H:point,
collinear B C A1 -> orthogonal A A1 B C ->
collinear A C B1 -> orthogonal B B1 A C ->
collinear A B C1 -> orthogonal C C1 A B ->
collinear A A1 H -> collinear B B1 H ->
collinear C C1 H
\/ equal2 A B
\/ collinear A B C.
Proof. geo_begin. tzR. tzR. Qed.
Algebraic version
First goal
p:= (1) *b*c*h^2*j + ((-1)) *a*d*h^2*j + ((-1)) *b*c*h^2*k + (1) *a*d*h^2*k + (1) *a*h^2*j*k + ((-1)) *c*h^2*j*k + ((-1)) *a*h^2*k^2 + (1) *c*h^2*k^2 + (1) *b*c*g*h*m + ((-1)) *a*d*g*h*m + ((-1)) *b*c*h*j*m + (1) *a*d*h*j*m + ((-1)) *b*h^2*j*m + (1) *d*h^2*j*m + (1) *a*g*h*k*m + ((-1)) *c*g*h*k*m + (1) *b*h^2*k*m + ((-1)) *d*h^2*k*m + ((-1)) *a*h*j*k*m + (1) *c*h*j*k*m + ((-1)) *b*g*h*m^2 + (1) *d*g*h*m^2 + (1) *b*h*j*m^2 + ((-1)) *d*h*j*m^2 + ((-1)) *b*c*g*h*n + (1) *a*d*g*h*n + ((-1)) *b*c*h*j*n + (1) *a*d*h*j*n + (2) *b*c*h*k*n + ((-2)) *a*d*h*k*n + ((-1)) *a*g*h*k*n + (1) *c*g*h*k*n + ((-1)) *a*h*j*k*n + (1) *c*h*j*k*n + (2) *a*h*k^2*n + ((-2)) *c*h*k^2*n + ((-1)) *b*c*g*m*n + (1) *a*d*g*m*n + (1) *b*g*h*m*n + ((-1)) *d*g*h*m*n + (1) *b*c*j*m*n + ((-1)) *a*d*j*m*n + (1) *b*h*j*m*n + ((-1)) *d*h*j*m*n + ((-1)) *a*g*k*m*n + (1) *c*g*k*m*n + ((-2)) *b*h*k*m*n + (2) *d*h*k*m*n + (1) *a*j*k*m*n + ((-1)) *c*j*k*m*n + (1) *b*g*m^2*n + ((-1)) *d*g*m^2*n + ((-1)) *b*j*m^2*n + (1) *d*j*m^2*n + (1) *b*c*g*n^2 + ((-1)) *a*d*g*n^2 + ((-1)) *b*c*k*n^2 + (1) *a*d*k*n^2 + (1) *a*g*k*n^2 + ((-1)) *c*g*k*n^2 + ((-1)) *a*k^2*n^2 + (1) *c*k^2*n^2 + ((-1)) *b*g*m*n^2 + (1) *d*g*m*n^2 + (1) *b*k*m*n^2 + ((-1)) *d*k*m*n^2
F:= [
((-1)) *i*j + (1) *i*k + (1) *j*m + ((-1)) *l*m + ((-1)) *k*n + (1) *l*n ;
(1) *g*j + ((-1)) *g*k + ((-1)) *j*l + (1) *k*l + ((-1)) *h*m + (1) *i*m + (1) *h*n + ((-1)) *i*n ;
((-1)) *e*g + (1) *f*h + (1) *e*k + ((-1)) *h*k + ((-1)) *f*m + (1) *g*m ;
((-1)) *f*g + ((-1)) *e*h + (1) *g*j + (1) *f*k + ((-1)) *j*k + (1) *e*m + (1) *h*n + ((-1)) *m*n ;
((-1)) *c*g + (1) *d*h + (1) *c*j + ((-1)) *h*j + ((-1)) *d*n + (1) *g*n ;
((-1)) *d*g + ((-1)) *c*h + (1) *d*j + (1) *g*k + ((-1)) *j*k + (1) *h*m + (1) *c*n + ((-1)) *m*n ;
((-1)) *a*g + (1) *b*h + ((-1)) *b*i + (1) *g*i + (1) *a*l + ((-1)) *h*l ;
((-1)) *b*e + (1) *a*f + ((-1)) *a*j + (1) *e*j + (1) *b*n + ((-1)) *f*n ;
];
Second goal
p:= (1) *b*c*g*h*j + ((-1)) *a*d*g*h*j + ((-1)) *b*c*h*j^2 + (1) *a*d*h*j^2 + ((-1)) *b*c*g*h*k + (1) *a*d*g*h*k + (1) *b*c*h*j*k + ((-1)) *a*d*h*j*k + (1) *a*g*h*j*k + ((-1)) *c*g*h*j*k + ((-1)) *a*h*j^2*k + (1) *c*h*j^2*k + ((-1)) *a*g*h*k^2 + (1) *c*g*h*k^2 + (1) *a*h*j*k^2 + ((-1)) *c*h*j*k^2 + (1) *b*c*g^2*m + ((-1)) *a*d*g^2*m + ((-2)) *b*c*g*j*m + (2) *a*d*g*j*m + ((-1)) *b*g*h*j*m + (1) *d*g*h*j*m + (1) *b*c*j^2*m + ((-1)) *a*d*j^2*m + (1) *b*h*j^2*m + ((-1)) *d*h*j^2*m + (1) *a*g^2*k*m + ((-1)) *c*g^2*k*m + (1) *b*g*h*k*m + ((-1)) *d*g*h*k*m + ((-2)) *a*g*j*k*m + (2) *c*g*j*k*m + ((-1)) *b*h*j*k*m + (1) *d*h*j*k*m + (1) *a*j^2*k*m + ((-1)) *c*j^2*k*m + ((-1)) *b*g^2*m^2 + (1) *d*g^2*m^2 + (2) *b*g*j*m^2 + ((-2)) *d*g*j*m^2 + ((-1)) *b*j^2*m^2 + (1) *d*j^2*m^2 + ((-1)) *b*c*g^2*n + (1) *a*d*g^2*n + (1) *b*c*g*j*n + ((-1)) *a*d*g*j*n + (1) *b*c*g*k*n + ((-1)) *a*d*g*k*n + ((-1)) *a*g^2*k*n + (1) *c*g^2*k*n + ((-1)) *b*c*j*k*n + (1) *a*d*j*k*n + (1) *a*g*j*k*n + ((-1)) *c*g*j*k*n + (1) *a*g*k^2*n + ((-1)) *c*g*k^2*n + ((-1)) *a*j*k^2*n + (1) *c*j*k^2*n + (1) *b*g^2*m*n + ((-1)) *d*g^2*m*n + ((-1)) *b*g*j*m*n + (1) *d*g*j*m*n + ((-1)) *b*g*k*m*n + (1) *d*g*k*m*n + (1) *b*j*k*m*n + ((-1)) *d*j*k*m*n
F:= [
((-1)) *i*j + (1) *i*k + (1) *j*m + ((-1)) *l*m + ((-1)) *k*n + (1) *l*n ;
(1) *g*j + ((-1)) *g*k + ((-1)) *j*l + (1) *k*l + ((-1)) *h*m + (1) *i*m + (1) *h*n + ((-1)) *i*n ;
((-1)) *e*g + (1) *f*h + (1) *e*k + ((-1)) *h*k + ((-1)) *f*m + (1) *g*m ;
((-1)) *f*g + ((-1)) *e*h + (1) *g*j + (1) *f*k + ((-1)) *j*k + (1) *e*m + (1) *h*n + ((-1)) *m*n ;
((-1)) *c*g + (1) *d*h + (1) *c*j + ((-1)) *h*j + ((-1)) *d*n + (1) *g*n ;
((-1)) *d*g + ((-1)) *c*h + (1) *d*j + (1) *g*k + ((-1)) *j*k + (1) *h*m + (1) *c*n + ((-1)) *m*n ;
((-1)) *a*g + (1) *b*h + ((-1)) *b*i + (1) *g*i + (1) *a*l + ((-1)) *h*l ;
((-1)) *b*e + (1) *a*f + ((-1)) *a*j + (1) *e*j + (1) *b*n + ((-1)) *f*n ;
];
Certificates
First certificate
CR:=[
((-3)) ; (2) ; ((-1)) ; ((-2)) ; (2) ; ((-1)) *m ; 0; 0; (2) *a + ((-1)) *i + (4) *m + ((-8)) *n ; (6) *n ; (6) *n ; (3) *k + ((-2)) *l ; ((-1)) *m ; ((-2)) *j + (1) *k ; ((-2)) *d + (2) *k + (1) *l ; ((-1)) *k + (1) *l ; ((-1)) *m + ((-2)) *n ; 0; (2) *j + ((-4)) *k + ((-2)) *l ; ((-2)) *k^2 + ((-2)) *k*l + (1) *h*m + ((-2)) *m^2 + (4) *a*n + (4) *m*n ; ((-1)) *h*k + ((-1)) *f*m + ((-4)) *b*n + (14) *f*n + ((-4)) *k*n ; (2) *i*m + ((-8)) *c*n + ((-2)) *h*n + ((-2)) *i*n ; ((-2)) *a*k + (3) *a*l + ((-1)) *k*m + (2) *l*m + (6) *j*n + ((-4)) *k*n + ((-2)) *l*n ; (2) *j*k + (1) *k^2 + ((-2)) *j*l + ((-3)) *k*l + (2) *l^2 + ((-1)) *a*m + ((-4)) *a*n + (8) *m*n + ((-6)) *n^2 ; (1) *k^2 + ((-1)) *k*l + (4) *a*n + ((-2)) *h*n + ((-4)) *i*n + ((-6)) *n^2 ; ((-1)) *c*k + (1) *h*k + ((-2)) *k*m + (4) *d*n + ((-4)) *k*n ; (1) *k^2 + ((-1)) *k*l + (1) *h*m + ((-4)) *a*n + ((-6)) *n^2 ; ((-1)) *a*k + (1) *h*k + (1) *a*l + ((-1)) *h*l + ((-1)) *k*m + (4) *l*m ; ((-2)) *k*l + ((-1)) *h*m + (2) *m*n ; ((-2)) *b*h + ((-2)) *a*j + ((-2)) *a*k + (2) *h*k + (4) *a*l + ((-2)) *h*l + (3) *b*m + ((-2)) *l*m + (2) *b*n + ((-2)) *k*n + (2) *l*n ; ((-2)) *a*h + (2) *b*j + ((-4)) *b*k + ((-1)) *j*k + ((-1)) *k^2 + ((-2)) *b*l + (1) *j*l + (3) *k*l + ((-2)) *l^2 + (1) *a*m + (1) *h*m + (2) *m^2 + ((-6)) *a*n ; (2) *h*j + (1) *c*k + ((-1)) *h*k + (1) *c*l + ((-2)) *h*l + (2) *l*m + ((-10)) *d*n + (2) *k*n + (2) *l*n ; ((-1)) *d*k + (2) *k^2 + (3) *d*l + ((-4)) *k*l + ((-1)) *a*m + ((-1)) *c*m + (1) *h*m ; ((-2)) *a*c + ((-2)) *b*d + ((-1)) *c*e + (1) *d*f + (1) *c*h + (1) *e*h + (7) *b*k + ((-1)) *d*k + (1) *f*k + ((-5)) *g*k + (2) *k^2 + (2) *e*m + ((-4)) *h*m + ((-2)) *h*n + (2) *m*n ; ((-1)) *c*h*k + ((-2)) *d*k^2 + (1) *j*k^2 + (2) *k^3 + (1) *a*c*l + ((-1)) *c*h*l + ((-1)) *c*j*m + ((-2)) *h*k*m + ((-4)) *i*k*m + ((-2)) *a*l*m + ((-4)) *c*l*m + (10) *h*l*m + ((-2)) *d*m^2 + (2) *k*m^2 + ((-6)) *b*c*n + (4) *a*d*n + (4) *d*i*n + ((-6)) *h*j*n + ((-6)) *c*k*n + (6) *h*k*n + ((-2)) *i*k*n + (8) *c*l*n + ((-4)) *h*l*n + (6) *b*m*n + (2) *d*m*n + (2) *k*m*n + ((-4)) *l*m*n + ((-6)) *d*n^2 ; ((-2)) *g*k^2 + (2) *k^3 + ((-2)) *g*k*l + (3) *h*k*m + ((-7)) *i*k*m + (2) *k*m^2 + ((-4)) *a*g*n + (2) *h*k*n + (4) *i*k*n + (2) *b*m*n + ((-4)) *g*m*n + ((-2)) *k*m*n + ((-2)) *g*n^2 + (2) *k*n^2 ; (1) *a*g*k + ((-2)) *b*h*k + ((-2)) *a*k^2 + (2) *h*k^2 + (1) *a*k*l + ((-4)) *h*k*l + (2) *a*l^2 + ((-2)) *h*l^2 + ((-1)) *a*h*m + (1) *h*i*m + ((-1)) *i^2*m + (4) *k*l*m + ((-4)) *l^2*m + ((-2)) *a*m^2 + ((-2)) *h*m^2 + (2) *i*m^2 + (4) *a^2*n + (6) *b^2*n + (2) *a*h*n + (10) *a*i*n + (4) *b*k*n + ((-6)) *g*k*n + (4) *k^2*n + ((-4)) *b*l*n + (2) *l^2*n + ((-8)) *a*m*n + ((-2)) *h*m*n + (2) *i*m*n + ((-8)) *i*n^2 + (8) *m*n^2 ; ((-2)) *a*h*k + (1) *a^2*l + ((-1)) *a*h*l + ((-1)) *a*g*m + (1) *b*h*m + (1) *b*i*m + ((-1)) *h*k*m + (1) *i*k*m + ((-4)) *a*l*m + ((-2)) *h*l*m + (2) *i*l*m + (2) *l*m^2 + (2) *b*h*n + ((-2)) *b*i*n + ((-20)) *a*k*n + ((-2)) *h*k*n + (8) *i*k*n + (18) *a*l*n + ((-2)) *h*l*n + ((-4)) *i*l*n + (6) *g*m*n + (2) *k*m*n + ((-2)) *l*m*n + ((-6)) *b*n^2 + (4) *k*n^2 + ((-4)) *l*n^2 ; ((-1)) *a*g*k + (1) *d*h*k + ((-1)) *a*k^2 + ((-1)) *c*k^2 + (2) *a*k*l + (2) *c*k*l + ((-2)) *h*k*l + (1) *a*c*m + ((-1)) *a*h*m + ((-1)) *c*i*m + (2) *i^2*m + (4) *b*k*m + ((-1)) *d*k*m + ((-2)) *b*l*m + (4) *d*l*m + ((-2)) *k*l*m + (2) *l^2*m + (4) *a^2*n + ((-8)) *a*c*n + ((-4)) *b*d*n + ((-2)) *b*g*n + (10) *a*h*n + ((-4)) *c*h*n + ((-16)) *a*i*n + (4) *c*i*n + ((-2)) *h*i*n + (2) *i^2*n + ((-2)) *b*k*n + ((-4)) *d*k*n + (6) *g*k*n + ((-4)) *k^2*n + (2) *b*l*n + (2) *k*l*n + (12) *a*m*n + ((-8)) *c*m*n + (8) *h*m*n + ((-6)) *a*n^2 + (14) *c*n^2 + ((-4)) *h*n^2 + (4) *i*n^2 + ((-8)) *m*n^2 ; (1) *c*h*k + (1) *a*i*k + ((-1)) *c*i*k + ((-1)) *b*k^2 + (1) *b*k*l + (2) *d*k*l + ((-2)) *k*l^2 + (1) *a*d*m + (3) *a*k*m + (4) *c*l*m + ((-4)) *a*b*n + ((-2)) *b*c*n + ((-10)) *a*d*n + (10) *a*g*n + (2) *b*h*n + (4) *d*i*n + (8) *a*k*n + (2) *c*k*n + (2) *h*k*n + ((-6)) *i*k*n + ((-8)) *a*l*n + ((-4)) *c*l*n + ((-2)) *h*l*n + (2) *i*l*n + ((-6)) *d*m*n + (2) *k*m*n + ((-2)) *l*m*n + (6) *b*n^2 + (6) *d*n^2 + ((-6)) *g*n^2 + ((-6)) *k*n^2 + (6) *l*n^2 ; ((-1)) *c*j^2 + (1) *h*j^2 + ((-4)) *a*d*k + ((-1)) *b*e*k + ((-1)) *a*f*k + (1) *c*f*k + ((-2)) *a*g*k + (1) *e*g*k + (1) *b*h*k + ((-1)) *f*h*k + (2) *a*j*k + ((-2)) *c*j*k + ((-2)) *a*k^2 + ((-1)) *c*k^2 + (2) *e*k^2 + (2) *h*k^2 + (4) *a*d*l + (1) *a*f*l + ((-2)) *d*h*l + ((-1)) *f*h*l + ((-1)) *a*j*l + (3) *c*j*l + (1) *e*j*l + ((-2)) *h*j*l + ((-2)) *a*k*l + (3) *c*k*l + ((-2)) *e*k*l + ((-2)) *h*k*l + ((-2)) *c*l^2 + ((-1)) *c*e*m + ((-1)) *b*f*m + (1) *d*f*m + ((-1)) *b*g*m + ((-6)) *a*h*m + (2) *e*h*m + ((-1)) *b*j*m + (2) *d*j*m + (1) *g*j*m + (2) *b*k*m + (2) *f*k*m + ((-6)) *d*l*m + (2) *f*l*m + (2) *g*l*m + (2) *k*l*m + (2) *c*m^2 + ((-2)) *h*m^2 + (2) *a*c*n + (4) *b*d*n + (8) *c*e*n + ((-6)) *d*f*n + (2) *f*g*n + ((-12)) *a*h*n + (4) *c*h*n + (2) *e*h*n + ((-4)) *d*j*n + ((-6)) *d*k*n + (4) *f*k*n + ((-4)) *g*k*n + (4) *j*k*n + (2) *k^2*n + (6) *d*l*n + (2) *f*l*n + ((-2)) *g*l*n + ((-2)) *k*l*n + (4) *a*m*n + ((-2)) *c*m*n + ((-4)) *e*m*n + ((-4)) *h*m*n + (2) *m^2*n + ((-8)) *c*n^2 + (4) *h*n^2 + (4) *m*n^2 ; (2) *b*g*j + ((-2)) *g^2*j + (2) *b*d*k + ((-1)) *a*e*k + (1) *c*e*k + (1) *b*f*k + (2) *b*g*k + ((-2)) *d*g*k + ((-1)) *f*g*k + ((-2)) *g^2*k + (1) *a*h*k + ((-1)) *c*h*k + ((-3)) *b*j*k + (3) *g*j*k + (2) *b*k^2 + ((-2)) *g*k^2 + (1) *b*c*m + ((-2)) *a*d*m + (1) *b*e*m + (3) *d*e*m + (2) *c*f*m + ((-3)) *a*g*m + ((-2)) *c*g*m + (2) *e*g*m + (2) *d*h*m + ((-2)) *f*h*m + ((-3)) *g*h*m + ((-1)) *d*i*m + (2) *g*i*m + ((-1)) *c*j*m + (1) *h*j*m + (2) *a*k*m + ((-6)) *e*k*m + (2) *h*k*m + (2) *i*k*m + ((-2)) *b*c*n + (18) *a*d*n + ((-6)) *d*e*n + (2) *c*f*n + ((-16)) *a*g*n + (2) *c*g*n + (4) *e*g*n + (2) *b*h*n + ((-4)) *d*h*n + ((-2)) *f*h*n + (2) *g*i*n + ((-2)) *c*j*n + (2) *h*j*n + ((-2)) *a*k*n + (6) *c*k*n + (2) *e*k*n + ((-4)) *h*k*n + ((-2)) *i*k*n + ((-2)) *c*l*n + (2) *h*l*n + (2) *b*m*n + ((-4)) *d*m*n + (2) *g*m*n + ((-4)) *d*n^2 + (4) *g*n^2 ; ];
C:=[
[
((-3)) ; (2) ; ((-1)) ; ((-2)) ; (2) ; ((-1)) *m ; 0; 0; (2) *a + ((-1)) *i + (4) *m + ((-8)) *n ; (6) *n ; (6) *n ; (3) *k + ((-2)) *l ; ((-1)) *m ; ((-2)) *j + (1) *k ; ((-2)) *d + (2) *k + (1) *l ; ((-1)) *k + (1) *l ; ((-1)) *m + ((-2)) *n ; 0; (2) *j + ((-4)) *k + ((-2)) *l ; ((-2)) *k^2 + ((-2)) *k*l + (1) *h*m + ((-2)) *m^2 + (4) *a*n + (4) *m*n ; ((-1)) *h*k + ((-1)) *f*m + ((-4)) *b*n + (14) *f*n + ((-4)) *k*n ; (2) *i*m + ((-8)) *c*n + ((-2)) *h*n + ((-2)) *i*n ; ((-2)) *a*k + (3) *a*l + ((-1)) *k*m + (2) *l*m + (6) *j*n + ((-4)) *k*n + ((-2)) *l*n ; (2) *j*k + (1) *k^2 + ((-2)) *j*l + ((-3)) *k*l + (2) *l^2 + ((-1)) *a*m + ((-4)) *a*n + (8) *m*n + ((-6)) *n^2 ; (1) *k^2 + ((-1)) *k*l + (4) *a*n + ((-2)) *h*n + ((-4)) *i*n + ((-6)) *n^2 ; ((-1)) *c*k + (1) *h*k + ((-2)) *k*m + (4) *d*n + ((-4)) *k*n ; (1) *k^2 + ((-1)) *k*l + (1) *h*m + ((-4)) *a*n + ((-6)) *n^2 ; ((-1)) *a*k + (1) *h*k + (1) *a*l + ((-1)) *h*l + ((-1)) *k*m + (4) *l*m ; ((-2)) *k*l + ((-1)) *h*m + (2) *m*n ; ((-2)) *b*h + ((-2)) *a*j + ((-2)) *a*k + (2) *h*k + (4) *a*l + ((-2)) *h*l + (3) *b*m + ((-2)) *l*m + (2) *b*n + ((-2)) *k*n + (2) *l*n ; ((-2)) *a*h + (2) *b*j + ((-4)) *b*k + ((-1)) *j*k + ((-1)) *k^2 + ((-2)) *b*l + (1) *j*l + (3) *k*l + ((-2)) *l^2 + (1) *a*m + (1) *h*m + (2) *m^2 + ((-6)) *a*n ; (2) *h*j + (1) *c*k + ((-1)) *h*k + (1) *c*l + ((-2)) *h*l + (2) *l*m + ((-10)) *d*n + (2) *k*n + (2) *l*n ; ((-1)) *d*k + (2) *k^2 + (3) *d*l + ((-4)) *k*l + ((-1)) *a*m + ((-1)) *c*m + (1) *h*m ; ((-2)) *a*c + ((-2)) *b*d + ((-1)) *c*e + (1) *d*f + (1) *c*h + (1) *e*h + (7) *b*k + ((-1)) *d*k + (1) *f*k + ((-5)) *g*k + (2) *k^2 + (2) *e*m + ((-4)) *h*m + ((-2)) *h*n + (2) *m*n ; ((-1)) *c*h*k + ((-2)) *d*k^2 + (1) *j*k^2 + (2) *k^3 + (1) *a*c*l + ((-1)) *c*h*l + ((-1)) *c*j*m + ((-2)) *h*k*m + ((-4)) *i*k*m + ((-2)) *a*l*m + ((-4)) *c*l*m + (10) *h*l*m + ((-2)) *d*m^2 + (2) *k*m^2 + ((-6)) *b*c*n + (4) *a*d*n + (4) *d*i*n + ((-6)) *h*j*n + ((-6)) *c*k*n + (6) *h*k*n + ((-2)) *i*k*n + (8) *c*l*n + ((-4)) *h*l*n + (6) *b*m*n + (2) *d*m*n + (2) *k*m*n + ((-4)) *l*m*n + ((-6)) *d*n^2 ; ((-2)) *g*k^2 + (2) *k^3 + ((-2)) *g*k*l + (3) *h*k*m + ((-7)) *i*k*m + (2) *k*m^2 + ((-4)) *a*g*n + (2) *h*k*n + (4) *i*k*n + (2) *b*m*n + ((-4)) *g*m*n + ((-2)) *k*m*n + ((-2)) *g*n^2 + (2) *k*n^2 ; (1) *a*g*k + ((-2)) *b*h*k + ((-2)) *a*k^2 + (2) *h*k^2 + (1) *a*k*l + ((-4)) *h*k*l + (2) *a*l^2 + ((-2)) *h*l^2 + ((-1)) *a*h*m + (1) *h*i*m + ((-1)) *i^2*m + (4) *k*l*m + ((-4)) *l^2*m + ((-2)) *a*m^2 + ((-2)) *h*m^2 + (2) *i*m^2 + (4) *a^2*n + (6) *b^2*n + (2) *a*h*n + (10) *a*i*n + (4) *b*k*n + ((-6)) *g*k*n + (4) *k^2*n + ((-4)) *b*l*n + (2) *l^2*n + ((-8)) *a*m*n + ((-2)) *h*m*n + (2) *i*m*n + ((-8)) *i*n^2 + (8) *m*n^2 ; ((-2)) *a*h*k + (1) *a^2*l + ((-1)) *a*h*l + ((-1)) *a*g*m + (1) *b*h*m + (1) *b*i*m + ((-1)) *h*k*m + (1) *i*k*m + ((-4)) *a*l*m + ((-2)) *h*l*m + (2) *i*l*m + (2) *l*m^2 + (2) *b*h*n + ((-2)) *b*i*n + ((-20)) *a*k*n + ((-2)) *h*k*n + (8) *i*k*n + (18) *a*l*n + ((-2)) *h*l*n + ((-4)) *i*l*n + (6) *g*m*n + (2) *k*m*n + ((-2)) *l*m*n + ((-6)) *b*n^2 + (4) *k*n^2 + ((-4)) *l*n^2 ; ((-1)) *a*g*k + (1) *d*h*k + ((-1)) *a*k^2 + ((-1)) *c*k^2 + (2) *a*k*l + (2) *c*k*l + ((-2)) *h*k*l + (1) *a*c*m + ((-1)) *a*h*m + ((-1)) *c*i*m + (2) *i^2*m + (4) *b*k*m + ((-1)) *d*k*m + ((-2)) *b*l*m + (4) *d*l*m + ((-2)) *k*l*m + (2) *l^2*m + (4) *a^2*n + ((-8)) *a*c*n + ((-4)) *b*d*n + ((-2)) *b*g*n + (10) *a*h*n + ((-4)) *c*h*n + ((-16)) *a*i*n + (4) *c*i*n + ((-2)) *h*i*n + (2) *i^2*n + ((-2)) *b*k*n + ((-4)) *d*k*n + (6) *g*k*n + ((-4)) *k^2*n + (2) *b*l*n + (2) *k*l*n + (12) *a*m*n + ((-8)) *c*m*n + (8) *h*m*n + ((-6)) *a*n^2 + (14) *c*n^2 + ((-4)) *h*n^2 + (4) *i*n^2 + ((-8)) *m*n^2 ; (1) *c*h*k + (1) *a*i*k + ((-1)) *c*i*k + ((-1)) *b*k^2 + (1) *b*k*l + (2) *d*k*l + ((-2)) *k*l^2 + (1) *a*d*m + (3) *a*k*m + (4) *c*l*m + ((-4)) *a*b*n + ((-2)) *b*c*n + ((-10)) *a*d*n + (10) *a*g*n + (2) *b*h*n + (4) *d*i*n + (8) *a*k*n + (2) *c*k*n + (2) *h*k*n + ((-6)) *i*k*n + ((-8)) *a*l*n + ((-4)) *c*l*n + ((-2)) *h*l*n + (2) *i*l*n + ((-6)) *d*m*n + (2) *k*m*n + ((-2)) *l*m*n + (6) *b*n^2 + (6) *d*n^2 + ((-6)) *g*n^2 + ((-6)) *k*n^2 + (6) *l*n^2 ; ((-1)) *c*j^2 + (1) *h*j^2 + ((-4)) *a*d*k + ((-1)) *b*e*k + ((-1)) *a*f*k + (1) *c*f*k + ((-2)) *a*g*k + (1) *e*g*k + (1) *b*h*k + ((-1)) *f*h*k + (2) *a*j*k + ((-2)) *c*j*k + ((-2)) *a*k^2 + ((-1)) *c*k^2 + (2) *e*k^2 + (2) *h*k^2 + (4) *a*d*l + (1) *a*f*l + ((-2)) *d*h*l + ((-1)) *f*h*l + ((-1)) *a*j*l + (3) *c*j*l + (1) *e*j*l + ((-2)) *h*j*l + ((-2)) *a*k*l + (3) *c*k*l + ((-2)) *e*k*l + ((-2)) *h*k*l + ((-2)) *c*l^2 + ((-1)) *c*e*m + ((-1)) *b*f*m + (1) *d*f*m + ((-1)) *b*g*m + ((-6)) *a*h*m + (2) *e*h*m + ((-1)) *b*j*m + (2) *d*j*m + (1) *g*j*m + (2) *b*k*m + (2) *f*k*m + ((-6)) *d*l*m + (2) *f*l*m + (2) *g*l*m + (2) *k*l*m + (2) *c*m^2 + ((-2)) *h*m^2 + (2) *a*c*n + (4) *b*d*n + (8) *c*e*n + ((-6)) *d*f*n + (2) *f*g*n + ((-12)) *a*h*n + (4) *c*h*n + (2) *e*h*n + ((-4)) *d*j*n + ((-6)) *d*k*n + (4) *f*k*n + ((-4)) *g*k*n + (4) *j*k*n + (2) *k^2*n + (6) *d*l*n + (2) *f*l*n + ((-2)) *g*l*n + ((-2)) *k*l*n + (4) *a*m*n + ((-2)) *c*m*n + ((-4)) *e*m*n + ((-4)) *h*m*n + (2) *m^2*n + ((-8)) *c*n^2 + (4) *h*n^2 + (4) *m*n^2 ; (2) *b*g*j + ((-2)) *g^2*j + (2) *b*d*k + ((-1)) *a*e*k + (1) *c*e*k + (1) *b*f*k + (2) *b*g*k + ((-2)) *d*g*k + ((-1)) *f*g*k + ((-2)) *g^2*k + (1) *a*h*k + ((-1)) *c*h*k + ((-3)) *b*j*k + (3) *g*j*k + (2) *b*k^2 + ((-2)) *g*k^2 + (1) *b*c*m + ((-2)) *a*d*m + (1) *b*e*m + (3) *d*e*m + (2) *c*f*m + ((-3)) *a*g*m + ((-2)) *c*g*m + (2) *e*g*m + (2) *d*h*m + ((-2)) *f*h*m + ((-3)) *g*h*m + ((-1)) *d*i*m + (2) *g*i*m + ((-1)) *c*j*m + (1) *h*j*m + (2) *a*k*m + ((-6)) *e*k*m + (2) *h*k*m + (2) *i*k*m + ((-2)) *b*c*n + (18) *a*d*n + ((-6)) *d*e*n + (2) *c*f*n + ((-16)) *a*g*n + (2) *c*g*n + (4) *e*g*n + (2) *b*h*n + ((-4)) *d*h*n + ((-2)) *f*h*n + (2) *g*i*n + ((-2)) *c*j*n + (2) *h*j*n + ((-2)) *a*k*n + (6) *c*k*n + (2) *e*k*n + ((-4)) *h*k*n + ((-2)) *i*k*n + ((-2)) *c*l*n + (2) *h*l*n + (2) *b*m*n + ((-4)) *d*m*n + (2) *g*m*n + ((-4)) *d*n^2 + (4) *g*n^2 ; ];
[
0; (1) ; (2) ; 0; ((-1)) *m ; (2) *k ; (2) *j + (2) *k + ((-2)) *l ; ((-2)) *a + (1) *i ; 0; (2) *a ; ((-1)) *k ; ((-1)) *m ; (1) *k ; (2) *d + ((-1)) *l ; (2) *b + ((-2)) *j + (1) *k + ((-1)) *l ; (1) *m ; 0; (2) *l ; (2) *f*k + (2) *k*l + ((-1)) *h*m ; (1) *h*k + ((-1)) *f*m ; ((-2)) *d*k ; (2) *a*k + ((-3)) *a*l + (1) *k*m ; (2) *j^2 + ((-1)) *k^2 + (3) *k*l + ((-2)) *l^2 + (3) *a*m ; ((-1)) *k^2 + (1) *k*l ; (1) *c*k + ((-1)) *h*k + ((-2)) *d*m + ((-2)) *k*m ; ((-1)) *k^2 + (1) *k*l + (2) *a*m + ((-1)) *h*m ; (3) *a*k + ((-1)) *h*k + ((-1)) *a*l + (1) *h*l + (1) *k*m ; (2) *j*k + ((-2)) *k^2 + ((-2)) *j*l + (2) *k*l + ((-1)) *h*m ; ((-1)) *b*m ; (2) *b*k + ((-1)) *j*k + (1) *k^2 + (1) *j*l + ((-3)) *k*l + (2) *l^2 + (1) *a*m + (1) *h*m ; (1) *c*k + ((-1)) *h*k + ((-1)) *c*l ; ((-2)) *b*k + (1) *d*k + (2) *b*l + ((-3)) *d*l + (2) *k*l + ((-1)) *a*m + ((-1)) *c*m + (1) *h*m ; (2) *a*c + (2) *a*e + ((-1)) *c*e + (1) *d*f + ((-1)) *c*h + ((-1)) *e*h + (1) *b*k + (1) *d*k + (1) *f*k + ((-1)) *g*k ; (2) *a*h*k + ((-1)) *c*h*k + ((-2)) *b*j*k + ((-1)) *j*k^2 + ((-1)) *a*c*l + (1) *c*h*l + ((-2)) *d*j*l + (4) *d*k*l + (2) *j*l^2 + ((-2)) *k*l^2 + (2) *b*h*m + ((-2)) *d*h*m + (2) *d*i*m + ((-1)) *c*j*m + (2) *h*k*m + ((-2)) *i*k*m ; (2) *g*k*l + ((-2)) *k^2*l + (1) *h*k*m + ((-1)) *i*k*m ; ((-3)) *a*g*k + (5) *a*k*l + ((-2)) *a*l^2 + (2) *h*l^2 + ((-1)) *a*h*m + (2) *a*i*m + ((-1)) *h*i*m + (1) *i^2*m ; ((-1)) *a^2*l + (1) *a*h*l + (3) *a*g*m + (1) *b*h*m + ((-1)) *b*i*m + (1) *h*k*m + (1) *i*k*m ; ((-2)) *a*b*k + (2) *b*c*k + (2) *a*d*k + (3) *a*g*k + ((-1)) *d*h*k + ((-1)) *a*k^2 + (1) *c*k^2 + ((-2)) *a*k*l + ((-2)) *c*k*l + ((-3)) *a*c*m + (3) *a*h*m + ((-1)) *c*i*m + (1) *d*k*m ; (2) *b^2*k + (2) *a*c*k + ((-2)) *b*d*k + ((-1)) *c*h*k + ((-1)) *a*i*k + (1) *c*i*k + (1) *b*k^2 + ((-1)) *b*k*l + ((-2)) *d*k*l + (2) *k*l^2 + ((-3)) *a*d*m + ((-2)) *d*i*m + ((-1)) *a*k*m ; (2) *b*c*j + ((-1)) *c*j^2 + (1) *h*j^2 + (2) *b*c*k + ((-1)) *b*e*k + (3) *a*f*k + (1) *c*f*k + ((-4)) *a*g*k + (1) *e*g*k + (1) *b*h*k + ((-1)) *f*h*k + ((-2)) *a*k^2 + (1) *c*k^2 + ((-2)) *b*c*l + (1) *a*f*l + ((-1)) *f*h*l + ((-1)) *a*j*l + ((-1)) *c*j*l + (1) *e*j*l + (4) *a*k*l + ((-3)) *c*k*l + (2) *c*l^2 + (2) *a*c*m + ((-1)) *c*e*m + (1) *b*f*m + ((-1)) *d*f*m + ((-1)) *b*g*m + ((-2)) *a*h*m + ((-1)) *b*j*m + (1) *g*j*m + (2) *f*k*m ; (1) *a*e*k + ((-1)) *c*e*k + (1) *b*f*k + ((-1)) *f*g*k + ((-1)) *a*h*k + (1) *c*h*k + (1) *b*j*k + ((-1)) *g*j*k + ((-2)) *b*j*l + (2) *g*j*l + ((-2)) *b*k*l + (2) *g*k*l + ((-1)) *b*c*m + (1) *b*e*m + ((-1)) *d*e*m + ((-1)) *a*g*m + (2) *c*g*m + ((-2)) *d*h*m + (1) *g*h*m + (1) *d*i*m + ((-1)) *c*j*m + (1) *h*j*m ; ];
[
0; 0; 0; 0; 0; ((-1)) *g + (1) *l ; 0; 0; 0; 0; 0; 0; (1) *d + ((-1)) *k ; 0; 0; 0; (1) *f ; 0; 0; (1) *d*k + (1) *c*m ; ((-1)) *a*l ; (1) *k*l + ((-1)) *l^2 ; (1) *h*m ; ((-1)) *h*k + (1) *d*m ; 0; ((-1)) *a*l + (1) *h*l ; (1) *k^2 + ((-1)) *k*l ; 0; ((-1)) *k*l + (1) *l^2 ; ((-1)) *c*l + (1) *h*l ; ((-1)) *b*d + (1) *b*k + ((-1)) *d*l + (1) *k*l ; (1) *b*d + (1) *c*e + ((-1)) *d*f + ((-1)) *e*h ; (1) *h^2*k + ((-1)) *h*i*k + (1) *d*j*k + ((-1)) *j*k^2 + ((-1)) *d*j*l + (1) *j*k*l + ((-1)) *k^2*l + (1) *d*i*m ; (1) *g*k^2 + ((-1)) *k^2*l ; (1) *h*k*l + (1) *b*g*m ; ((-1)) *b*f*j + (1) *b*g*k + ((-1)) *b*k*l + ((-1)) *b*i*m ; (1) *a*g*k + ((-1)) *b*h*k + (1) *b*i*k + ((-1)) *g*i*k + ((-1)) *a*d*l + (1) *d*h*l + ((-1)) *a*k*l + ((-1)) *c*k*l + (1) *h*k*l + ((-1)) *b*d*m + (1) *a*h*m + (1) *c*i*m + ((-1)) *h*i*m ; ((-1)) *b*g*k + ((-1)) *a*h*k + (1) *b*k^2 + (1) *b*k*l + ((-1)) *d*k*l + (1) *k*l^2 + (1) *b*c*m + ((-1)) *b*h*m + (1) *d*i*m ; (1) *a*d*f + ((-1)) *b*c*g + ((-1)) *b*f*h + ((-1)) *a*d*j + (1) *d*e*j + ((-1)) *b*e*k + (1) *a*f*k + ((-1)) *a*g*k + (2) *b*h*k + (1) *a*k^2 + ((-1)) *d*h*l + ((-1)) *c*j*l + (1) *h*j*l + ((-1)) *c*k*l + (1) *c*l^2 ; ((-1)) *b*f*k + (1) *b*g*k + (1) *f*g*k + ((-1)) *g^2*k + ((-1)) *b*k*l + (1) *g*k*l ; ];
[
0; 0; 0; ((-1)) *d ; 0; 0; (1) *a ; (1) *a ; 0; 0; ((-1)) *j ; 0; 0; (1) *a ; ((-1)) *f ; 0; 0; 0; (1) *b*d + ((-1)) *c*h ; (1) *a*j ; 0; 0; ((-1)) *b*c + (1) *d*h ; ((-1)) *a*i + (1) *h*i ; 0; 0; ((-1)) *a*b + ((-2)) *a*j ; ((-1)) *a^2 + ((-1)) *a*h ; ((-1)) *a*d + ((-1)) *d*h + (1) *c*j + (1) *h*j ; ((-1)) *a*c ; 0; ((-1)) *a*h*j + ((-1)) *c*h*j ; 0; 0; 0; (1) *a*c*i + ((-1)) *c*h*i ; ((-1)) *b*c*i + (1) *d*h*i ; ((-1)) *a*c*h + (1) *c*e*h + ((-1)) *d*h*j ; ((-1)) *a*b*c + (1) *b*c*e + ((-1)) *a*d*e + (1) *a*c*g + (1) *a*d*h + ((-1)) *c*g*h + (1) *b*g*j + ((-1)) *g^2*j ; ];
[
0; (1) *c ; 0; ((-1)) *k + (1) *l ; ((-1)) *a ; 0; 0; 0; 0; 0; ((-1)) *d + (1) *l ; 0; 0; 0; ((-1)) *l ; ((-1)) *k*l ; (1) *f*m ; 0; 0; ((-1)) *k*l + (1) *l^2 ; 0; (1) *d*m ; ((-1)) *a*m ; 0; ((-1)) *j*k + (1) *k^2 + (1) *j*l + ((-1)) *k*l ; 0; ((-1)) *b*k + (1) *k*l + ((-1)) *l^2 ; (1) *c*l ; (1) *b*k + ((-1)) *b*l + (1) *d*l + ((-1)) *k*l ; ((-1)) *a*c + ((-1)) *a*e + (1) *c*e + ((-1)) *d*f ; ((-1)) *d*k*l + (1) *j*k*l + ((-1)) *j*l^2 + (1) *k*l^2 ; ((-1)) *g*k*l + (1) *k^2*l ; ((-1)) *a*k*l + (1) *a*l^2 + ((-1)) *h*l^2 + ((-1)) *a*i*m ; 0; (1) *c*k*l + (1) *c*i*m ; (1) *d*k*l + ((-1)) *k*l^2 + (1) *d*i*m ; ((-1)) *b*c*k + (1) *a*k^2 + (1) *b*c*l + (1) *c*j*l + ((-2)) *a*k*l + (1) *c*k*l + ((-1)) *c*l^2 ; ((-1)) *b*j*k + (1) *g*j*k + (1) *b*j*l + ((-1)) *g*j*l + (1) *b*k*l + ((-1)) *g*k*l ; ];
[
(1) *h ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *l ; 0; 0; 0; 0; 0; 0; (1) *k^2 ; 0; 0; (1) *k^2 + (1) *h*m ; 0; 0; 0; (1) *f*k + ((-1)) *j*k + (1) *k^2 + (1) *j*l + ((-1)) *k*l ; 0; 0; (1) *h*l ; ((-1)) *b*l ; ((-1)) *a*e + ((-1)) *b*f ; (1) *j*k*l + ((-1)) *j*l^2 + (1) *k*l^2 ; 0; 0; 0; (1) *a*k^2 + (1) *h*k*l ; ((-1)) *b*k*l ; (1) *a*k^2 + (1) *h*j*l + ((-1)) *a*k*l ; (1) *b*f*k + ((-1)) *f*g*k + ((-1)) *b*j*k + (1) *g*j*k + (1) *b*j*l + ((-1)) *g*j*l ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *k ; 0; 0; ((-1)) *e ; 0; 0; ((-1)) *b ; 0; 0; (1) *h*k + ((-1)) *i*k ; 0; 0; 0; ((-1)) *b*k ; ((-1)) *a*k ; ((-1)) *b*j ; ((-1)) *b*e + (1) *e*g ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *a*h ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *d*j ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *i*k ; 0; ((-1)) *i*k ; 0; ((-1)) *d*e + ((-1)) *c*f + (1) *c*g + (1) *f*h + (1) *e*k + ((-1)) *h*k ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *c*j ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *g + ((-1)) *j ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *d ; 0; 0; 0; 0; 0; ((-1)) *e*j ; 0; 0; ((-1)) *d*f + (1) *d*g + ((-1)) *e*h ; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *i*k ; 0; (1) *i*k ; 0; 0; ((-1)) *c*e + (1) *d*f + ((-1)) *d*g + (1) *e*h + ((-1)) *f*k + (1) *g*k ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *a ; 0; 0; (1) *i ; ((-1)) *b ; 0; 0; (1) *a ; 0; 0; 0; ((-1)) *a ; 0; ((-1)) *h*j ; 0; 0; 0; (1) *a*i ; ((-1)) *b*i ; (1) *a^2 + ((-1)) *a*e ; (1) *b*e + ((-1)) *e*g ; ];
[
0; 0; 0; 0; 0; 0; 0; (1) *g ; 0; 0; 0; (1) *h ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *h*i ; 0; 0; 0; ((-1)) *b*i + (1) *g*i ; 0; (1) *a*g + ((-1)) *e*g ; 0; ];
[
0; 0; 0; 0; 0; 0; (1) *j + ((-1)) *k ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *j*k ; 0; 0; 0; 0; 0; (1) *a*j + ((-1)) *e*j ; ((-1)) *b*f + (1) *f*g ; ];
[
0; 0; 0; (1) *f ; (1) *e ; ((-1)) *d ; 0; (1) *j ; 0; ((-1)) *c ; (1) *b ; (1) *a ; 0; ((-1)) *a ; 0; (1) *c ; 0; 0; ((-1)) *c*i + (1) *d*j ; 0; 0; 0; 0; 0; ((-1)) *a*d + (1) *d*e ; 0; ];
[
0; 0; (1) *h ; ((-1)) *g ; 0; 0; 0; 0; 0; 0; 0; (1) *h ; (1) *b ; 0; 0; 0; 0; 0; 0; (1) *a*h ; ((-1)) *b*h + (1) *b*i + ((-1)) *g*i ; 0; 0; ((-1)) *a*c + (1) *a*h ; (1) *b*c + ((-1)) *c*g ; ];
[
0; (1) *b ; ((-1)) *a ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ];
[
((-1)) *g ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; ((-1)) *c*h ; ((-1)) *b*h + (1) *b*i + ((-1)) *g*i ; 0; 0; 0; ((-1)) *a*d ; (1) *b*d + ((-1)) *d*g ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *d ; ((-1)) *a ; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *c ; 0; ((-1)) *a ; 0; 0; 0; 0; ];
[
0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *f ; 0; 0; ((-1)) *a ; 0; 0; 0; ];
[
0; 0; 0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *f ; 0; ((-1)) *d ; 0; 0; 0; ];
[
0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *f ; (1) *c ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *g ; 0; 0; 0; ((-1)) *a ; (1) *b ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *h + ((-1)) *i ; (1) *e ; 0; 0; 0; ((-1)) *a ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *e ; 0; 0; ((-1)) *d ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *e ; 0; ((-1)) *c ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; 0; 0; ((-1)) *a ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; 0; ((-1)) *d ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; ((-1)) *c ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; ((-1)) *f ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; ((-1)) *e ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *i ; ((-1)) *g + (1) *l ; ];
];
c:=
(-2);
Second certificate
CR:=[
((-1)) ; (1) *m ; ((-1)) *k ; (1) *a + ((-1)) *n ; (1) *m + ((-1)) *n ; ((-1)) *c ; 0; (1) *j + ((-2)) *k ; (1) *n ; (1) *f*m + ((-1)) *f*n + (2) *k*n ; ((-1)) *f*k + ((-1)) *k^2 + ((-1)) *m^2 + (2) *m*n ; ((-1)) *d*m + ((-1)) *k*m + (1) *d*n + (1) *k*n ; (1) *j*k + ((-1)) *j*l + ((-2)) *a*n + (1) *m*n ; (2) *a*k + ((-1)) *a*l + (1) *l*m ; (1) *a*k ; ((-1)) *m^2 + (1) *m*n ; (1) *a*k ; (1) *a*m + ((-2)) *a*n ; ((-1)) *j*m + (1) *k*m + (1) *l*m + (2) *k*n + ((-2)) *l*n ; ((-1)) *b*j + (2) *b*k + (1) *j*k + ((-1)) *j*l ; ((-1)) *a*j + ((-1)) *a*k + (2) *a*l + ((-1)) *h*l + (1) *k*m + ((-1)) *l*m + (1) *b*n + ((-1)) *k*n + (1) *l*n ; ((-1)) *d*k + ((-1)) *j*k + (1) *k*l + ((-1)) *h*m + (1) *m^2 + (1) *h*n + ((-1)) *m*n ; (1) *a*k + (1) *d*m + ((-1)) *l*m ; ((-1)) *b*m + (1) *g*m + (2) *b*n + ((-2)) *g*n ; (1) *d*h*k + (1) *a*j*k + ((-1)) *c*k^2 + (1) *h*j*l + ((-1)) *h*k*l + ((-1)) *a*h*m + (1) *c*h*m + ((-1)) *h*i*m + ((-1)) *j*k*m + (1) *k^2*m + ((-1)) *c*m^2 + ((-1)) *i*m^2 + (1) *m^3 + ((-1)) *a*c*n + ((-1)) *c*h*n + (1) *h*i*n + ((-1)) *d*k*n + (1) *a*m*n + (1) *c*m*n + (1) *i*m*n + ((-1)) *m^2*n ; ((-1)) *g*k*m + (1) *k^2*m + (1) *k*l*m + ((-1)) *h*m^2 + (1) *i*m^2 + (1) *m^3 + (1) *g*k*n + ((-2)) *k*l*n + (3) *h*m*n + ((-3)) *i*m*n + ((-1)) *m^2*n + ((-1)) *h*n^2 + (2) *i*n^2 + ((-1)) *m*n^2 ; (1) *a*g*m + (1) *h*k*m + ((-1)) *i*k*m + ((-1)) *g*m^2 + (1) *l*m^2 + (1) *a*b*n + ((-1)) *a*g*n + (1) *b*h*n + (4) *a*k*n + ((-1)) *h*k*n + ((-2)) *a*l*n + (1) *h*l*n + ((-1)) *b*m*n + (1) *g*m*n + ((-1)) *l*m*n + ((-1)) *k*n^2 + (1) *l*n^2 ; (1) *b*h*k + ((-1)) *a*k^2 + (2) *a*k*l + ((-2)) *h*k*l + ((-1)) *b*g*m + ((-1)) *a*h*m + (1) *a*i*m + (1) *g*k*m + ((-1)) *a*m^2 + (1) *h*m^2 + ((-1)) *i*m^2 + (1) *b*g*n + (1) *a*h*n + ((-1)) *b*k*n + ((-1)) *g*k*n + (1) *k^2*n + (1) *a*m*n + ((-1)) *h*m*n + (1) *i*m*n + ((-1)) *i*n^2 + (1) *m*n^2 ; (1) *a^2*k + ((-1)) *a*c*k + ((-1)) *a*k*m + (1) *a*l*m + ((-1)) *h*l*m + (1) *b*m^2 + ((-1)) *a*d*n + ((-1)) *b*h*n + ((-1)) *a*k*n + (1) *i*k*n + (1) *h*l*n + (1) *d*m*n + ((-1)) *g*m*n + (1) *k*m*n + ((-1)) *l*m*n + ((-1)) *d*n^2 + (1) *g*n^2 ; ((-1)) *a*b*k + ((-1)) *a*d*k + (1) *a*k*l + (1) *g*k*m + ((-2)) *k*l*m + (1) *h*m^2 + ((-1)) *i*m^2 + ((-1)) *a*i*n + (1) *b*k*n + (1) *d*k*n + ((-1)) *g*k*n + ((-1)) *k^2*n + (1) *k*l*n + (1) *a*m*n + ((-1)) *h*m*n + (2) *i*m*n + ((-1)) *m^2*n ; (1) *b*c*h + ((-1)) *a*d*h + (1) *d*j^2 + ((-2)) *a*c*k + ((-1)) *d*f*k + (1) *a*h*k + ((-1)) *c*h*k + (1) *d*j*k + ((-1)) *j^2*k + (2) *a*c*l + ((-1)) *c*h*l + ((-1)) *d*j*l + (1) *f*k*l + ((-1)) *b*c*m + (1) *d*e*m + ((-1)) *b*h*m + (1) *d*h*m + (1) *c*j*m + ((-1)) *h*j*m + (1) *c*k*m + (1) *e*k*m + ((-1)) *c*l*m + ((-1)) *e*l*m + (1) *h*l*m + (1) *b*m^2 + (1) *b*c*n + (1) *a*d*n + ((-1)) *d*e*n + ((-1)) *c*f*n + ((-1)) *a*g*n + (3) *b*h*n + (1) *h*j*n + (2) *a*k*n + ((-1)) *c*k*n + (1) *c*l*n + ((-2)) *h*l*n + ((-1)) *b*m*n + ((-1)) *d*m*n + (1) *g*m*n + ((-1)) *j*m*n + (1) *d*n^2 + ((-1)) *g*n^2 ; (1) *b*c*k + ((-1)) *c*g*k + ((-1)) *a*c*m + (1) *c*e*m + ((-1)) *d*f*m + ((-1)) *b*g*m + (1) *g^2*m + ((-1)) *e*h*m + ((-1)) *b*j*m + (1) *d*j*m + (1) *g*j*m + (1) *b*k*m + (1) *f*k*m + ((-1)) *g*k*m + ((-1)) *j*k*m + (1) *b*l*m + ((-1)) *g*l*m + (1) *a*m^2 + (2) *a*c*n + ((-1)) *b*d*n + ((-1)) *c*e*n + (1) *d*f*n + (2) *b*g*n + (1) *d*g*n + ((-2)) *g^2*n + ((-1)) *a*h*n + (1) *e*h*n + ((-1)) *d*j*n + ((-1)) *d*k*n + ((-1)) *f*k*n + (1) *g*k*n + (1) *j*k*n + ((-2)) *b*l*n + (2) *g*l*n + ((-1)) *a*m*n + (1) *h*m*n + ((-1)) *m^2*n + ((-1)) *c*n^2 + (1) *m*n^2 ; ];
C:=[
[
((-1)) ; (1) *m ; ((-1)) *k ; (1) *a + ((-1)) *n ; (1) *m + ((-1)) *n ; ((-1)) *c ; 0; (1) *j + ((-2)) *k ; (1) *n ; (1) *f*m + ((-1)) *f*n + (2) *k*n ; ((-1)) *f*k + ((-1)) *k^2 + ((-1)) *m^2 + (2) *m*n ; ((-1)) *d*m + ((-1)) *k*m + (1) *d*n + (1) *k*n ; (1) *j*k + ((-1)) *j*l + ((-2)) *a*n + (1) *m*n ; (2) *a*k + ((-1)) *a*l + (1) *l*m ; (1) *a*k ; ((-1)) *m^2 + (1) *m*n ; (1) *a*k ; (1) *a*m + ((-2)) *a*n ; ((-1)) *j*m + (1) *k*m + (1) *l*m + (2) *k*n + ((-2)) *l*n ; ((-1)) *b*j + (2) *b*k + (1) *j*k + ((-1)) *j*l ; ((-1)) *a*j + ((-1)) *a*k + (2) *a*l + ((-1)) *h*l + (1) *k*m + ((-1)) *l*m + (1) *b*n + ((-1)) *k*n + (1) *l*n ; ((-1)) *d*k + ((-1)) *j*k + (1) *k*l + ((-1)) *h*m + (1) *m^2 + (1) *h*n + ((-1)) *m*n ; (1) *a*k + (1) *d*m + ((-1)) *l*m ; ((-1)) *b*m + (1) *g*m + (2) *b*n + ((-2)) *g*n ; (1) *d*h*k + (1) *a*j*k + ((-1)) *c*k^2 + (1) *h*j*l + ((-1)) *h*k*l + ((-1)) *a*h*m + (1) *c*h*m + ((-1)) *h*i*m + ((-1)) *j*k*m + (1) *k^2*m + ((-1)) *c*m^2 + ((-1)) *i*m^2 + (1) *m^3 + ((-1)) *a*c*n + ((-1)) *c*h*n + (1) *h*i*n + ((-1)) *d*k*n + (1) *a*m*n + (1) *c*m*n + (1) *i*m*n + ((-1)) *m^2*n ; ((-1)) *g*k*m + (1) *k^2*m + (1) *k*l*m + ((-1)) *h*m^2 + (1) *i*m^2 + (1) *m^3 + (1) *g*k*n + ((-2)) *k*l*n + (3) *h*m*n + ((-3)) *i*m*n + ((-1)) *m^2*n + ((-1)) *h*n^2 + (2) *i*n^2 + ((-1)) *m*n^2 ; (1) *a*g*m + (1) *h*k*m + ((-1)) *i*k*m + ((-1)) *g*m^2 + (1) *l*m^2 + (1) *a*b*n + ((-1)) *a*g*n + (1) *b*h*n + (4) *a*k*n + ((-1)) *h*k*n + ((-2)) *a*l*n + (1) *h*l*n + ((-1)) *b*m*n + (1) *g*m*n + ((-1)) *l*m*n + ((-1)) *k*n^2 + (1) *l*n^2 ; (1) *b*h*k + ((-1)) *a*k^2 + (2) *a*k*l + ((-2)) *h*k*l + ((-1)) *b*g*m + ((-1)) *a*h*m + (1) *a*i*m + (1) *g*k*m + ((-1)) *a*m^2 + (1) *h*m^2 + ((-1)) *i*m^2 + (1) *b*g*n + (1) *a*h*n + ((-1)) *b*k*n + ((-1)) *g*k*n + (1) *k^2*n + (1) *a*m*n + ((-1)) *h*m*n + (1) *i*m*n + ((-1)) *i*n^2 + (1) *m*n^2 ; (1) *a^2*k + ((-1)) *a*c*k + ((-1)) *a*k*m + (1) *a*l*m + ((-1)) *h*l*m + (1) *b*m^2 + ((-1)) *a*d*n + ((-1)) *b*h*n + ((-1)) *a*k*n + (1) *i*k*n + (1) *h*l*n + (1) *d*m*n + ((-1)) *g*m*n + (1) *k*m*n + ((-1)) *l*m*n + ((-1)) *d*n^2 + (1) *g*n^2 ; ((-1)) *a*b*k + ((-1)) *a*d*k + (1) *a*k*l + (1) *g*k*m + ((-2)) *k*l*m + (1) *h*m^2 + ((-1)) *i*m^2 + ((-1)) *a*i*n + (1) *b*k*n + (1) *d*k*n + ((-1)) *g*k*n + ((-1)) *k^2*n + (1) *k*l*n + (1) *a*m*n + ((-1)) *h*m*n + (2) *i*m*n + ((-1)) *m^2*n ; (1) *b*c*h + ((-1)) *a*d*h + (1) *d*j^2 + ((-2)) *a*c*k + ((-1)) *d*f*k + (1) *a*h*k + ((-1)) *c*h*k + (1) *d*j*k + ((-1)) *j^2*k + (2) *a*c*l + ((-1)) *c*h*l + ((-1)) *d*j*l + (1) *f*k*l + ((-1)) *b*c*m + (1) *d*e*m + ((-1)) *b*h*m + (1) *d*h*m + (1) *c*j*m + ((-1)) *h*j*m + (1) *c*k*m + (1) *e*k*m + ((-1)) *c*l*m + ((-1)) *e*l*m + (1) *h*l*m + (1) *b*m^2 + (1) *b*c*n + (1) *a*d*n + ((-1)) *d*e*n + ((-1)) *c*f*n + ((-1)) *a*g*n + (3) *b*h*n + (1) *h*j*n + (2) *a*k*n + ((-1)) *c*k*n + (1) *c*l*n + ((-2)) *h*l*n + ((-1)) *b*m*n + ((-1)) *d*m*n + (1) *g*m*n + ((-1)) *j*m*n + (1) *d*n^2 + ((-1)) *g*n^2 ; (1) *b*c*k + ((-1)) *c*g*k + ((-1)) *a*c*m + (1) *c*e*m + ((-1)) *d*f*m + ((-1)) *b*g*m + (1) *g^2*m + ((-1)) *e*h*m + ((-1)) *b*j*m + (1) *d*j*m + (1) *g*j*m + (1) *b*k*m + (1) *f*k*m + ((-1)) *g*k*m + ((-1)) *j*k*m + (1) *b*l*m + ((-1)) *g*l*m + (1) *a*m^2 + (2) *a*c*n + ((-1)) *b*d*n + ((-1)) *c*e*n + (1) *d*f*n + (2) *b*g*n + (1) *d*g*n + ((-2)) *g^2*n + ((-1)) *a*h*n + (1) *e*h*n + ((-1)) *d*j*n + ((-1)) *d*k*n + ((-1)) *f*k*n + (1) *g*k*n + (1) *j*k*n + ((-2)) *b*l*n + (2) *g*l*n + ((-1)) *a*m*n + (1) *h*m*n + ((-1)) *m^2*n + ((-1)) *c*n^2 + (1) *m*n^2 ; ];
[
(1) *h ; 0; 0; 0; 0; (1) *a ; 0; 0; 0; ((-1)) *f*j ; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *a*j ; ((-1)) *d*j ; (2) *a*d + ((-1)) *b*h ; 0; 0; 0; 0; 0; 0; 0; (1) *b*c*h ; (1) *b*c*f + ((-1)) *c*f*g ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *d*j ; 0; 0; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *i*k ; 0; ((-1)) *i*k ; 0; ((-1)) *d*e + ((-1)) *c*f + (1) *c*g + (1) *f*h + (1) *e*k + ((-1)) *h*k ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *i ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *i*k ; 0; (1) *i*k ; 0; 0; ((-1)) *c*e + (1) *d*f + ((-1)) *d*g + (1) *e*h + ((-1)) *f*k + (1) *g*k ; ];
[
0; 0; 0; 0; 0; 0; (1) *g ; 0; 0; 0; (1) *h ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *h*i ; 0; 0; 0; ((-1)) *b*i + (1) *g*i ; 0; (1) *a*g + ((-1)) *e*g ; 0; ];
[
0; 0; 0; 0; 0; (1) *j + ((-1)) *k ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *j*k ; 0; 0; 0; 0; 0; (1) *a*j + ((-1)) *e*j ; ((-1)) *b*f + (1) *f*g ; ];
[
0; 0; (1) *f ; (1) *e ; ((-1)) *d ; 0; (1) *j ; 0; ((-1)) *c ; (1) *b ; (1) *a ; 0; ((-1)) *a ; 0; (1) *c ; 0; 0; ((-1)) *c*i + (1) *d*j ; 0; 0; 0; 0; 0; ((-1)) *a*d + (1) *d*e ; 0; ];
[
0; (1) *h ; ((-1)) *g ; 0; 0; 0; 0; 0; 0; 0; (1) *h ; (1) *b ; 0; 0; 0; 0; 0; 0; (1) *a*h ; ((-1)) *b*h + (1) *b*i + ((-1)) *g*i ; 0; 0; ((-1)) *a*c + (1) *a*h ; (1) *b*c + ((-1)) *c*g ; ];
[
((-1)) *g ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *b ; 0; 0; 0; 0; ((-1)) *c*h ; ((-1)) *b*h + (1) *b*i + ((-1)) *g*i ; 0; 0; 0; ((-1)) *a*d ; (1) *b*d + ((-1)) *d*g ; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *d ; ((-1)) *a ; 0; 0; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *c ; 0; ((-1)) *a ; 0; 0; 0; 0; ];
[
0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *f ; 0; 0; ((-1)) *a ; 0; 0; 0; ];
[
0; 0; 0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; (1) *f ; 0; ((-1)) *d ; 0; 0; 0; ];
[
0; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *f ; (1) *c ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; ((-1)) *g ; 0; 0; 0; ((-1)) *a ; (1) *b ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; (1) *h + ((-1)) *i ; (1) *e ; 0; 0; 0; ((-1)) *a ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *e ; 0; 0; ((-1)) *d ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *e ; 0; ((-1)) *c ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; 0; 0; ((-1)) *a ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; 0; ((-1)) *d ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; 0; ((-1)) *c ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; 0; ((-1)) *f ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *j ; ((-1)) *e ; 0; ];
[
0; 0; 0; 0; 0; 0; ((-1)) *i ; ((-1)) *g + (1) *l ; ];
];
c:=
1;