source: CGBLisp/examples/klee3.macsyma@ 1

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);