Euler circle
Geogebra sheet
Coq statement
Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point,
middle A B C1 -> middle B C A1 -> middle C A B1 ->
orthogonal A B C C2 -> collinear A B C2 ->
orthogonal B C A A2 -> collinear B C A2 ->
orthogonal A C B B2 -> collinear A C B2 ->
distance2 O A1 = distance2 O B1 ->
distance2 O A1 = distance2 O C1 ->
(distance2 O A2 = distance2 O A1
/\distance2 O B2 = distance2 O A1
/\distance2 O C2 = distance2 O A1)
\/ collinear A B C.
Proof. geo_begin. tzR. tzR. tzR. Qed.
Algebraic version
First goal
p:= (1) *c^2*h*i + (1) *d^2*h*i + ((-1)) *c^2*h*j + ((-1)) *d^2*h*j + ((-1)) *c^2*g*k + ((-1)) *d^2*g*k + (1) *c^2*j*k + (1) *d^2*j*k + (1) *c^2*g*l + (1) *d^2*g*l + ((-1)) *c^2*i*l + ((-1)) *d^2*i*l + ((-2)) *c*h*i*q + (2) *c*h*j*q + (2) *c*g*k*q + ((-2)) *c*j*k*q + ((-2)) *c*g*l*q + (2) *c*i*l*q + (2) *h*i*q*r + ((-2)) *h*j*q*r + ((-2)) *g*k*q*r + (2) *j*k*q*r + (2) *g*l*q*r + ((-2)) *i*l*q*r + ((-1)) *h*i*r^2 + (1) *h*j*r^2 + (1) *g*k*r^2 + ((-1)) *j*k*r^2 + ((-1)) *g*l*r^2 + (1) *i*l*r^2 + ((-2)) *d*h*i*s + (2) *d*h*j*s + (2) *d*g*k*s + ((-2)) *d*j*k*s + ((-2)) *d*g*l*s + (2) *d*i*l*s + (2) *h*i*s*t + ((-2)) *h*j*s*t + ((-2)) *g*k*s*t + (2) *j*k*s*t + (2) *g*l*s*t + ((-2)) *i*l*s*t + ((-1)) *h*i*t^2 + (1) *h*j*t^2 + (1) *g*k*t^2 + ((-1)) *j*k*t^2 + ((-1)) *g*l*t^2 + (1) *i*l*t^2
F:= [
((-1)) *o^2 + ((-1)) *p^2 + (2) *o*q + ((-2)) *q*r + (1) *r^2 + (2) *p*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *m^2 + ((-1)) *n^2 + (2) *m*q + ((-2)) *q*r + (1) *r^2 + (2) *n*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *k + ((-1)) *l + (2) *p ;
((-1)) *i + ((-1)) *j + (2) *o ;
((-1)) *h + ((-1)) *l + (2) *t ;
((-1)) *g + ((-1)) *j + (2) *r ;
((-1)) *h + ((-1)) *k + (2) *n ;
((-1)) *g + ((-1)) *i + (2) *m ;
(1) *e*g + (1) *f*h + ((-1)) *e*i + ((-1)) *g*j + (1) *i*j + ((-1)) *f*k + ((-1)) *h*l + (1) *k*l ;
(1) *f*g + ((-1)) *e*h + ((-1)) *f*i + (1) *h*i + (1) *e*k + ((-1)) *g*k ;
((-1)) *c*g + ((-1)) *d*h + (1) *g*i + (1) *c*j + ((-1)) *i*j + (1) *h*k + (1) *d*l + ((-1)) *k*l ;
((-1)) *d*g + (1) *c*h + (1) *d*j + ((-1)) *h*j + ((-1)) *c*l + (1) *g*l ;
((-1)) *a*i + (1) *g*i + (1) *a*j + ((-1)) *g*j + ((-1)) *b*k + (1) *h*k + (1) *b*l + ((-1)) *h*l ;
((-1)) *b*i + (1) *b*j + (1) *a*k + ((-1)) *j*k + ((-1)) *a*l + (1) *i*l ;
];
Second goal
p:= (1) *a^2*h*i + (1) *b^2*h*i + ((-1)) *a^2*h*j + ((-1)) *b^2*h*j + ((-1)) *a^2*g*k + ((-1)) *b^2*g*k + (1) *a^2*j*k + (1) *b^2*j*k + (1) *a^2*g*l + (1) *b^2*g*l + ((-1)) *a^2*i*l + ((-1)) *b^2*i*l + ((-2)) *a*h*i*q + (2) *a*h*j*q + (2) *a*g*k*q + ((-2)) *a*j*k*q + ((-2)) *a*g*l*q + (2) *a*i*l*q + (2) *h*i*q*r + ((-2)) *h*j*q*r + ((-2)) *g*k*q*r + (2) *j*k*q*r + (2) *g*l*q*r + ((-2)) *i*l*q*r + ((-1)) *h*i*r^2 + (1) *h*j*r^2 + (1) *g*k*r^2 + ((-1)) *j*k*r^2 + ((-1)) *g*l*r^2 + (1) *i*l*r^2 + ((-2)) *b*h*i*s + (2) *b*h*j*s + (2) *b*g*k*s + ((-2)) *b*j*k*s + ((-2)) *b*g*l*s + (2) *b*i*l*s + (2) *h*i*s*t + ((-2)) *h*j*s*t + ((-2)) *g*k*s*t + (2) *j*k*s*t + (2) *g*l*s*t + ((-2)) *i*l*s*t + ((-1)) *h*i*t^2 + (1) *h*j*t^2 + (1) *g*k*t^2 + ((-1)) *j*k*t^2 + ((-1)) *g*l*t^2 + (1) *i*l*t^2
F:= [
((-1)) *o^2 + ((-1)) *p^2 + (2) *o*q + ((-2)) *q*r + (1) *r^2 + (2) *p*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *m^2 + ((-1)) *n^2 + (2) *m*q + ((-2)) *q*r + (1) *r^2 + (2) *n*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *k + ((-1)) *l + (2) *p ;
((-1)) *i + ((-1)) *j + (2) *o ;
((-1)) *h + ((-1)) *l + (2) *t ;
((-1)) *g + ((-1)) *j + (2) *r ;
((-1)) *h + ((-1)) *k + (2) *n ;
((-1)) *g + ((-1)) *i + (2) *m ;
(1) *e*g + (1) *f*h + ((-1)) *e*i + ((-1)) *g*j + (1) *i*j + ((-1)) *f*k + ((-1)) *h*l + (1) *k*l ;
(1) *f*g + ((-1)) *e*h + ((-1)) *f*i + (1) *h*i + (1) *e*k + ((-1)) *g*k ;
((-1)) *c*g + ((-1)) *d*h + (1) *g*i + (1) *c*j + ((-1)) *i*j + (1) *h*k + (1) *d*l + ((-1)) *k*l ;
((-1)) *d*g + (1) *c*h + (1) *d*j + ((-1)) *h*j + ((-1)) *c*l + (1) *g*l ;
((-1)) *a*i + (1) *g*i + (1) *a*j + ((-1)) *g*j + ((-1)) *b*k + (1) *h*k + (1) *b*l + ((-1)) *h*l ;
((-1)) *b*i + (1) *b*j + (1) *a*k + ((-1)) *j*k + ((-1)) *a*l + (1) *i*l ;
];
Third goal
p:= (1) *e^2*h*i + (1) *f^2*h*i + ((-1)) *e^2*h*j + ((-1)) *f^2*h*j + ((-1)) *e^2*g*k + ((-1)) *f^2*g*k + (1) *e^2*j*k + (1) *f^2*j*k + (1) *e^2*g*l + (1) *f^2*g*l + ((-1)) *e^2*i*l + ((-1)) *f^2*i*l + ((-2)) *e*h*i*q + (2) *e*h*j*q + (2) *e*g*k*q + ((-2)) *e*j*k*q + ((-2)) *e*g*l*q + (2) *e*i*l*q + (2) *h*i*q*r + ((-2)) *h*j*q*r + ((-2)) *g*k*q*r + (2) *j*k*q*r + (2) *g*l*q*r + ((-2)) *i*l*q*r + ((-1)) *h*i*r^2 + (1) *h*j*r^2 + (1) *g*k*r^2 + ((-1)) *j*k*r^2 + ((-1)) *g*l*r^2 + (1) *i*l*r^2 + ((-2)) *f*h*i*s + (2) *f*h*j*s + (2) *f*g*k*s + ((-2)) *f*j*k*s + ((-2)) *f*g*l*s + (2) *f*i*l*s + (2) *h*i*s*t + ((-2)) *h*j*s*t + ((-2)) *g*k*s*t + (2) *j*k*s*t + (2) *g*l*s*t + ((-2)) *i*l*s*t + ((-1)) *h*i*t^2 + (1) *h*j*t^2 + (1) *g*k*t^2 + ((-1)) *j*k*t^2 + ((-1)) *g*l*t^2 + (1) *i*l*t^2
F:= [
((-1)) *o^2 + ((-1)) *p^2 + (2) *o*q + ((-2)) *q*r + (1) *r^2 + (2) *p*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *m^2 + ((-1)) *n^2 + (2) *m*q + ((-2)) *q*r + (1) *r^2 + (2) *n*s + ((-2)) *s*t + (1) *t^2 ;
((-1)) *k + ((-1)) *l + (2) *p ;
((-1)) *i + ((-1)) *j + (2) *o ;
((-1)) *h + ((-1)) *l + (2) *t ;
((-1)) *g + ((-1)) *j + (2) *r ;
((-1)) *h + ((-1)) *k + (2) *n ;
((-1)) *g + ((-1)) *i + (2) *m ;
(1) *e*g + (1) *f*h + ((-1)) *e*i + ((-1)) *g*j + (1) *i*j + ((-1)) *f*k + ((-1)) *h*l + (1) *k*l ;
(1) *f*g + ((-1)) *e*h + ((-1)) *f*i + (1) *h*i + (1) *e*k + ((-1)) *g*k ;
((-1)) *c*g + ((-1)) *d*h + (1) *g*i + (1) *c*j + ((-1)) *i*j + (1) *h*k + (1) *d*l + ((-1)) *k*l ;
((-1)) *d*g + (1) *c*h + (1) *d*j + ((-1)) *h*j + ((-1)) *c*l + (1) *g*l ;
((-1)) *a*i + (1) *g*i + (1) *a*j + ((-1)) *g*j + ((-1)) *b*k + (1) *h*k + (1) *b*l + ((-1)) *h*l ;
((-1)) *b*i + (1) *b*j + (1) *a*k + ((-1)) *j*k + ((-1)) *a*l + (1) *i*l ;
];
Certificates
First certificate
CR:=[
(1) *d + ((-1)) *t ; ((-2)) *r ; (1) *c + ((-2)) *q + (1) *r ; (1) *d*p + (4) *q*r + ((-2)) *r^2 + ((-2)) *n*s + ((-2)) *p*s + ((-2)) *d*t + (2) *n*t + (1) *p*t + (4) *s*t + ((-2)) *t^2 ; (1) *c*p + (2) *n*q + ((-2)) *n*r + ((-1)) *p*r + ((-2)) *c*t ; (1) *c*n*o + (2) *c^2*p + (2) *d^2*p + (1) *c*m*p + (1) *c*o*p + (1) *d*p^2 + ((-2)) *d*m*q + (2) *m*n*q + ((-2)) *d*o*q + ((-4)) *c*p*q + ((-2)) *m*n*r + (2) *d*o*r + ((-1)) *n*o*r + ((-1)) *m*p*r + ((-1)) *o*p*r + (4) *d*q*r + (4) *p*q*r + ((-2)) *d*r^2 + ((-2)) *p*r^2 + ((-2)) *d*n*s + ((-6)) *d*p*s + ((-2)) *c^2*t + ((-2)) *d^2*t + ((-1)) *c*m*t + (1) *d*n*t + ((-1)) *c*o*t + (1) *d*p*t + ((-1)) *p^2*t + (4) *c*q*t + ((-2)) *c*r*t + (1) *m*r*t + (1) *o*r*t + ((-4)) *q*r*t + (2) *r^2*t + (8) *d*s*t + (4) *p*s*t + ((-4)) *d*t^2 + (1) *n*t^2 + ((-1)) *p*t^2 + ((-4)) *s*t^2 + (2) *t^3 ; ((-2)) *c^2*o + ((-2)) *d^2*o + ((-1)) *d*n*o + ((-1)) *d*m*p + (2) *c*n*p + ((-1)) *d*o*p + (1) *c*p^2 + (2) *n^2*q + (4) *c*o*q + (2) *c^2*r + (2) *d^2*r + ((-1)) *c*m*r + (1) *d*n*r + ((-2)) *n^2*r + ((-1)) *c*o*r + (1) *d*p*r + ((-2)) *n*p*r + ((-1)) *p^2*r + ((-4)) *c*q*r + (2) *m*q*r + ((-2)) *o*q*r + (2) *c*r^2 + ((-1)) *m*r^2 + (1) *o*r^2 + (4) *d*o*s + ((-4)) *d*r*s + (2) *n*r*s + (2) *p*r*s + ((-2)) *c*n*t + (1) *n*o*t + ((-2)) *c*p*t + (1) *m*p*t + (1) *o*p*t + (2) *d*r*t + ((-1)) *n*r*t + ((-1)) *p*r*t + ((-4)) *o*s*t + (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *c^2*l + (2) *d^2*l + ((-2)) *c*n*o + ((-2)) *c^2*p + ((-2)) *d^2*p + ((-2)) *c*o*p + ((-2)) *d*p^2 + ((-4)) *c*l*q + (4) *d*o*q + (4) *c*p*q + ((-4)) *d*o*r + (2) *n*o*r + (2) *o*p*r + ((-4)) *d*q*r + (4) *l*q*r + ((-4)) *p*q*r + (2) *d*r^2 + ((-2)) *l*r^2 + (2) *p*r^2 + ((-4)) *d*l*s + (8) *d*p*s + (4) *c*o*t + (2) *p^2*t + ((-4)) *o*q*t + (4) *q*r*t + ((-2)) *r^2*t + ((-4)) *d*s*t + (4) *l*s*t + ((-8)) *p*s*t + (2) *d*t^2 + ((-2)) *l*t^2 + (2) *p*t^2 + (4) *s*t^2 + ((-2)) *t^3 ; ((-2)) *c^2*j + ((-2)) *d^2*j + (2) *c^2*o + (2) *d^2*o + (2) *d*m*p + ((-2)) *c*n*p + (2) *d*o*p + ((-2)) *c*p^2 + (4) *c*j*q + ((-4)) *c*o*q + ((-4)) *d*p*r + (2) *n*p*r + (2) *p^2*r + ((-4)) *j*q*r + (4) *o*q*r + (2) *j*r^2 + ((-2)) *o*r^2 + (4) *d*j*s + ((-4)) *d*o*s + (4) *c*p*t + ((-2)) *m*p*t + ((-2)) *o*p*t + ((-4)) *j*s*t + (4) *o*s*t + (2) *j*t^2 + ((-2)) *o*t^2 ; (1) *c^2*h + (1) *d^2*h + ((-1)) *c^2*l + ((-1)) *d^2*l + ((-2)) *c*h*q + (2) *c*l*q + (2) *h*q*r + ((-2)) *l*q*r + ((-1)) *h*r^2 + (1) *l*r^2 + ((-2)) *d*h*s + (2) *d*l*s + (2) *h*s*t + ((-2)) *l*s*t + ((-1)) *h*t^2 + (1) *l*t^2 ; ((-1)) *c^2*g + ((-1)) *d^2*g + (1) *c^2*j + (1) *d^2*j + (2) *c*g*q + ((-2)) *c*j*q + ((-2)) *g*q*r + (2) *j*q*r + (1) *g*r^2 + ((-1)) *j*r^2 + (2) *d*g*s + ((-2)) *d*j*s + ((-2)) *g*s*t + (2) *j*s*t + (1) *g*t^2 + ((-1)) *j*t^2 ; ((-2)) *c*p + (4) *d*q + ((-4)) *n*q + (4) *n*r + (2) *p*r + (2) *c*t + ((-2)) *r*t ; (2) *d*g + ((-4)) *d*m + (2) *c*n + (2) *c*p + (2) *d*r + ((-2)) *n*r + ((-2)) *p*r + ((-4)) *c*t + ((-2)) *g*t + (4) *m*t + (2) *r*t ; ];
C:=[
[
(1) *d + ((-1)) *t ; ((-2)) *r ; (1) *c + ((-2)) *q + (1) *r ; (1) *d*p + (4) *q*r + ((-2)) *r^2 + ((-2)) *n*s + ((-2)) *p*s + ((-2)) *d*t + (2) *n*t + (1) *p*t + (4) *s*t + ((-2)) *t^2 ; (1) *c*p + (2) *n*q + ((-2)) *n*r + ((-1)) *p*r + ((-2)) *c*t ; (1) *c*n*o + (2) *c^2*p + (2) *d^2*p + (1) *c*m*p + (1) *c*o*p + (1) *d*p^2 + ((-2)) *d*m*q + (2) *m*n*q + ((-2)) *d*o*q + ((-4)) *c*p*q + ((-2)) *m*n*r + (2) *d*o*r + ((-1)) *n*o*r + ((-1)) *m*p*r + ((-1)) *o*p*r + (4) *d*q*r + (4) *p*q*r + ((-2)) *d*r^2 + ((-2)) *p*r^2 + ((-2)) *d*n*s + ((-6)) *d*p*s + ((-2)) *c^2*t + ((-2)) *d^2*t + ((-1)) *c*m*t + (1) *d*n*t + ((-1)) *c*o*t + (1) *d*p*t + ((-1)) *p^2*t + (4) *c*q*t + ((-2)) *c*r*t + (1) *m*r*t + (1) *o*r*t + ((-4)) *q*r*t + (2) *r^2*t + (8) *d*s*t + (4) *p*s*t + ((-4)) *d*t^2 + (1) *n*t^2 + ((-1)) *p*t^2 + ((-4)) *s*t^2 + (2) *t^3 ; ((-2)) *c^2*o + ((-2)) *d^2*o + ((-1)) *d*n*o + ((-1)) *d*m*p + (2) *c*n*p + ((-1)) *d*o*p + (1) *c*p^2 + (2) *n^2*q + (4) *c*o*q + (2) *c^2*r + (2) *d^2*r + ((-1)) *c*m*r + (1) *d*n*r + ((-2)) *n^2*r + ((-1)) *c*o*r + (1) *d*p*r + ((-2)) *n*p*r + ((-1)) *p^2*r + ((-4)) *c*q*r + (2) *m*q*r + ((-2)) *o*q*r + (2) *c*r^2 + ((-1)) *m*r^2 + (1) *o*r^2 + (4) *d*o*s + ((-4)) *d*r*s + (2) *n*r*s + (2) *p*r*s + ((-2)) *c*n*t + (1) *n*o*t + ((-2)) *c*p*t + (1) *m*p*t + (1) *o*p*t + (2) *d*r*t + ((-1)) *n*r*t + ((-1)) *p*r*t + ((-4)) *o*s*t + (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *c^2*l + (2) *d^2*l + ((-2)) *c*n*o + ((-2)) *c^2*p + ((-2)) *d^2*p + ((-2)) *c*o*p + ((-2)) *d*p^2 + ((-4)) *c*l*q + (4) *d*o*q + (4) *c*p*q + ((-4)) *d*o*r + (2) *n*o*r + (2) *o*p*r + ((-4)) *d*q*r + (4) *l*q*r + ((-4)) *p*q*r + (2) *d*r^2 + ((-2)) *l*r^2 + (2) *p*r^2 + ((-4)) *d*l*s + (8) *d*p*s + (4) *c*o*t + (2) *p^2*t + ((-4)) *o*q*t + (4) *q*r*t + ((-2)) *r^2*t + ((-4)) *d*s*t + (4) *l*s*t + ((-8)) *p*s*t + (2) *d*t^2 + ((-2)) *l*t^2 + (2) *p*t^2 + (4) *s*t^2 + ((-2)) *t^3 ; ((-2)) *c^2*j + ((-2)) *d^2*j + (2) *c^2*o + (2) *d^2*o + (2) *d*m*p + ((-2)) *c*n*p + (2) *d*o*p + ((-2)) *c*p^2 + (4) *c*j*q + ((-4)) *c*o*q + ((-4)) *d*p*r + (2) *n*p*r + (2) *p^2*r + ((-4)) *j*q*r + (4) *o*q*r + (2) *j*r^2 + ((-2)) *o*r^2 + (4) *d*j*s + ((-4)) *d*o*s + (4) *c*p*t + ((-2)) *m*p*t + ((-2)) *o*p*t + ((-4)) *j*s*t + (4) *o*s*t + (2) *j*t^2 + ((-2)) *o*t^2 ; (1) *c^2*h + (1) *d^2*h + ((-1)) *c^2*l + ((-1)) *d^2*l + ((-2)) *c*h*q + (2) *c*l*q + (2) *h*q*r + ((-2)) *l*q*r + ((-1)) *h*r^2 + (1) *l*r^2 + ((-2)) *d*h*s + (2) *d*l*s + (2) *h*s*t + ((-2)) *l*s*t + ((-1)) *h*t^2 + (1) *l*t^2 ; ((-1)) *c^2*g + ((-1)) *d^2*g + (1) *c^2*j + (1) *d^2*j + (2) *c*g*q + ((-2)) *c*j*q + ((-2)) *g*q*r + (2) *j*q*r + (1) *g*r^2 + ((-1)) *j*r^2 + (2) *d*g*s + ((-2)) *d*j*s + ((-2)) *g*s*t + (2) *j*s*t + (1) *g*t^2 + ((-1)) *j*t^2 ; ((-2)) *c*p + (4) *d*q + ((-4)) *n*q + (4) *n*r + (2) *p*r + (2) *c*t + ((-2)) *r*t ; (2) *d*g + ((-4)) *d*m + (2) *c*n + (2) *c*p + (2) *d*r + ((-2)) *n*r + ((-2)) *p*r + ((-4)) *c*t + ((-2)) *g*t + (4) *m*t + (2) *r*t ; ];
[
0; 0; (1) *n ; ((-1)) *m + ((-1)) *o ; (1) *n^2 + ((-2)) *m*o ; ((-1)) *m*n ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *m*o ; 0; 0; 0; ((-2)) *c + ((-2)) *j + (4) *o ; 0; ];
[
0; (1) *c ; ((-1)) *d ; ((-1)) *d*m ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *d ; 0; ];
[
(1) *m + (1) *o ; (1) *n ; (1) *m*n ; (1) *n^2 ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *d + ((-2)) *n ; 0; ];
[
0; 0; (1) *c ; 0; 0; ((-1)) ; 0; 0; 0; (1) *d ; 0; ((-1)) *l ; ((-1)) *c + (1) *j ; ((-1)) *d ; 0; 0; 0; ];
[
((-1)) *j ; ((-1)) *d + ((-1)) *l ; 0; 0; 0; ((-1)) ; 0; 0; (1) *c ; 0; (1) *j ; (1) *d + (1) *l ; ((-1)) *c + ((-1)) *g + (1) *j ; ((-1)) *h + (1) *l ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; ];
];
c:=
(-1);
Second certificate
CR:=[
(2) *o + ((-2)) *r ; (2) *b*p + ((-2)) *o*r + (2) *r^2 + ((-2)) *b*t + ((-2)) *p*t + (2) *t^2 ; (2) *a*p + ((-2)) *p*r + ((-2)) *a*t + (2) *o*t ; (2) *a^2*p + (2) *b^2*p + (2) *a*m*p + (2) *a*o*p + (2) *b*p^2 + ((-4)) *a*p*q + ((-2)) *b*o*r + ((-2)) *m*p*r + ((-2)) *o*p*r + (4) *p*q*r + (2) *b*r^2 + ((-2)) *p*r^2 + ((-4)) *b*p*s + ((-2)) *a^2*t + ((-2)) *b^2*t + ((-2)) *a*m*t + (2) *m*o*t + ((-2)) *b*p*t + ((-2)) *p^2*t + (4) *a*q*t + ((-2)) *a*r*t + (2) *o*r*t + ((-4)) *q*r*t + (2) *r^2*t + (4) *b*s*t + (4) *p*s*t + ((-4)) *s*t^2 + (2) *t^3 ; ((-2)) *a^2*o + ((-2)) *b^2*o + ((-2)) *b*n*o + (2) *a*n*p + ((-2)) *b*o*p + (2) *a*p^2 + (2) *a^2*r + (2) *b^2*r + (2) *b*n*r + (2) *a*o*r + ((-2)) *n*p*r + ((-2)) *p^2*r + ((-2)) *a*r^2 + (4) *b*o*s + ((-4)) *a*p*s + ((-4)) *b*r*s + (4) *p*r*s + ((-2)) *a*n*t + (2) *n*o*t + (2) *a*p*t + (2) *o*p*t + (2) *b*r*t + ((-2)) *p*r*t + (4) *a*s*t + ((-4)) *o*s*t + ((-4)) *a*t^2 + (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *a^2*l + (2) *b^2*l + ((-2)) *a^2*p + ((-2)) *b^2*p + ((-4)) *a*o*p + ((-4)) *b*p^2 + ((-4)) *a*l*q + (8) *b*o*q + (4) *a*p*q + ((-4)) *b*o*r + (4) *o*p*r + ((-8)) *b*q*r + (4) *l*q*r + ((-4)) *p*q*r + (4) *b*r^2 + ((-2)) *l*r^2 + (2) *p*r^2 + ((-4)) *b*l*s + (12) *b*p*s + (4) *a*o*t + (4) *p^2*t + ((-8)) *o*q*t + (8) *q*r*t + ((-4)) *r^2*t + ((-8)) *b*s*t + (4) *l*s*t + ((-12)) *p*s*t + (4) *b*t^2 + ((-2)) *l*t^2 + (2) *p*t^2 + (8) *s*t^2 + ((-4)) *t^3 ; ((-2)) *a^2*j + ((-2)) *b^2*j + (2) *a^2*o + (2) *b^2*o + (4) *b*o*p + ((-4)) *a*p^2 + (4) *a*j*q + ((-4)) *a*o*q + ((-4)) *b*p*r + (4) *p^2*r + ((-4)) *j*q*r + (4) *o*q*r + (2) *j*r^2 + ((-2)) *o*r^2 + (4) *b*j*s + ((-4)) *b*o*s + (4) *a*p*t + ((-4)) *o*p*t + ((-4)) *j*s*t + (4) *o*s*t + (2) *j*t^2 + ((-2)) *o*t^2 ; (1) *a^2*h + (1) *b^2*h + ((-1)) *a^2*l + ((-1)) *b^2*l + ((-2)) *a*h*q + (2) *a*l*q + (2) *h*q*r + ((-2)) *l*q*r + ((-1)) *h*r^2 + (1) *l*r^2 + ((-2)) *b*h*s + (2) *b*l*s + (2) *h*s*t + ((-2)) *l*s*t + ((-1)) *h*t^2 + (1) *l*t^2 ; ((-1)) *a^2*g + ((-1)) *b^2*g + (1) *a^2*j + (1) *b^2*j + (2) *a*g*q + ((-2)) *a*j*q + ((-2)) *g*q*r + (2) *j*q*r + (1) *g*r^2 + ((-1)) *j*r^2 + (2) *b*g*s + ((-2)) *b*j*s + ((-2)) *g*s*t + (2) *j*s*t + (1) *g*t^2 + ((-1)) *j*t^2 ; ((-4)) *a*p + (4) *p*r + (4) *a*t + ((-4)) *o*t ; (4) *b*g + (4) *b*j + ((-4)) *a*l + ((-4)) *b*m + (4) *a*p + ((-4)) *b*r + (4) *l*r + ((-4)) *p*r + ((-4)) *g*t + ((-4)) *j*t + (4) *m*t + (4) *r*t ; ];
C:=[
[
(2) *o + ((-2)) *r ; (2) *b*p + ((-2)) *o*r + (2) *r^2 + ((-2)) *b*t + ((-2)) *p*t + (2) *t^2 ; (2) *a*p + ((-2)) *p*r + ((-2)) *a*t + (2) *o*t ; (2) *a^2*p + (2) *b^2*p + (2) *a*m*p + (2) *a*o*p + (2) *b*p^2 + ((-4)) *a*p*q + ((-2)) *b*o*r + ((-2)) *m*p*r + ((-2)) *o*p*r + (4) *p*q*r + (2) *b*r^2 + ((-2)) *p*r^2 + ((-4)) *b*p*s + ((-2)) *a^2*t + ((-2)) *b^2*t + ((-2)) *a*m*t + (2) *m*o*t + ((-2)) *b*p*t + ((-2)) *p^2*t + (4) *a*q*t + ((-2)) *a*r*t + (2) *o*r*t + ((-4)) *q*r*t + (2) *r^2*t + (4) *b*s*t + (4) *p*s*t + ((-4)) *s*t^2 + (2) *t^3 ; ((-2)) *a^2*o + ((-2)) *b^2*o + ((-2)) *b*n*o + (2) *a*n*p + ((-2)) *b*o*p + (2) *a*p^2 + (2) *a^2*r + (2) *b^2*r + (2) *b*n*r + (2) *a*o*r + ((-2)) *n*p*r + ((-2)) *p^2*r + ((-2)) *a*r^2 + (4) *b*o*s + ((-4)) *a*p*s + ((-4)) *b*r*s + (4) *p*r*s + ((-2)) *a*n*t + (2) *n*o*t + (2) *a*p*t + (2) *o*p*t + (2) *b*r*t + ((-2)) *p*r*t + (4) *a*s*t + ((-4)) *o*s*t + ((-4)) *a*t^2 + (2) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; (2) *a^2*l + (2) *b^2*l + ((-2)) *a^2*p + ((-2)) *b^2*p + ((-4)) *a*o*p + ((-4)) *b*p^2 + ((-4)) *a*l*q + (8) *b*o*q + (4) *a*p*q + ((-4)) *b*o*r + (4) *o*p*r + ((-8)) *b*q*r + (4) *l*q*r + ((-4)) *p*q*r + (4) *b*r^2 + ((-2)) *l*r^2 + (2) *p*r^2 + ((-4)) *b*l*s + (12) *b*p*s + (4) *a*o*t + (4) *p^2*t + ((-8)) *o*q*t + (8) *q*r*t + ((-4)) *r^2*t + ((-8)) *b*s*t + (4) *l*s*t + ((-12)) *p*s*t + (4) *b*t^2 + ((-2)) *l*t^2 + (2) *p*t^2 + (8) *s*t^2 + ((-4)) *t^3 ; ((-2)) *a^2*j + ((-2)) *b^2*j + (2) *a^2*o + (2) *b^2*o + (4) *b*o*p + ((-4)) *a*p^2 + (4) *a*j*q + ((-4)) *a*o*q + ((-4)) *b*p*r + (4) *p^2*r + ((-4)) *j*q*r + (4) *o*q*r + (2) *j*r^2 + ((-2)) *o*r^2 + (4) *b*j*s + ((-4)) *b*o*s + (4) *a*p*t + ((-4)) *o*p*t + ((-4)) *j*s*t + (4) *o*s*t + (2) *j*t^2 + ((-2)) *o*t^2 ; (1) *a^2*h + (1) *b^2*h + ((-1)) *a^2*l + ((-1)) *b^2*l + ((-2)) *a*h*q + (2) *a*l*q + (2) *h*q*r + ((-2)) *l*q*r + ((-1)) *h*r^2 + (1) *l*r^2 + ((-2)) *b*h*s + (2) *b*l*s + (2) *h*s*t + ((-2)) *l*s*t + ((-1)) *h*t^2 + (1) *l*t^2 ; ((-1)) *a^2*g + ((-1)) *b^2*g + (1) *a^2*j + (1) *b^2*j + (2) *a*g*q + ((-2)) *a*j*q + ((-2)) *g*q*r + (2) *j*q*r + (1) *g*r^2 + ((-1)) *j*r^2 + (2) *b*g*s + ((-2)) *b*j*s + ((-2)) *g*s*t + (2) *j*s*t + (1) *g*t^2 + ((-1)) *j*t^2 ; ((-4)) *a*p + (4) *p*r + (4) *a*t + ((-4)) *o*t ; (4) *b*g + (4) *b*j + ((-4)) *a*l + ((-4)) *b*m + (4) *a*p + ((-4)) *b*r + (4) *l*r + ((-4)) *p*r + ((-4)) *g*t + ((-4)) *j*t + (4) *m*t + (4) *r*t ; ];
[
(1) *a ; ((-1)) *b ; ((-1)) *b*m ; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; (2) *b ; 0; ];
[
0; ((-1)) *b ; (1) *a ; ((-1)) ; 0; 0; 0; 0; 0; 0; 0; 0; 0; (1) *b + ((-1)) *l ; ((-1)) *a + (1) *j ; 0; 0; ];
[
((-1)) *a + ((-1)) *j ; ((-1)) *b + ((-1)) *l ; 0; ((-1)) ; 0; 0; 0; 0; 0; 0; (2) *j ; (2) *l ; (1) *a + ((-1)) *g ; (1) *b + ((-1)) *h ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; ];
];
c:=
(-1);
Third certificate
CR:=[
(2) *m + ((-2)) *r ; ((-2)) *f*n + ((-2)) *n^2 + (4) *m*q + ((-4)) *q*r + (4) *n*s + (2) *f*t + (2) *n*t + ((-4)) *s*t ; ((-2)) *e*n + (2) *m*n + (2) *e*t + ((-2)) *m*t ; ((-2)) *e*n*o + (2) *m*n*o + ((-2)) *e^2*p + ((-2)) *f^2*p + ((-2)) *e*m*p + ((-2)) *f*n*p + (4) *e*p*q + ((-2)) *f*m*r + (2) *e*n*r + (2) *e*p*r + (2) *m*p*r + ((-4)) *p*q*r + (2) *f*r^2 + ((-2)) *n*r^2 + (4) *f*p*s + (2) *e^2*t + (2) *f^2*t + (2) *e*m*t + (2) *f*n*t + (2) *e*o*t + ((-2)) *m*o*t + (2) *f*p*t + (2) *n*p*t + ((-4)) *e*q*t + ((-4)) *e*r*t + (4) *q*r*t + ((-4)) *f*s*t + ((-4)) *p*s*t + ((-2)) *f*t^2 + ((-2)) *n*t^2 + (4) *s*t^2 ; (2) *e^2*o + (2) *f^2*o + (2) *f*n*o + (2) *n^2*o + (2) *f*m*p + ((-2)) *e*n*p + ((-4)) *e*o*q + ((-4)) *m*o*q + ((-2)) *e^2*r + ((-2)) *f^2*r + ((-2)) *e*m*r + ((-2)) *f*n*r + ((-2)) *f*p*r + (2) *n*p*r + (4) *e*q*r + (8) *o*q*r + (2) *e*r^2 + (2) *m*r^2 + ((-2)) *o*r^2 + ((-4)) *q*r^2 + ((-4)) *f*o*s + ((-4)) *n*o*s + (4) *f*r*s + ((-2)) *f*m*t + (2) *e*n*t + ((-2)) *f*o*t + ((-2)) *n*o*t + (2) *e*p*t + ((-2)) *m*p*t + (4) *f*r*t + (8) *o*s*t + ((-4)) *r*s*t + ((-2)) *e*t^2 + (2) *m*t^2 + ((-2)) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *e^2*l + ((-2)) *f^2*l + (2) *e^2*p + (2) *f^2*p + (4) *e*m*p + (4) *f*n*p + (4) *e*l*q + ((-4)) *e*p*q + ((-4)) *e*p*r + ((-4)) *m*p*r + ((-4)) *l*q*r + (4) *p*q*r + (2) *l*r^2 + (2) *p*r^2 + (4) *f*l*s + ((-4)) *f*p*s + ((-4)) *f*p*t + ((-4)) *n*p*t + ((-4)) *l*s*t + (4) *p*s*t + (2) *l*t^2 + (2) *p*t^2 ; (2) *e^2*j + (2) *f^2*j + ((-2)) *e^2*o + ((-2)) *f^2*o + ((-4)) *f*n*o + ((-4)) *n^2*o + ((-4)) *e*j*q + (4) *e*o*q + (8) *m*o*q + (4) *j*q*r + ((-12)) *o*q*r + ((-2)) *j*r^2 + (2) *o*r^2 + ((-4)) *f*j*s + (4) *f*o*s + (8) *n*o*s + (4) *f*o*t + (4) *n*o*t + (4) *j*s*t + ((-12)) *o*s*t + ((-2)) *j*t^2 + (2) *o*t^2 ; ((-1)) *e^2*h + ((-1)) *f^2*h + (1) *e^2*l + (1) *f^2*l + (2) *e*h*q + ((-2)) *e*l*q + ((-2)) *h*q*r + (2) *l*q*r + (1) *h*r^2 + ((-1)) *l*r^2 + (2) *f*h*s + ((-2)) *f*l*s + ((-2)) *h*s*t + (2) *l*s*t + (1) *h*t^2 + ((-1)) *l*t^2 ; (1) *e^2*g + (1) *f^2*g + ((-1)) *e^2*j + ((-1)) *f^2*j + ((-2)) *e*g*q + (2) *e*j*q + (2) *g*q*r + ((-2)) *j*q*r + ((-1)) *g*r^2 + (1) *j*r^2 + ((-2)) *f*g*s + (2) *f*j*s + (2) *g*s*t + ((-2)) *j*s*t + ((-1)) *g*t^2 + (1) *j*t^2 ; ((-4)) *n*o + (4) *g*p + (4) *o*p + ((-4)) *l*r + ((-4)) *p*r + (4) *j*t ; ((-4)) *e*n + (4) *m*n + (4) *e*t + ((-4)) *m*t ; ];
C:=[
[
(2) *m + ((-2)) *r ; ((-2)) *f*n + ((-2)) *n^2 + (4) *m*q + ((-4)) *q*r + (4) *n*s + (2) *f*t + (2) *n*t + ((-4)) *s*t ; ((-2)) *e*n + (2) *m*n + (2) *e*t + ((-2)) *m*t ; ((-2)) *e*n*o + (2) *m*n*o + ((-2)) *e^2*p + ((-2)) *f^2*p + ((-2)) *e*m*p + ((-2)) *f*n*p + (4) *e*p*q + ((-2)) *f*m*r + (2) *e*n*r + (2) *e*p*r + (2) *m*p*r + ((-4)) *p*q*r + (2) *f*r^2 + ((-2)) *n*r^2 + (4) *f*p*s + (2) *e^2*t + (2) *f^2*t + (2) *e*m*t + (2) *f*n*t + (2) *e*o*t + ((-2)) *m*o*t + (2) *f*p*t + (2) *n*p*t + ((-4)) *e*q*t + ((-4)) *e*r*t + (4) *q*r*t + ((-4)) *f*s*t + ((-4)) *p*s*t + ((-2)) *f*t^2 + ((-2)) *n*t^2 + (4) *s*t^2 ; (2) *e^2*o + (2) *f^2*o + (2) *f*n*o + (2) *n^2*o + (2) *f*m*p + ((-2)) *e*n*p + ((-4)) *e*o*q + ((-4)) *m*o*q + ((-2)) *e^2*r + ((-2)) *f^2*r + ((-2)) *e*m*r + ((-2)) *f*n*r + ((-2)) *f*p*r + (2) *n*p*r + (4) *e*q*r + (8) *o*q*r + (2) *e*r^2 + (2) *m*r^2 + ((-2)) *o*r^2 + ((-4)) *q*r^2 + ((-4)) *f*o*s + ((-4)) *n*o*s + (4) *f*r*s + ((-2)) *f*m*t + (2) *e*n*t + ((-2)) *f*o*t + ((-2)) *n*o*t + (2) *e*p*t + ((-2)) *m*p*t + (4) *f*r*t + (8) *o*s*t + ((-4)) *r*s*t + ((-2)) *e*t^2 + (2) *m*t^2 + ((-2)) *o*t^2 ; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *e^2*l + ((-2)) *f^2*l + (2) *e^2*p + (2) *f^2*p + (4) *e*m*p + (4) *f*n*p + (4) *e*l*q + ((-4)) *e*p*q + ((-4)) *e*p*r + ((-4)) *m*p*r + ((-4)) *l*q*r + (4) *p*q*r + (2) *l*r^2 + (2) *p*r^2 + (4) *f*l*s + ((-4)) *f*p*s + ((-4)) *f*p*t + ((-4)) *n*p*t + ((-4)) *l*s*t + (4) *p*s*t + (2) *l*t^2 + (2) *p*t^2 ; (2) *e^2*j + (2) *f^2*j + ((-2)) *e^2*o + ((-2)) *f^2*o + ((-4)) *f*n*o + ((-4)) *n^2*o + ((-4)) *e*j*q + (4) *e*o*q + (8) *m*o*q + (4) *j*q*r + ((-12)) *o*q*r + ((-2)) *j*r^2 + (2) *o*r^2 + ((-4)) *f*j*s + (4) *f*o*s + (8) *n*o*s + (4) *f*o*t + (4) *n*o*t + (4) *j*s*t + ((-12)) *o*s*t + ((-2)) *j*t^2 + (2) *o*t^2 ; ((-1)) *e^2*h + ((-1)) *f^2*h + (1) *e^2*l + (1) *f^2*l + (2) *e*h*q + ((-2)) *e*l*q + ((-2)) *h*q*r + (2) *l*q*r + (1) *h*r^2 + ((-1)) *l*r^2 + (2) *f*h*s + ((-2)) *f*l*s + ((-2)) *h*s*t + (2) *l*s*t + (1) *h*t^2 + ((-1)) *l*t^2 ; (1) *e^2*g + (1) *f^2*g + ((-1)) *e^2*j + ((-1)) *f^2*j + ((-2)) *e*g*q + (2) *e*j*q + (2) *g*q*r + ((-2)) *j*q*r + ((-1)) *g*r^2 + (1) *j*r^2 + ((-2)) *f*g*s + (2) *f*j*s + (2) *g*s*t + ((-2)) *j*s*t + ((-1)) *g*t^2 + (1) *j*t^2 ; ((-4)) *n*o + (4) *g*p + (4) *o*p + ((-4)) *l*r + ((-4)) *p*r + (4) *j*t ; ((-4)) *e*n + (4) *m*n + (4) *e*t + ((-4)) *m*t ; ];
[
((-1)) *e + ((-1)) *m ; (1) *f + ((-1)) *n ; (1) *f*o + ((-1)) *n*o ; (1) *e*o + (1) *m*o ; 0; 0; 0; 0; 0; 0; 0; 0; 0; ((-2)) *e*o + ((-2)) *m*o ; 0; 0; 0; (2) *f + ((-2)) *n ; ];
[
0; (1) *f ; 0; 0; 0; 0; 0; (1) ; 0; (1) *f ; 0; (1) *l ; ((-1)) *e + ((-1)) *j ; ((-2)) *f + (1) *h ; (1) *e + ((-1)) *g ; 0; 0; ];
[
(1) *e ; 0; 0; 0; 0; 0; 0; (1) ; (1) *e ; 0; ((-1)) *j ; (1) *f + ((-1)) *l ; ((-2)) *e + (1) *j ; ((-1)) *f + (1) *l ; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; 0; ];
[
0; 0; 0; 0; 0; 0; 0; ((-1)) ; 0; (1) ; 0; (1) ; 0; 0; ];
];
c:=
1;