;; An automatic proof of the Apollonius Circle Theorem
;; Encoding by hand
(setf vars '(x1 x2))
(setf params '(u1 u2))
(setf allvars (append vars params))
(setf hypotheses "[x1*u1-x2*u2, -x1*u2-u1*x2+u1*u2]")
(setf conclusions  "[2*x2^2-u2*x2+2*x1^2-u1*x1,u1,u2]")
;; Saturation test
(string-ideal-polysaturation-1 hypotheses conclusions allvars)