if get('geometry2, 'version)=false then load(geometry2);
X:[x1,y1]; Y:[x2,y2]; O1:[a,0]; O2:[-a,0];
vars:[]; params:[a,x1,y1,x2,y2,r1,r2,s1,s2];

eqns:[r1+s1-u*r1*s1];

cover:[
[
	distance(X,O1,r1),
	distance(X,O2,r2),
	r1+r2-2,
	distance(Y,O1,s1),
	distance(Y,O2,s2),
	s1+s2-2,
	collinear(X,Y,O1),
	u*(1-a^2)-2
],
[a,x1-x2]
];

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