if get('geometry2, 'version)=false then load(geometry2);
X:[x1,y1]; Y:[x2,y2]; O1:[-p,0]; O2:[p,0];
/* Semi-axes are 1 and sqrt(1-p^2) */
f(W) := (1-p^2)*w[1]^2+w[2]^2-(1-p^2); /* W is on the ellipse */
vars: []; params: [p,u,x1,y1,x2,y2,r1,r2,s1,s2];
cover: [
	[
		f(X), f(Y),
		distance(X,O1,r1),
		distance(Y,O1,s1),
		collinear(X,Y,O1),
		u*(1-p^2)-2
	],
	[
		p,
		(x1-x2)*(y1-y2)
	]
];
concl: (r1+s1-u*r1*s1)*(r1+s1+u*r1*s1)*(r1-s1-u*r1*s1)*(r1-s1+u*r1*s1);



eqns:[concl];

eqns:expand(eqns);
cover:expand(cover);
stringout("klee2.out",eqns,vars,params,cover);