Thales
Geogebra sheet
Coq statement
Lemma Thales: forall O A B C D:point,
collinear O A C -> collinear O B D ->
parallel A B C D ->
(distance2 O B * distance2 O C = distance2 O D * distance2 O A
/\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
\/ collinear O A B.
Proof. geo_begin. tzR. tzR. Qed.
Algebraic version
First goal
p:= (2) *a^2*b^2*c*e + (2) *b^4*c*e + ((-1)) *a^2*b*c^2*e + ((-1)) *b^3*c^2*e + ((-2)) *a^2*b^2*d*e + ((-2)) *b^4*d*e + (1) *a^2*b*d^2*e + (1) *b^3*d^2*e + ((-2)) *a^3*b*e^2 + ((-2)) *a*b^3*e^2 + (4) *a*b^2*d*e^2 + ((-2)) *a*b*d^2*e^2 + (1) *a^2*b*e^3 + (1) *b^3*e^3 + ((-2)) *b^2*d*e^3 + (1) *b*d^2*e^3 + ((-2)) *a^2*b^2*c*f + ((-2)) *b^4*c*f + (1) *a^2*b*c^2*f + (1) *b^3*c^2*f + (2) *a^2*b^2*d*f + (2) *b^4*d*f + ((-1)) *a^2*b*d^2*f + ((-1)) *b^3*d^2*f + (4) *a^3*b*e*f + (4) *a*b^3*e*f + ((-4)) *a*b^2*c*e*f + (2) *a*b*c^2*e*f + ((-4)) *a*b^2*d*e*f + (2) *a*b*d^2*e*f + ((-1)) *a^2*b*e^2*f + ((-1)) *b^3*e^2*f + (2) *b^2*d*e^2*f + ((-1)) *b*d^2*e^2*f + ((-2)) *a^3*b*f^2 + ((-2)) *a*b^3*f^2 + (4) *a*b^2*c*f^2 + ((-2)) *a*b*c^2*f^2 + ((-1)) *a^2*b*e*f^2 + ((-1)) *b^3*e*f^2 + (2) *b^2*c*e*f^2 + ((-1)) *b*c^2*e*f^2 + (1) *a^2*b*f^3 + (1) *b^3*f^3 + ((-2)) *b^2*c*f^3 + (1) *b*c^2*f^3 + (2) *a^3*b*e*g + (2) *a*b^3*e*g + ((-2)) *a^3*b*f*g + ((-2)) *a*b^3*f*g + ((-4)) *a^2*b*e*f*g + (4) *a^2*b*f^2*g + (2) *a*b*e*f^2*g + ((-2)) *a*b*f^3*g + ((-1)) *a^2*b*e*g^2 + ((-1)) *b^3*e*g^2 + (1) *a^2*b*f*g^2 + (1) *b^3*f*g^2 + (2) *a*b*e*f*g^2 + ((-2)) *a*b*f^2*g^2 + ((-1)) *b*e*f^2*g^2 + (1) *b*f^3*g^2 + ((-2)) *a^3*b*e*h + ((-2)) *a*b^3*e*h + (4) *a^2*b*e^2*h + ((-2)) *a*b*e^3*h + (2) *a^3*b*f*h + (2) *a*b^3*f*h + ((-4)) *a^2*b*e*f*h + (2) *a*b*e^2*f*h + (1) *a^2*b*e*h^2 + (1) *b^3*e*h^2 + ((-2)) *a*b*e^2*h^2 + (1) *b*e^3*h^2 + ((-1)) *a^2*b*f*h^2 + ((-1)) *b^3*f*h^2 + (2) *a*b*e*f*h^2 + ((-1)) *b*e^2*f*h^2 + ((-2)) *a^3*b*c*i + ((-2)) *a*b^3*c*i + (1) *a^3*c^2*i + (1) *a*b^2*c^2*i + (2) *a^3*b*d*i + (2) *a*b^3*d*i + ((-1)) *a^3*d^2*i + ((-1)) *a*b^2*d^2*i + (2) *a^4*e*i + ((-2)) *b^4*e*i + ((-4)) *a^2*b*d*e*i + (4) *b^3*d*e*i + (2) *a^2*d^2*e*i + ((-2)) *b^2*d^2*e*i + ((-1)) *a^3*e^2*i + ((-1)) *a*b^2*e^2*i + (2) *a*b*d*e^2*i + ((-1)) *a*d^2*e^2*i + ((-2)) *a^4*f*i + (2) *b^4*f*i + (6) *a^2*b*c*f*i + (2) *b^3*c*f*i + ((-3)) *a^2*c^2*f*i + ((-1)) *b^2*c^2*f*i + ((-2)) *a^2*b*d*f*i + ((-6)) *b^3*d*f*i + (1) *a^2*d^2*f*i + (3) *b^2*d^2*f*i + ((-2)) *a^3*e*f*i + ((-2)) *a*b^2*e*f*i + (4) *a*b*d*e*f*i + ((-2)) *a*d^2*e*f*i + (1) *a^2*e^2*f*i + (1) *b^2*e^2*f*i + ((-2)) *b*d*e^2*f*i + (1) *d^2*e^2*f*i + (3) *a^3*f^2*i + (3) *a*b^2*f^2*i + ((-6)) *a*b*c*f^2*i + (3) *a*c^2*f^2*i + ((-1)) *a^2*f^3*i + ((-1)) *b^2*f^3*i + (2) *b*c*f^3*i + ((-1)) *c^2*f^3*i + ((-2)) *a^4*g*i + ((-2)) *a^2*b^2*g*i + (6) *a^3*f*g*i + (2) *a*b^2*f*g*i + ((-6)) *a^2*f^2*g*i + (2) *a*f^3*g*i + (1) *a^3*g^2*i + (1) *a*b^2*g^2*i + ((-3)) *a^2*f*g^2*i + ((-1)) *b^2*f*g^2*i + (3) *a*f^2*g^2*i + ((-1)) *f^3*g^2*i + (2) *a^4*h*i + (2) *a^2*b^2*h*i + ((-4)) *a^3*e*h*i + (4) *a*b^2*e*h*i + (2) *a^2*e^2*h*i + ((-2)) *a^3*f*h*i + ((-6)) *a*b^2*f*h*i + (4) *a^2*e*f*h*i + ((-2)) *a*e^2*f*h*i + ((-1)) *a^3*h^2*i + ((-1)) *a*b^2*h^2*i + (2) *a^2*e*h^2*i + ((-2)) *b^2*e*h^2*i + ((-1)) *a*e^2*h^2*i + (1) *a^2*f*h^2*i + (3) *b^2*f*h^2*i + ((-2)) *a*e*f*h^2*i + (1) *e^2*f*h^2*i + (2) *a^3*b*i^2 + (2) *a*b^3*i^2 + ((-4)) *a*b^2*d*i^2 + (2) *a*b*d^2*i^2 + (1) *a^2*b*e*i^2 + (1) *b^3*e*i^2 + ((-2)) *b^2*d*e*i^2 + (1) *b*d^2*e*i^2 + ((-3)) *a^2*b*f*i^2 + ((-3)) *b^3*f*i^2 + (6) *b^2*d*f*i^2 + ((-3)) *b*d^2*f*i^2 + ((-4)) *a^2*b*h*i^2 + ((-2)) *a*b*e*h*i^2 + (6) *a*b*f*h*i^2 + (2) *a*b*h^2*i^2 + (1) *b*e*h^2*i^2 + ((-3)) *b*f*h^2*i^2 + ((-1)) *a^3*i^3 + ((-1)) *a*b^2*i^3 + (2) *a*b*d*i^3 + ((-1)) *a*d^2*i^3 + (1) *a^2*f*i^3 + (1) *b^2*f*i^3 + ((-2)) *b*d*f*i^3 + (1) *d^2*f*i^3 + (2) *a^2*h*i^3 + ((-2)) *a*f*h*i^3 + ((-1)) *a*h^2*i^3 + (1) *f*h^2*i^3 + (2) *a^3*b*c*j + (2) *a*b^3*c*j + ((-1)) *a^3*c^2*j + ((-1)) *a*b^2*c^2*j + ((-2)) *a^3*b*d*j + ((-2)) *a*b^3*d*j + (1) *a^3*d^2*j + (1) *a*b^2*d^2*j + ((-2)) *a^4*e*j + (2) *b^4*e*j + ((-2)) *a^2*b*c*e*j + ((-6)) *b^3*c*e*j + (1) *a^2*c^2*e*j + (3) *b^2*c^2*e*j + (6) *a^2*b*d*e*j + (2) *b^3*d*e*j + ((-3)) *a^2*d^2*e*j + ((-1)) *b^2*d^2*e*j + (3) *a^3*e^2*j + (3) *a*b^2*e^2*j + ((-6)) *a*b*d*e^2*j + (3) *a*d^2*e^2*j + ((-1)) *a^2*e^3*j + ((-1)) *b^2*e^3*j + (2) *b*d*e^3*j + ((-1)) *d^2*e^3*j + (2) *a^4*f*j + ((-2)) *b^4*f*j + ((-4)) *a^2*b*c*f*j + (4) *b^3*c*f*j + (2) *a^2*c^2*f*j + ((-2)) *b^2*c^2*f*j + ((-2)) *a^3*e*f*j + ((-2)) *a*b^2*e*f*j + (4) *a*b*c*e*f*j + ((-2)) *a*c^2*e*f*j + ((-1)) *a^3*f^2*j + ((-1)) *a*b^2*f^2*j + (2) *a*b*c*f^2*j + ((-1)) *a*c^2*f^2*j + (1) *a^2*e*f^2*j + (1) *b^2*e*f^2*j + ((-2)) *b*c*e*f^2*j + (1) *c^2*e*f^2*j + (2) *a^4*g*j + (2) *a^2*b^2*g*j + ((-2)) *a^3*e*g*j + ((-6)) *a*b^2*e*g*j + ((-4)) *a^3*f*g*j + (4) *a*b^2*f*g*j + (4) *a^2*e*f*g*j + (2) *a^2*f^2*g*j + ((-2)) *a*e*f^2*g*j + ((-1)) *a^3*g^2*j + ((-1)) *a*b^2*g^2*j + (1) *a^2*e*g^2*j + (3) *b^2*e*g^2*j + (2) *a^2*f*g^2*j + ((-2)) *b^2*f*g^2*j + ((-2)) *a*e*f*g^2*j + ((-1)) *a*f^2*g^2*j + (1) *e*f^2*g^2*j + ((-2)) *a^4*h*j + ((-2)) *a^2*b^2*h*j + (6) *a^3*e*h*j + (2) *a*b^2*e*h*j + ((-6)) *a^2*e^2*h*j + (2) *a*e^3*h*j + (1) *a^3*h^2*j + (1) *a*b^2*h^2*j + ((-3)) *a^2*e*h^2*j + ((-1)) *b^2*e*h^2*j + (3) *a*e^2*h^2*j + ((-1)) *e^3*h^2*j + ((-4)) *a^3*b*i*j + ((-4)) *a*b^3*i*j + (4) *a*b^2*c*i*j + ((-2)) *a*b*c^2*i*j + (4) *a*b^2*d*i*j + ((-2)) *a*b*d^2*i*j + (2) *a^2*b*e*i*j + (2) *b^3*e*i*j + ((-4)) *b^2*d*e*i*j + (2) *b*d^2*e*i*j + (2) *a^2*b*f*i*j + (2) *b^3*f*i*j + ((-4)) *b^2*c*f*i*j + (2) *b*c^2*f*i*j + (4) *a^2*b*g*i*j + ((-4)) *a*b*f*g*i*j + ((-2)) *a*b*g^2*i*j + (2) *b*f*g^2*i*j + (4) *a^2*b*h*i*j + ((-4)) *a*b*e*h*i*j + ((-2)) *a*b*h^2*i*j + (2) *b*e*h^2*i*j + (1) *a^3*i^2*j + (1) *a*b^2*i^2*j + ((-2)) *a*b*d*i^2*j + (1) *a*d^2*i^2*j + ((-1)) *a^2*e*i^2*j + ((-1)) *b^2*e*i^2*j + (2) *b*d*e*i^2*j + ((-1)) *d^2*e*i^2*j + ((-2)) *a^2*h*i^2*j + (2) *a*e*h*i^2*j + (1) *a*h^2*i^2*j + ((-1)) *e*h^2*i^2*j + (2) *a^3*b*j^2 + (2) *a*b^3*j^2 + ((-4)) *a*b^2*c*j^2 + (2) *a*b*c^2*j^2 + ((-3)) *a^2*b*e*j^2 + ((-3)) *b^3*e*j^2 + (6) *b^2*c*e*j^2 + ((-3)) *b*c^2*e*j^2 + (1) *a^2*b*f*j^2 + (1) *b^3*f*j^2 + ((-2)) *b^2*c*f*j^2 + (1) *b*c^2*f*j^2 + ((-4)) *a^2*b*g*j^2 + (6) *a*b*e*g*j^2 + ((-2)) *a*b*f*g*j^2 + (2) *a*b*g^2*j^2 + ((-3)) *b*e*g^2*j^2 + (1) *b*f*g^2*j^2 + (1) *a^3*i*j^2 + (1) *a*b^2*i*j^2 + ((-2)) *a*b*c*i*j^2 + (1) *a*c^2*i*j^2 + ((-1)) *a^2*f*i*j^2 + ((-1)) *b^2*f*i*j^2 + (2) *b*c*f*i*j^2 + ((-1)) *c^2*f*i*j^2 + ((-2)) *a^2*g*i*j^2 + (2) *a*f*g*i*j^2 + (1) *a*g^2*i*j^2 + ((-1)) *f*g^2*i*j^2 + ((-1)) *a^3*j^3 + ((-1)) *a*b^2*j^3 + (2) *a*b*c*j^3 + ((-1)) *a*c^2*j^3 + (1) *a^2*e*j^3 + (1) *b^2*e*j^3 + ((-2)) *b*c*e*j^3 + (1) *c^2*e*j^3 + (2) *a^2*g*j^3 + ((-2)) *a*e*g*j^3 + ((-1)) *a*g^2*j^3 + (1) *e*g^2*j^3
F:= [
((-1)) *c*e + (1) *d*e + (1) *c*f + ((-1)) *d*f + (1) *g*i + ((-1)) *h*i + ((-1)) *g*j + (1) *h*j ;
((-1)) *a*d + ((-1)) *b*f + (1) *d*f + (1) *b*h + (1) *a*j + ((-1)) *h*j ;
((-1)) *a*c + ((-1)) *b*e + (1) *c*e + (1) *b*g + (1) *a*i + ((-1)) *g*i ;
];
Second Goal
p:= (1) *a^2*b*c^2*e + (1) *b^3*c^2*e + ((-2)) *a^2*b*c*d*e + ((-2)) *b^3*c*d*e + (1) *a^2*b*d^2*e + (1) *b^3*d^2*e + ((-2)) *a*b*c^2*e^2 + (4) *a*b*c*d*e^2 + ((-2)) *a*b*d^2*e^2 + ((-1)) *a^2*b*e^3 + ((-1)) *b^3*e^3 + (2) *b^2*c*e^3 + ((-2)) *b*c*d*e^3 + (1) *b*d^2*e^3 + ((-1)) *a^2*b*c^2*f + ((-1)) *b^3*c^2*f + (2) *a^2*b*c*d*f + (2) *b^3*c*d*f + ((-1)) *a^2*b*d^2*f + ((-1)) *b^3*d^2*f + (2) *a*b*c^2*e*f + ((-4)) *a*b*c*d*e*f + (2) *a*b*d^2*e*f + (3) *a^2*b*e^2*f + (3) *b^3*e^2*f + ((-6)) *b^2*c*e^2*f + (2) *b*c^2*e^2*f + (2) *b*c*d*e^2*f + ((-1)) *b*d^2*e^2*f + ((-3)) *a^2*b*e*f^2 + ((-3)) *b^3*e*f^2 + (6) *b^2*c*e*f^2 + ((-3)) *b*c^2*e*f^2 + (1) *a^2*b*f^3 + (1) *b^3*f^3 + ((-2)) *b^2*c*f^3 + (1) *b*c^2*f^3 + (2) *a*b*e^3*g + ((-6)) *a*b*e^2*f*g + (6) *a*b*e*f^2*g + ((-2)) *a*b*f^3*g + (1) *a^2*b*e*g^2 + (1) *b^3*e*g^2 + ((-2)) *a*b*e^2*g^2 + ((-1)) *a^2*b*f*g^2 + ((-1)) *b^3*f*g^2 + (2) *a*b*e*f*g^2 + (2) *b*e^2*f*g^2 + ((-3)) *b*e*f^2*g^2 + (1) *b*f^3*g^2 + ((-2)) *a^2*b*e*g*h + ((-2)) *b^3*e*g*h + (4) *a*b*e^2*g*h + ((-2)) *b*e^3*g*h + (2) *a^2*b*f*g*h + (2) *b^3*f*g*h + ((-4)) *a*b*e*f*g*h + (2) *b*e^2*f*g*h + (1) *a^2*b*e*h^2 + (1) *b^3*e*h^2 + ((-2)) *a*b*e^2*h^2 + (1) *b*e^3*h^2 + ((-1)) *a^2*b*f*h^2 + ((-1)) *b^3*f*h^2 + (2) *a*b*e*f*h^2 + ((-1)) *b*e^2*f*h^2 + ((-1)) *a^3*c^2*i + ((-1)) *a*b^2*c^2*i + (2) *a^3*c*d*i + (2) *a*b^2*c*d*i + ((-1)) *a^3*d^2*i + ((-1)) *a*b^2*d^2*i + (2) *a^2*c^2*e*i + ((-2)) *b^2*c^2*e*i + ((-4)) *a^2*c*d*e*i + (4) *b^2*c*d*e*i + (2) *a^2*d^2*e*i + ((-2)) *b^2*d^2*e*i + (1) *a^3*e^2*i + (1) *a*b^2*e^2*i + ((-2)) *a*b*c*e^2*i + (2) *a*c*d*e^2*i + ((-1)) *a*d^2*e^2*i + (1) *a^2*c^2*f*i + (3) *b^2*c^2*f*i + ((-2)) *a^2*c*d*f*i + ((-6)) *b^2*c*d*f*i + (1) *a^2*d^2*f*i + (3) *b^2*d^2*f*i + ((-2)) *a^3*e*f*i + ((-2)) *a*b^2*e*f*i + (4) *a*b*c*e*f*i + ((-4)) *a*c^2*e*f*i + (4) *a*c*d*e*f*i + ((-2)) *a*d^2*e*f*i + ((-1)) *a^2*e^2*f*i + ((-1)) *b^2*e^2*f*i + (2) *b*c*e^2*f*i + ((-2)) *c*d*e^2*f*i + (1) *d^2*e^2*f*i + (1) *a^3*f^2*i + (1) *a*b^2*f^2*i + ((-2)) *a*b*c*f^2*i + (1) *a*c^2*f^2*i + (2) *a^2*e*f^2*i + (2) *b^2*e*f^2*i + ((-4)) *b*c*e*f^2*i + (2) *c^2*e*f^2*i + ((-1)) *a^2*f^3*i + ((-1)) *b^2*f^3*i + (2) *b*c*f^3*i + ((-1)) *c^2*f^3*i + ((-2)) *a^2*e^2*g*i + (4) *a^2*e*f*g*i + (2) *a*e^2*f*g*i + ((-2)) *a^2*f^2*g*i + ((-4)) *a*e*f^2*g*i + (2) *a*f^3*g*i + ((-1)) *a^3*g^2*i + ((-1)) *a*b^2*g^2*i + (2) *a^2*e*g^2*i + ((-2)) *b^2*e*g^2*i + (1) *a^2*f*g^2*i + (3) *b^2*f*g^2*i + ((-4)) *a*e*f*g^2*i + (1) *a*f^2*g^2*i + (2) *e*f^2*g^2*i + ((-1)) *f^3*g^2*i + (2) *a^3*g*h*i + (2) *a*b^2*g*h*i + ((-4)) *a^2*e*g*h*i + (4) *b^2*e*g*h*i + (2) *a*e^2*g*h*i + ((-2)) *a^2*f*g*h*i + ((-6)) *b^2*f*g*h*i + (4) *a*e*f*g*h*i + ((-2)) *e^2*f*g*h*i + ((-1)) *a^3*h^2*i + ((-1)) *a*b^2*h^2*i + (2) *a^2*e*h^2*i + ((-2)) *b^2*e*h^2*i + ((-1)) *a*e^2*h^2*i + (1) *a^2*f*h^2*i + (3) *b^2*f*h^2*i + ((-2)) *a*e*f*h^2*i + (1) *e^2*f*h^2*i + (2) *a*b*c^2*i^2 + ((-4)) *a*b*c*d*i^2 + (2) *a*b*d^2*i^2 + ((-1)) *a^2*b*e*i^2 + ((-1)) *b^3*e*i^2 + (2) *b^2*c*e*i^2 + ((-2)) *b*c*d*e*i^2 + (1) *b*d^2*e*i^2 + (1) *a^2*b*f*i^2 + (1) *b^3*f*i^2 + ((-2)) *b^2*c*f*i^2 + ((-2)) *b*c^2*f*i^2 + (6) *b*c*d*f*i^2 + ((-3)) *b*d^2*f*i^2 + (2) *a*b*e*g*i^2 + ((-2)) *a*b*f*g*i^2 + (2) *a*b*g^2*i^2 + ((-2)) *b*f*g^2*i^2 + ((-4)) *a*b*g*h*i^2 + ((-2)) *b*e*g*h*i^2 + (6) *b*f*g*h*i^2 + (2) *a*b*h^2*i^2 + (1) *b*e*h^2*i^2 + ((-3)) *b*f*h^2*i^2 + (1) *a^3*i^3 + (1) *a*b^2*i^3 + ((-2)) *a*b*c*i^3 + (2) *a*c*d*i^3 + ((-1)) *a*d^2*i^3 + ((-1)) *a^2*f*i^3 + ((-1)) *b^2*f*i^3 + (2) *b*c*f*i^3 + ((-2)) *c*d*f*i^3 + (1) *d^2*f*i^3 + ((-2)) *a^2*g*i^3 + (2) *a*f*g*i^3 + (2) *a*g*h*i^3 + ((-2)) *f*g*h*i^3 + ((-1)) *a*h^2*i^3 + (1) *f*h^2*i^3 + (1) *a^3*c^2*j + (1) *a*b^2*c^2*j + ((-2)) *a^3*c*d*j + ((-2)) *a*b^2*c*d*j + (1) *a^3*d^2*j + (1) *a*b^2*d^2*j + ((-3)) *a^2*c^2*e*j + ((-1)) *b^2*c^2*e*j + (6) *a^2*c*d*e*j + (2) *b^2*c*d*e*j + ((-3)) *a^2*d^2*e*j + ((-1)) *b^2*d^2*e*j + ((-1)) *a^3*e^2*j + ((-1)) *a*b^2*e^2*j + (2) *a*b*c*e^2*j + (2) *a*c^2*e^2*j + ((-6)) *a*c*d*e^2*j + (3) *a*d^2*e^2*j + (1) *a^2*e^3*j + (1) *b^2*e^3*j + ((-2)) *b*c*e^3*j + (2) *c*d*e^3*j + ((-1)) *d^2*e^3*j + (2) *a^3*e*f*j + (2) *a*b^2*e*f*j + ((-4)) *a*b*c*e*f*j + (2) *a*c^2*e*f*j + ((-2)) *a^2*e^2*f*j + ((-2)) *b^2*e^2*f*j + (4) *b*c*e^2*f*j + ((-2)) *c^2*e^2*f*j + ((-1)) *a^3*f^2*j + ((-1)) *a*b^2*f^2*j + (2) *a*b*c*f^2*j + ((-1)) *a*c^2*f^2*j + (1) *a^2*e*f^2*j + (1) *b^2*e*f^2*j + ((-2)) *b*c*e*f^2*j + (1) *c^2*e*f^2*j + (2) *a^2*e^2*g*j + ((-2)) *a*e^3*g*j + ((-4)) *a^2*e*f*g*j + (4) *a*e^2*f*g*j + (2) *a^2*f^2*g*j + ((-2)) *a*e*f^2*g*j + (1) *a^3*g^2*j + (1) *a*b^2*g^2*j + ((-3)) *a^2*e*g^2*j + ((-1)) *b^2*e*g^2*j + (2) *a*e^2*g^2*j + (2) *a*e*f*g^2*j + ((-2)) *e^2*f*g^2*j + ((-1)) *a*f^2*g^2*j + (1) *e*f^2*g^2*j + ((-2)) *a^3*g*h*j + ((-2)) *a*b^2*g*h*j + (6) *a^2*e*g*h*j + (2) *b^2*e*g*h*j + ((-6)) *a*e^2*g*h*j + (2) *e^3*g*h*j + (1) *a^3*h^2*j + (1) *a*b^2*h^2*j + ((-3)) *a^2*e*h^2*j + ((-1)) *b^2*e*h^2*j + (3) *a*e^2*h^2*j + ((-1)) *e^3*h^2*j + ((-2)) *a*b*c^2*i*j + (4) *a*b*c*d*i*j + ((-2)) *a*b*d^2*i*j + (2) *a^2*b*e*i*j + (2) *b^3*e*i*j + ((-4)) *b^2*c*e*i*j + (4) *b*c^2*e*i*j + ((-4)) *b*c*d*e*i*j + (2) *b*d^2*e*i*j + ((-2)) *a^2*b*f*i*j + ((-2)) *b^3*f*i*j + (4) *b^2*c*f*i*j + ((-2)) *b*c^2*f*i*j + ((-4)) *a*b*e*g*i*j + (4) *a*b*f*g*i*j + ((-2)) *a*b*g^2*i*j + (4) *b*e*g^2*i*j + ((-2)) *b*f*g^2*i*j + (4) *a*b*g*h*i*j + ((-4)) *b*e*g*h*i*j + ((-2)) *a*b*h^2*i*j + (2) *b*e*h^2*i*j + ((-3)) *a^3*i^2*j + ((-3)) *a*b^2*i^2*j + (6) *a*b*c*i^2*j + ((-2)) *a*c^2*i^2*j + ((-2)) *a*c*d*i^2*j + (1) *a*d^2*i^2*j + (1) *a^2*e*i^2*j + (1) *b^2*e*i^2*j + ((-2)) *b*c*e*i^2*j + (2) *c*d*e*i^2*j + ((-1)) *d^2*e*i^2*j + (2) *a^2*f*i^2*j + (2) *b^2*f*i^2*j + ((-4)) *b*c*f*i^2*j + (2) *c^2*f*i^2*j + (6) *a^2*g*i^2*j + ((-2)) *a*e*g*i^2*j + ((-4)) *a*f*g*i^2*j + ((-2)) *a*g^2*i^2*j + (2) *f*g^2*i^2*j + ((-2)) *a*g*h*i^2*j + (2) *e*g*h*i^2*j + (1) *a*h^2*i^2*j + ((-1)) *e*h^2*i^2*j + ((-1)) *a^2*b*e*j^2 + ((-1)) *b^3*e*j^2 + (2) *b^2*c*e*j^2 + ((-1)) *b*c^2*e*j^2 + (1) *a^2*b*f*j^2 + (1) *b^3*f*j^2 + ((-2)) *b^2*c*f*j^2 + (1) *b*c^2*f*j^2 + (2) *a*b*e*g*j^2 + ((-2)) *a*b*f*g*j^2 + ((-1)) *b*e*g^2*j^2 + (1) *b*f*g^2*j^2 + (3) *a^3*i*j^2 + (3) *a*b^2*i*j^2 + ((-6)) *a*b*c*i*j^2 + (3) *a*c^2*i*j^2 + ((-2)) *a^2*e*i*j^2 + ((-2)) *b^2*e*i*j^2 + (4) *b*c*e*i*j^2 + ((-2)) *c^2*e*i*j^2 + ((-1)) *a^2*f*i*j^2 + ((-1)) *b^2*f*i*j^2 + (2) *b*c*f*i*j^2 + ((-1)) *c^2*f*i*j^2 + ((-6)) *a^2*g*i*j^2 + (4) *a*e*g*i*j^2 + (2) *a*f*g*i*j^2 + (3) *a*g^2*i*j^2 + ((-2)) *e*g^2*i*j^2 + ((-1)) *f*g^2*i*j^2 + ((-1)) *a^3*j^3 + ((-1)) *a*b^2*j^3 + (2) *a*b*c*j^3 + ((-1)) *a*c^2*j^3 + (1) *a^2*e*j^3 + (1) *b^2*e*j^3 + ((-2)) *b*c*e*j^3 + (1) *c^2*e*j^3 + (2) *a^2*g*j^3 + ((-2)) *a*e*g*j^3 + ((-1)) *a*g^2*j^3 + (1) *e*g^2*j^3
F:= [
((-1)) *c*e + (1) *d*e + (1) *c*f + ((-1)) *d*f + (1) *g*i + ((-1)) *h*i + ((-1)) *g*j + (1) *h*j ;
((-1)) *a*d + ((-1)) *b*f + (1) *d*f + (1) *b*h + (1) *a*j + ((-1)) *h*j ;
((-1)) *a*c + ((-1)) *b*e + (1) *c*e + (1) *b*g + (1) *a*i + ((-1)) *g*i ;
];
Certificates
First certificate:
CR:=[
((-1)) *b*f^2 + (1) *b^2*i + ((-1)) *b*i^2 + ((-1)) *b^2*j + (1) *f^2*j + (1) *i^2*j + (1) *b*j^2 + ((-1)) *i*j^2 ; (2) *a^3 + (2) *a*b^2 + ((-1)) *a^2*e + ((-1)) *b^2*e + (1) *b*d*e + ((-2)) *a^2*f + (2) *b^2*f + ((-2)) *b*d*f + (1) *a*e*f + ((-1)) *a^2*g + ((-1)) *b^2*g + (2) *a*f*g + ((-1)) *f^2*g + ((-1)) *a^2*h + ((-1)) *b^2*h + (1) *a*e*h + ((-1)) *e*f*h + (1) *f^2*h + ((-4)) *a*b*j + (1) *b*e*j + ((-1)) *d*e*j + ((-2)) *b*f*j + (2) *d*f*j + (2) *b*g*j + (2) *b*h*j + (2) *a*j^2 + ((-1)) *g*j^2 + ((-1)) *h*j^2 ; (2) *a^3*f + (2) *a*b^2*f + ((-3)) *a^2*f^2 + (1) *b^2*f^2 + (1) *a*f^3 + ((-1)) *a^2*f*g + ((-1)) *b^2*f*g + (2) *a*f^2*g + ((-1)) *f^3*g + ((-1)) *a^2*f*h + ((-1)) *b^2*f*h + (1) *a*f^2*h + ((-2)) *a^2*b*i + ((-2)) *b^3*i + (1) *a^2*c*i + (1) *b^2*c*i + (3) *a*b*f*i + ((-2)) *a*c*f*i + ((-1)) *b*f^2*i + (1) *c*f^2*i + (1) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-1)) *a*f*i^2 + ((-1)) *a*h*i^2 + (1) *f*h*i^2 + (2) *a^2*b*j + (2) *b^3*j + ((-1)) *a^2*c*j + ((-1)) *b^2*c*j + ((-7)) *a*b*f*j + (2) *a*c*f*j + ((-1)) *c*f^2*j + (2) *b*f*g*j + ((-1)) *a*b*h*j + (3) *b*f*h*j + ((-1)) *a^2*i*j + (2) *b^2*i*j + ((-2)) *b*c*i*j + (1) *a*f*i*j + (1) *a*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + ((-3)) *b^2*j^2 + (2) *b*c*j^2 + (2) *a*f*j^2 + ((-1)) *f*g*j^2 + ((-1)) *f*h*j^2 + (1) *c*i*j^2 + (1) *b*j^3 + ((-1)) *c*j^3 ; ((-2)) *a^2*e^2 + (2) *b^2*e^2 + ((-2)) *b*d*e^2 + (1) *a*e^3 + ((-2)) *a^3*f + ((-2)) *a*b^2*f + (4) *a^2*e*f + ((-4)) *b^2*e*f + (4) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + (1) *b^2*f^2 + ((-1)) *b*c*f^2 + ((-1)) *b*d*f^2 + ((-1)) *a*e*f^2 + (1) *a*e^2*g + (1) *a^2*f*g + (1) *b^2*f*g + ((-2)) *a*e*f*g + ((-1)) *e^2*f*g + ((-1)) *a*f^2*g + (2) *e*f^2*g + (1) *a*e^2*h + ((-1)) *e^3*h + (1) *a^2*f*h + (1) *b^2*f*h + ((-2)) *a*e*f*h + (2) *e^2*f*h + ((-1)) *e*f^2*h + (2) *a^2*b*i + (2) *b^3*i + ((-1)) *a^2*d*i + ((-1)) *b^2*d*i + ((-7)) *a*b*e*i + (3) *a*d*e*i + (1) *b*e^2*i + ((-1)) *d*e^2*i + (4) *a*b*f*i + ((-1)) *a*d*f*i + (1) *b*e*f*i + ((-1)) *d*e*f*i + ((-1)) *b*f^2*i + (1) *d*f^2*i + ((-1)) *a*b*g*i + (1) *b*e*g*i + (3) *b*e*h*i + ((-3)) *b*f*h*i + ((-3)) *b^2*i^2 + (2) *b*d*i^2 + (1) *a*e*i^2 + ((-1)) *a*f*i^2 + (1) *a*g*i^2 + ((-1)) *f*g*i^2 + ((-1)) *a*h*i^2 + ((-1)) *e*h*i^2 + (2) *f*h*i^2 + (1) *b*i^3 + ((-1)) *d*i^3 + ((-2)) *a^2*b*j + ((-2)) *b^3*j + (1) *a^2*d*j + (1) *b^2*d*j + (7) *a*b*e*j + ((-3)) *a*d*e*j + ((-3)) *b*e^2*j + (3) *d*e^2*j + (1) *a*d*f*j + (3) *b*e*f*j + ((-3)) *d*e*f*j + (1) *c*f^2*j + (1) *a*b*g*j + ((-1)) *b*e*g*j + ((-2)) *b*f*g*j + ((-3)) *b*e*h*j + (1) *b*f*h*j + ((-1)) *a^2*i*j + (2) *b^2*i*j + ((-2)) *b*d*i*j + (2) *a*e*i*j + ((-1)) *a*f*i*j + ((-1)) *a*g*i*j + ((-1)) *e*g*i*j + (2) *f*g*i*j + (2) *a*h*i*j + ((-1)) *e*h*i*j + ((-1)) *f*h*i*j + (1) *d*i^2*j + (1) *a^2*j^2 + (1) *b^2*j^2 + ((-3)) *a*e*j^2 + (1) *e*g*j^2 + ((-1)) *a*h*j^2 + (2) *e*h*j^2 + ((-1)) *b*i*j^2 ; (2) *a^2*b^2 + (2) *b^4 + ((-1)) *a^2*b*c + ((-1)) *b^3*c + ((-1)) *a^2*b*d + ((-1)) *b^3*d + ((-2)) *a^3*e + ((-2)) *a*b^2*e + (1) *a^2*e^2 + (1) *b^2*e^2 + ((-1)) *b*d*e^2 + ((-1)) *a^3*f + ((-5)) *a*b^2*f + (2) *a*b*c*f + (3) *a*b*d*f + (3) *a^2*e*f + ((-1)) *b^2*e*f + (1) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + (2) *b^2*f^2 + ((-1)) *b*c*f^2 + ((-1)) *b*d*f^2 + ((-1)) *a*e*f^2 + (1) *a^2*e*g + (1) *b^2*e*g + ((-2)) *a*e*f*g + (1) *e*f^2*g + (1) *a^2*e*h + (1) *b^2*e*h + ((-1)) *a*e^2*h + (1) *a^2*f*h + ((-1)) *a*e*f*h + (1) *e^2*f*h + ((-1)) *a*f^2*h + ((-3)) *a^2*b*i + ((-3)) *b^3*i + (1) *a^2*c*i + (1) *b^2*c*i + (1) *a^2*d*i + (2) *b^2*d*i + (5) *a*b*f*i + ((-2)) *a*c*f*i + ((-2)) *a*d*f*i + ((-2)) *b*f^2*i + (1) *c*f^2*i + (1) *d*f^2*i + (1) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-1)) *b*d*i^2 + ((-1)) *a*f*i^2 + ((-1)) *a*h*i^2 + (1) *f*h*i^2 + (1) *a^2*b*j + ((-3)) *b^3*j + (2) *b^2*c*j + (1) *b^2*d*j + (4) *a*b*e*j + ((-1)) *b*e^2*j + (1) *d*e^2*j + ((-1)) *a*d*f*j + (1) *b*e*f*j + ((-1)) *d*e*f*j + ((-2)) *b*e*g*j + ((-1)) *a*b*h*j + ((-2)) *b*e*h*j + (1) *b*f*h*j + ((-1)) *a^2*i*j + (4) *b^2*i*j + ((-2)) *b*c*i*j + ((-2)) *b*d*i*j + (1) *a*f*i*j + (1) *a*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + (1) *d*i^2*j + (1) *b^2*j^2 + ((-1)) *b*c*j^2 + ((-2)) *a*e*j^2 + (1) *e*g*j^2 + (1) *e*h*j^2 + ((-1)) *b*i*j^2 + (1) *c*i*j^2 ; ];
C:=[
[
((-1)) *b*f^2 + (1) *b^2*i + ((-1)) *b*i^2 + ((-1)) *b^2*j + (1) *f^2*j + (1) *i^2*j + (1) *b*j^2 + ((-1)) *i*j^2 ; (2) *a^3 + (2) *a*b^2 + ((-1)) *a^2*e + ((-1)) *b^2*e + (1) *b*d*e + ((-2)) *a^2*f + (2) *b^2*f + ((-2)) *b*d*f + (1) *a*e*f + ((-1)) *a^2*g + ((-1)) *b^2*g + (2) *a*f*g + ((-1)) *f^2*g + ((-1)) *a^2*h + ((-1)) *b^2*h + (1) *a*e*h + ((-1)) *e*f*h + (1) *f^2*h + ((-4)) *a*b*j + (1) *b*e*j + ((-1)) *d*e*j + ((-2)) *b*f*j + (2) *d*f*j + (2) *b*g*j + (2) *b*h*j + (2) *a*j^2 + ((-1)) *g*j^2 + ((-1)) *h*j^2 ; (2) *a^3*f + (2) *a*b^2*f + ((-3)) *a^2*f^2 + (1) *b^2*f^2 + (1) *a*f^3 + ((-1)) *a^2*f*g + ((-1)) *b^2*f*g + (2) *a*f^2*g + ((-1)) *f^3*g + ((-1)) *a^2*f*h + ((-1)) *b^2*f*h + (1) *a*f^2*h + ((-2)) *a^2*b*i + ((-2)) *b^3*i + (1) *a^2*c*i + (1) *b^2*c*i + (3) *a*b*f*i + ((-2)) *a*c*f*i + ((-1)) *b*f^2*i + (1) *c*f^2*i + (1) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-1)) *a*f*i^2 + ((-1)) *a*h*i^2 + (1) *f*h*i^2 + (2) *a^2*b*j + (2) *b^3*j + ((-1)) *a^2*c*j + ((-1)) *b^2*c*j + ((-7)) *a*b*f*j + (2) *a*c*f*j + ((-1)) *c*f^2*j + (2) *b*f*g*j + ((-1)) *a*b*h*j + (3) *b*f*h*j + ((-1)) *a^2*i*j + (2) *b^2*i*j + ((-2)) *b*c*i*j + (1) *a*f*i*j + (1) *a*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + ((-3)) *b^2*j^2 + (2) *b*c*j^2 + (2) *a*f*j^2 + ((-1)) *f*g*j^2 + ((-1)) *f*h*j^2 + (1) *c*i*j^2 + (1) *b*j^3 + ((-1)) *c*j^3 ; ((-2)) *a^2*e^2 + (2) *b^2*e^2 + ((-2)) *b*d*e^2 + (1) *a*e^3 + ((-2)) *a^3*f + ((-2)) *a*b^2*f + (4) *a^2*e*f + ((-4)) *b^2*e*f + (4) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + (1) *b^2*f^2 + ((-1)) *b*c*f^2 + ((-1)) *b*d*f^2 + ((-1)) *a*e*f^2 + (1) *a*e^2*g + (1) *a^2*f*g + (1) *b^2*f*g + ((-2)) *a*e*f*g + ((-1)) *e^2*f*g + ((-1)) *a*f^2*g + (2) *e*f^2*g + (1) *a*e^2*h + ((-1)) *e^3*h + (1) *a^2*f*h + (1) *b^2*f*h + ((-2)) *a*e*f*h + (2) *e^2*f*h + ((-1)) *e*f^2*h + (2) *a^2*b*i + (2) *b^3*i + ((-1)) *a^2*d*i + ((-1)) *b^2*d*i + ((-7)) *a*b*e*i + (3) *a*d*e*i + (1) *b*e^2*i + ((-1)) *d*e^2*i + (4) *a*b*f*i + ((-1)) *a*d*f*i + (1) *b*e*f*i + ((-1)) *d*e*f*i + ((-1)) *b*f^2*i + (1) *d*f^2*i + ((-1)) *a*b*g*i + (1) *b*e*g*i + (3) *b*e*h*i + ((-3)) *b*f*h*i + ((-3)) *b^2*i^2 + (2) *b*d*i^2 + (1) *a*e*i^2 + ((-1)) *a*f*i^2 + (1) *a*g*i^2 + ((-1)) *f*g*i^2 + ((-1)) *a*h*i^2 + ((-1)) *e*h*i^2 + (2) *f*h*i^2 + (1) *b*i^3 + ((-1)) *d*i^3 + ((-2)) *a^2*b*j + ((-2)) *b^3*j + (1) *a^2*d*j + (1) *b^2*d*j + (7) *a*b*e*j + ((-3)) *a*d*e*j + ((-3)) *b*e^2*j + (3) *d*e^2*j + (1) *a*d*f*j + (3) *b*e*f*j + ((-3)) *d*e*f*j + (1) *c*f^2*j + (1) *a*b*g*j + ((-1)) *b*e*g*j + ((-2)) *b*f*g*j + ((-3)) *b*e*h*j + (1) *b*f*h*j + ((-1)) *a^2*i*j + (2) *b^2*i*j + ((-2)) *b*d*i*j + (2) *a*e*i*j + ((-1)) *a*f*i*j + ((-1)) *a*g*i*j + ((-1)) *e*g*i*j + (2) *f*g*i*j + (2) *a*h*i*j + ((-1)) *e*h*i*j + ((-1)) *f*h*i*j + (1) *d*i^2*j + (1) *a^2*j^2 + (1) *b^2*j^2 + ((-3)) *a*e*j^2 + (1) *e*g*j^2 + ((-1)) *a*h*j^2 + (2) *e*h*j^2 + ((-1)) *b*i*j^2 ; (2) *a^2*b^2 + (2) *b^4 + ((-1)) *a^2*b*c + ((-1)) *b^3*c + ((-1)) *a^2*b*d + ((-1)) *b^3*d + ((-2)) *a^3*e + ((-2)) *a*b^2*e + (1) *a^2*e^2 + (1) *b^2*e^2 + ((-1)) *b*d*e^2 + ((-1)) *a^3*f + ((-5)) *a*b^2*f + (2) *a*b*c*f + (3) *a*b*d*f + (3) *a^2*e*f + ((-1)) *b^2*e*f + (1) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + (2) *b^2*f^2 + ((-1)) *b*c*f^2 + ((-1)) *b*d*f^2 + ((-1)) *a*e*f^2 + (1) *a^2*e*g + (1) *b^2*e*g + ((-2)) *a*e*f*g + (1) *e*f^2*g + (1) *a^2*e*h + (1) *b^2*e*h + ((-1)) *a*e^2*h + (1) *a^2*f*h + ((-1)) *a*e*f*h + (1) *e^2*f*h + ((-1)) *a*f^2*h + ((-3)) *a^2*b*i + ((-3)) *b^3*i + (1) *a^2*c*i + (1) *b^2*c*i + (1) *a^2*d*i + (2) *b^2*d*i + (5) *a*b*f*i + ((-2)) *a*c*f*i + ((-2)) *a*d*f*i + ((-2)) *b*f^2*i + (1) *c*f^2*i + (1) *d*f^2*i + (1) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-1)) *b*d*i^2 + ((-1)) *a*f*i^2 + ((-1)) *a*h*i^2 + (1) *f*h*i^2 + (1) *a^2*b*j + ((-3)) *b^3*j + (2) *b^2*c*j + (1) *b^2*d*j + (4) *a*b*e*j + ((-1)) *b*e^2*j + (1) *d*e^2*j + ((-1)) *a*d*f*j + (1) *b*e*f*j + ((-1)) *d*e*f*j + ((-2)) *b*e*g*j + ((-1)) *a*b*h*j + ((-2)) *b*e*h*j + (1) *b*f*h*j + ((-1)) *a^2*i*j + (4) *b^2*i*j + ((-2)) *b*c*i*j + ((-2)) *b*d*i*j + (1) *a*f*i*j + (1) *a*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + (1) *d*i^2*j + (1) *b^2*j^2 + ((-1)) *b*c*j^2 + ((-2)) *a*e*j^2 + (1) *e*g*j^2 + (1) *e*h*j^2 + ((-1)) *b*i*j^2 + (1) *c*i*j^2 ; ];
[
0; (1) *d ; ((-1)) *c ; 0; ];
[
((-1)) *e ; (1) *e ; (1) *a ; ];
];
c:=
(-1);
Second certificate
CR:=[
((-1)) *b*f^2 + ((-1)) *b^2*i + (1) *b*i^2 + (1) *b^2*j + (1) *f^2*j + ((-1)) *i^2*j + ((-1)) *b*j^2 + (1) *i*j^2 ; ((-1)) *a^2*e + ((-1)) *b^2*e + (1) *b*d*e + (2) *a^2*f + (2) *b^2*f + ((-2)) *b*d*f + (1) *a*e*f + ((-2)) *a*f^2 + ((-1)) *a^2*g + ((-1)) *b^2*g + (2) *a*e*g + ((-2)) *a*f*g + ((-2)) *e*f*g + (3) *f^2*g + (1) *a^2*h + (1) *b^2*h + ((-1)) *a*e*h + (1) *e*f*h + ((-1)) *f^2*h + (2) *b*g*i + ((-2)) *b*h*i + (1) *b*e*j + ((-1)) *d*e*j + ((-2)) *b*f*j + (2) *d*f*j + ((-2)) *g*i*j + (2) *h*i*j + (1) *g*j^2 + ((-1)) *h*j^2 ; (1) *a^2*f^2 + (1) *b^2*f^2 + ((-1)) *a*f^3 + ((-1)) *a^2*f*g + ((-1)) *b^2*f*g + (1) *f^3*g + (1) *a^2*f*h + (1) *b^2*f*h + ((-1)) *a*f^2*h + (1) *a^2*c*i + (1) *b^2*c*i + (1) *a*b*f*i + ((-2)) *a*c*f*i + ((-1)) *b*f^2*i + (1) *c*f^2*i + (2) *b*f*g*i + ((-1)) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-2)) *b*c*i^2 + ((-1)) *a*f*i^2 + ((-2)) *a*g*i^2 + (2) *f*g*i^2 + (1) *a*h*i^2 + ((-1)) *f*h*i^2 + ((-1)) *a^2*c*j + ((-1)) *b^2*c*j + ((-1)) *a*b*f*j + (2) *a*c*f*j + ((-1)) *c*f^2*j + (1) *a*b*h*j + ((-1)) *b*f*h*j + ((-3)) *a^2*i*j + ((-2)) *b^2*i*j + (2) *b*c*i*j + (3) *a*f*i*j + (4) *a*g*i*j + ((-6)) *f*g*i*j + ((-1)) *a*h*i*j + (3) *f*h*i*j + ((-1)) *b*i^2*j + (2) *c*i^2*j + (2) *a^2*j^2 + (1) *b^2*j^2 + ((-2)) *a*f*j^2 + ((-2)) *a*g*j^2 + (3) *f*g*j^2 + ((-1)) *f*h*j^2 + (2) *b*i*j^2 + ((-3)) *c*i*j^2 + ((-1)) *b*j^3 + (1) *c*j^3 ; (1) *a*e^3 + ((-3)) *a*e^2*f + ((-1)) *a^2*f^2 + ((-1)) *b^2*f^2 + ((-1)) *b*c*f^2 + (1) *b*d*f^2 + (3) *a*e*f^2 + (1) *a*e^2*g + ((-2)) *e^3*g + (1) *a^2*f*g + (1) *b^2*f*g + ((-2)) *a*e*f*g + (5) *e^2*f*g + (1) *a*f^2*g + ((-4)) *e*f^2*g + ((-1)) *a*e^2*h + (1) *e^3*h + ((-1)) *a^2*f*h + ((-1)) *b^2*f*h + (2) *a*e*f*h + ((-2)) *e^2*f*h + (1) *e*f^2*h + ((-2)) *a^2*c*i + ((-2)) *b^2*c*i + (1) *a^2*d*i + (1) *b^2*d*i + ((-1)) *a*b*e*i + (1) *a*d*e*i + (1) *b*e^2*i + ((-1)) *d*e^2*i + (4) *a*c*f*i + ((-3)) *a*d*f*i + ((-1)) *b*e*f*i + (1) *d*e*f*i + (1) *b*f^2*i + ((-2)) *c*f^2*i + (1) *d*f^2*i + (1) *a*b*g*i + (1) *b*e*g*i + ((-4)) *b*f*g*i + ((-1)) *b*e*h*i + (3) *b*f*h*i + ((-1)) *b^2*i^2 + (4) *b*c*i^2 + ((-2)) *b*d*i^2 + (1) *a*e*i^2 + ((-1)) *a*f*i^2 + (3) *a*g*i^2 + ((-4)) *e*g*i^2 + (1) *f*g*i^2 + ((-3)) *a*h*i^2 + (3) *e*h*i^2 + (1) *b*i^3 + ((-2)) *c*i^3 + (1) *d*i^3 + (2) *a^2*c*j + (2) *b^2*c*j + ((-1)) *a^2*d*j + ((-1)) *b^2*d*j + (1) *a*b*e*j + ((-1)) *a*d*e*j + ((-1)) *b*e^2*j + (1) *d*e^2*j + ((-4)) *a*c*f*j + (3) *a*d*f*j + (1) *b*e*f*j + ((-1)) *d*e*f*j + (3) *c*f^2*j + ((-2)) *d*f^2*j + ((-1)) *a*b*g*j + ((-1)) *b*e*g*j + (2) *b*f*g*j + (1) *b*e*h*j + ((-1)) *b*f*h*j + (1) *a^2*i*j + (2) *b^2*i*j + ((-4)) *b*c*i*j + (2) *b*d*i*j + ((-2)) *a*e*i*j + (1) *a*f*i*j + ((-7)) *a*g*i*j + (7) *e*g*i*j + (2) *f*g*i*j + (6) *a*h*i*j + ((-5)) *e*h*i*j + ((-3)) *f*h*i*j + ((-2)) *b*i^2*j + (2) *c*i^2*j + ((-1)) *d*i^2*j + ((-1)) *a^2*j^2 + ((-1)) *b^2*j^2 + (1) *a*e*j^2 + (4) *a*g*j^2 + ((-3)) *e*g*j^2 + ((-2)) *f*g*j^2 + ((-3)) *a*h*j^2 + (2) *e*h*j^2 + (2) *f*h*j^2 + (1) *b*i*j^2 ; ((-1)) *a^2*b*c + ((-1)) *b^3*c + (1) *a^2*b*d + (1) *b^3*d + (2) *a*b*c*e + ((-2)) *a*b*d*e + (1) *a^2*e^2 + ((-1)) *b^2*e^2 + (1) *b*d*e^2 + ((-1)) *a^3*f + ((-1)) *a*b^2*f + (1) *a*b*d*f + ((-1)) *a^2*e*f + (3) *b^2*e*f + ((-2)) *b*c*e*f + ((-1)) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + ((-2)) *b^2*f^2 + (1) *b*c*f^2 + (1) *b*d*f^2 + (1) *a*e*f^2 + (1) *a^2*e*g + (1) *b^2*e*g + ((-2)) *a*e^2*g + (2) *a^2*f*g + (2) *e^2*f*g + ((-2)) *a*f^2*g + ((-1)) *e*f^2*g + ((-1)) *a^2*e*h + ((-1)) *b^2*e*h + (1) *a*e^2*h + ((-1)) *a^2*f*h + (1) *a*e*f*h + ((-1)) *e^2*f*h + (1) *a*f^2*h + ((-1)) *a^2*b*i + ((-1)) *b^3*i + ((-1)) *a^2*c*i + (3) *b^2*c*i + (3) *a^2*d*i + ((-2)) *b^2*d*i + (2) *a*b*e*i + ((-2)) *a*d*e*i + (1) *a*b*f*i + (2) *a*c*f*i + ((-4)) *a*d*f*i + ((-2)) *b*e*f*i + (2) *d*e*f*i + ((-1)) *c*f^2*i + (1) *d*f^2*i + (2) *a*b*g*i + ((-2)) *b*e*g*i + ((-2)) *b*f*g*i + ((-3)) *a*b*h*i + (2) *b*e*h*i + (3) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-2)) *b*c*i^2 + (1) *b*d*i^2 + ((-1)) *a*f*i^2 + ((-2)) *a*g*i^2 + (2) *f*g*i^2 + (1) *a*h*i^2 + ((-1)) *f*h*i^2 + (1) *a^2*b*j + (1) *b^3*j + (2) *a^2*c*j + ((-4)) *a^2*d*j + ((-1)) *b^2*d*j + ((-2)) *a*b*e*j + ((-2)) *a*c*e*j + (4) *a*d*e*j + (1) *b*e^2*j + ((-1)) *d*e^2*j + ((-2)) *a*c*f*j + (3) *a*d*f*j + ((-1)) *b*e*f*j + (2) *c*e*f*j + ((-1)) *d*e*f*j + (2) *b*f^2*j + ((-2)) *d*f^2*j + ((-2)) *a*b*g*j + (2) *b*f*g*j + (3) *a*b*h*j + ((-3)) *b*f*h*j + ((-3)) *a^2*i*j + ((-2)) *b*c*i*j + (2) *b*d*i*j + (3) *a*f*i*j + (2) *a*g*i*j + (2) *e*g*i*j + ((-2)) *f*g*i*j + (1) *a*h*i*j + ((-2)) *e*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + (2) *c*i^2*j + ((-1)) *d*i^2*j + (2) *a^2*j^2 + ((-1)) *b^2*j^2 + (1) *b*c*j^2 + ((-2)) *a*f*j^2 + ((-1)) *e*g*j^2 + ((-2)) *a*h*j^2 + (1) *e*h*j^2 + (2) *f*h*j^2 + (1) *b*i*j^2 + ((-1)) *c*i*j^2 ; ];
C:=[
[
((-1)) *b*f^2 + ((-1)) *b^2*i + (1) *b*i^2 + (1) *b^2*j + (1) *f^2*j + ((-1)) *i^2*j + ((-1)) *b*j^2 + (1) *i*j^2 ; ((-1)) *a^2*e + ((-1)) *b^2*e + (1) *b*d*e + (2) *a^2*f + (2) *b^2*f + ((-2)) *b*d*f + (1) *a*e*f + ((-2)) *a*f^2 + ((-1)) *a^2*g + ((-1)) *b^2*g + (2) *a*e*g + ((-2)) *a*f*g + ((-2)) *e*f*g + (3) *f^2*g + (1) *a^2*h + (1) *b^2*h + ((-1)) *a*e*h + (1) *e*f*h + ((-1)) *f^2*h + (2) *b*g*i + ((-2)) *b*h*i + (1) *b*e*j + ((-1)) *d*e*j + ((-2)) *b*f*j + (2) *d*f*j + ((-2)) *g*i*j + (2) *h*i*j + (1) *g*j^2 + ((-1)) *h*j^2 ; (1) *a^2*f^2 + (1) *b^2*f^2 + ((-1)) *a*f^3 + ((-1)) *a^2*f*g + ((-1)) *b^2*f*g + (1) *f^3*g + (1) *a^2*f*h + (1) *b^2*f*h + ((-1)) *a*f^2*h + (1) *a^2*c*i + (1) *b^2*c*i + (1) *a*b*f*i + ((-2)) *a*c*f*i + ((-1)) *b*f^2*i + (1) *c*f^2*i + (2) *b*f*g*i + ((-1)) *a*b*h*i + ((-1)) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-2)) *b*c*i^2 + ((-1)) *a*f*i^2 + ((-2)) *a*g*i^2 + (2) *f*g*i^2 + (1) *a*h*i^2 + ((-1)) *f*h*i^2 + ((-1)) *a^2*c*j + ((-1)) *b^2*c*j + ((-1)) *a*b*f*j + (2) *a*c*f*j + ((-1)) *c*f^2*j + (1) *a*b*h*j + ((-1)) *b*f*h*j + ((-3)) *a^2*i*j + ((-2)) *b^2*i*j + (2) *b*c*i*j + (3) *a*f*i*j + (4) *a*g*i*j + ((-6)) *f*g*i*j + ((-1)) *a*h*i*j + (3) *f*h*i*j + ((-1)) *b*i^2*j + (2) *c*i^2*j + (2) *a^2*j^2 + (1) *b^2*j^2 + ((-2)) *a*f*j^2 + ((-2)) *a*g*j^2 + (3) *f*g*j^2 + ((-1)) *f*h*j^2 + (2) *b*i*j^2 + ((-3)) *c*i*j^2 + ((-1)) *b*j^3 + (1) *c*j^3 ; (1) *a*e^3 + ((-3)) *a*e^2*f + ((-1)) *a^2*f^2 + ((-1)) *b^2*f^2 + ((-1)) *b*c*f^2 + (1) *b*d*f^2 + (3) *a*e*f^2 + (1) *a*e^2*g + ((-2)) *e^3*g + (1) *a^2*f*g + (1) *b^2*f*g + ((-2)) *a*e*f*g + (5) *e^2*f*g + (1) *a*f^2*g + ((-4)) *e*f^2*g + ((-1)) *a*e^2*h + (1) *e^3*h + ((-1)) *a^2*f*h + ((-1)) *b^2*f*h + (2) *a*e*f*h + ((-2)) *e^2*f*h + (1) *e*f^2*h + ((-2)) *a^2*c*i + ((-2)) *b^2*c*i + (1) *a^2*d*i + (1) *b^2*d*i + ((-1)) *a*b*e*i + (1) *a*d*e*i + (1) *b*e^2*i + ((-1)) *d*e^2*i + (4) *a*c*f*i + ((-3)) *a*d*f*i + ((-1)) *b*e*f*i + (1) *d*e*f*i + (1) *b*f^2*i + ((-2)) *c*f^2*i + (1) *d*f^2*i + (1) *a*b*g*i + (1) *b*e*g*i + ((-4)) *b*f*g*i + ((-1)) *b*e*h*i + (3) *b*f*h*i + ((-1)) *b^2*i^2 + (4) *b*c*i^2 + ((-2)) *b*d*i^2 + (1) *a*e*i^2 + ((-1)) *a*f*i^2 + (3) *a*g*i^2 + ((-4)) *e*g*i^2 + (1) *f*g*i^2 + ((-3)) *a*h*i^2 + (3) *e*h*i^2 + (1) *b*i^3 + ((-2)) *c*i^3 + (1) *d*i^3 + (2) *a^2*c*j + (2) *b^2*c*j + ((-1)) *a^2*d*j + ((-1)) *b^2*d*j + (1) *a*b*e*j + ((-1)) *a*d*e*j + ((-1)) *b*e^2*j + (1) *d*e^2*j + ((-4)) *a*c*f*j + (3) *a*d*f*j + (1) *b*e*f*j + ((-1)) *d*e*f*j + (3) *c*f^2*j + ((-2)) *d*f^2*j + ((-1)) *a*b*g*j + ((-1)) *b*e*g*j + (2) *b*f*g*j + (1) *b*e*h*j + ((-1)) *b*f*h*j + (1) *a^2*i*j + (2) *b^2*i*j + ((-4)) *b*c*i*j + (2) *b*d*i*j + ((-2)) *a*e*i*j + (1) *a*f*i*j + ((-7)) *a*g*i*j + (7) *e*g*i*j + (2) *f*g*i*j + (6) *a*h*i*j + ((-5)) *e*h*i*j + ((-3)) *f*h*i*j + ((-2)) *b*i^2*j + (2) *c*i^2*j + ((-1)) *d*i^2*j + ((-1)) *a^2*j^2 + ((-1)) *b^2*j^2 + (1) *a*e*j^2 + (4) *a*g*j^2 + ((-3)) *e*g*j^2 + ((-2)) *f*g*j^2 + ((-3)) *a*h*j^2 + (2) *e*h*j^2 + (2) *f*h*j^2 + (1) *b*i*j^2 ; ((-1)) *a^2*b*c + ((-1)) *b^3*c + (1) *a^2*b*d + (1) *b^3*d + (2) *a*b*c*e + ((-2)) *a*b*d*e + (1) *a^2*e^2 + ((-1)) *b^2*e^2 + (1) *b*d*e^2 + ((-1)) *a^3*f + ((-1)) *a*b^2*f + (1) *a*b*d*f + ((-1)) *a^2*e*f + (3) *b^2*e*f + ((-2)) *b*c*e*f + ((-1)) *b*d*e*f + ((-1)) *a*e^2*f + (1) *a^2*f^2 + ((-2)) *b^2*f^2 + (1) *b*c*f^2 + (1) *b*d*f^2 + (1) *a*e*f^2 + (1) *a^2*e*g + (1) *b^2*e*g + ((-2)) *a*e^2*g + (2) *a^2*f*g + (2) *e^2*f*g + ((-2)) *a*f^2*g + ((-1)) *e*f^2*g + ((-1)) *a^2*e*h + ((-1)) *b^2*e*h + (1) *a*e^2*h + ((-1)) *a^2*f*h + (1) *a*e*f*h + ((-1)) *e^2*f*h + (1) *a*f^2*h + ((-1)) *a^2*b*i + ((-1)) *b^3*i + ((-1)) *a^2*c*i + (3) *b^2*c*i + (3) *a^2*d*i + ((-2)) *b^2*d*i + (2) *a*b*e*i + ((-2)) *a*d*e*i + (1) *a*b*f*i + (2) *a*c*f*i + ((-4)) *a*d*f*i + ((-2)) *b*e*f*i + (2) *d*e*f*i + ((-1)) *c*f^2*i + (1) *d*f^2*i + (2) *a*b*g*i + ((-2)) *b*e*g*i + ((-2)) *b*f*g*i + ((-3)) *a*b*h*i + (2) *b*e*h*i + (3) *b*f*h*i + (1) *a^2*i^2 + (1) *b^2*i^2 + ((-2)) *b*c*i^2 + (1) *b*d*i^2 + ((-1)) *a*f*i^2 + ((-2)) *a*g*i^2 + (2) *f*g*i^2 + (1) *a*h*i^2 + ((-1)) *f*h*i^2 + (1) *a^2*b*j + (1) *b^3*j + (2) *a^2*c*j + ((-4)) *a^2*d*j + ((-1)) *b^2*d*j + ((-2)) *a*b*e*j + ((-2)) *a*c*e*j + (4) *a*d*e*j + (1) *b*e^2*j + ((-1)) *d*e^2*j + ((-2)) *a*c*f*j + (3) *a*d*f*j + ((-1)) *b*e*f*j + (2) *c*e*f*j + ((-1)) *d*e*f*j + (2) *b*f^2*j + ((-2)) *d*f^2*j + ((-2)) *a*b*g*j + (2) *b*f*g*j + (3) *a*b*h*j + ((-3)) *b*f*h*j + ((-3)) *a^2*i*j + ((-2)) *b*c*i*j + (2) *b*d*i*j + (3) *a*f*i*j + (2) *a*g*i*j + (2) *e*g*i*j + ((-2)) *f*g*i*j + (1) *a*h*i*j + ((-2)) *e*h*i*j + ((-1)) *f*h*i*j + ((-1)) *b*i^2*j + (2) *c*i^2*j + ((-1)) *d*i^2*j + (2) *a^2*j^2 + ((-1)) *b^2*j^2 + (1) *b*c*j^2 + ((-2)) *a*f*j^2 + ((-1)) *e*g*j^2 + ((-2)) *a*h*j^2 + (1) *e*h*j^2 + (2) *f*h*j^2 + (1) *b*i*j^2 + ((-1)) *c*i*j^2 ; ];
[
0; (1) *d ; ((-1)) *c ; 0; ];
[
((-1)) *e ; (1) *e ; (1) *a ; ];
];
c:=
1;