;; This is supposed to prove that the 3 altitudes of a triangle
;; intersect at a single point; if consistent, then the altitudes have
;; a common point (x,y). Only x3 y3 are treated as parameters, i.e.
;; we vary only one vertex; adding all three vertices produces 6 parameters,
;; too much to swallow for the software
(string-grobner-system
"[X*Y1-U1*Y1-X1*Y+U1*Y+V1*X1-V1*X,X*Y2-U2*Y2-X2*Y+U2*Y+V2*X2-V2*X,X*Y3-U3*Y3-X3*Y+U3*Y+V3*X3-V3*X,-Y1*Y3+V1*Y3+Y1*Y2-V1*Y2-X1*X3+U1*X3+X1*X2-U1*X2,-Y2*Y3+V2*Y3+Y1*Y2-V2*Y1-X2*X3+U2*X3+X1*X2-U2*X1,-Y2*Y3+Y1*Y3+V3*Y2-V3*Y1-X2*X3+X1*X3+U3*X2-U3*X1]"
'(x y u1 v1 u2 v2 u3 v3)
'(x1 y1 x2 y2 x3 y3)
:main-order #'lex>
:parameter-order #'lex>)