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;