REMIS: Consistency of Inequalities

Description of the problem on p.325: The problem decides whether the intersection of the open ball with radius 1 centered at the origin and in the open circular cylinder with radius 1 and axis the $x=0$, $y+z=2$ is nonempty.

con := ex({x,y,z},x**2+y**2+z**2<1 and x**2+(y+z-2)**2<1);

end;  % of file