source: CGBLisp/tags/rel-1.0-alpha-1/examples/klee.macsyma@ 22

if get('geometry2, 'version)=false then load(geometry2);
X:[x1,y1]; Y:[x2,y2]; O1:[a,0]; O2:[-a,0];
vars:[x1,y1,x2,y2,r1,r2,s1,s2,v]; params:[a];
cover:[[],[a]];
u:2/(1-a^2);
concl:r1+s1-u*r1*s1;


eqns:[
        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),
        1-v*concl
];

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