<< Developer`; << 
      Experimental`;

Finns det två punkter på en enhetscirkel med avstånd minst 2?

S =  
      x1^2 + y1^2 == 1  &&  
        x2^2 + y2^2 == 
          1  &&  (x1 - x2)^2 + (y1 - 
                  y2)^2 ≥4

ExistsRealQ[ 
      S, {x1, y1, x2, y2}]

För vilka t ≥ 
      0 finns det tre punkter på enhetscirkeln med inbördes avstånd minst (Sqrt[t])?
(Vi kan fixera en punkt :  x1 = 1,  
            y1 = 0)

x1 = 1;  y1 = 0;

Resolve[
      Exists[{x2, y2, x3, y3},  (x2 | y2 | x3 | y3 | t)  ∈ 
          Reals, 
 
        x2^2 +  y2^2  == 1  &&  
x3^2 + y3^2  == 
            1   && 
t  ≥ 
            0  &&  
(x1 - x2)^2  + (y1 - 
                    y2)^2 ≥  
            t &&  
(x1 - x3)^2  + (y1 - 
                    y3)^2 ≥  
            t &&   
(x2 - x3)^2  +  (y2 - 
                    y3)^2  ≥  t]]

T  =  
        0  ≤  x1  &&  
          x1  ≤ 
            1  && 
    0  ≤  y1  &&  
          y1  ≤ 
            1  && 
    0  ≤  x2  &&  
          x2  ≤ 
            1  && 
    0  ≤  y2  &&  
          y2  ≤ 
            1  && 
    0  ≤  x3  &&  
          x3  ≤ 
            1  && 
    0  ≤  y3  &&  
          y3  ≤ 
            1  && 
   0  ≤  x4  &&  
          x4  ≤ 
            1  && 
    0  ≤  y4  &&  
          y4  ≤ 
            1  && 
    t  ≥ 
            0  && 
    t ≤  
            2  && 
(x1 - x2)^2  + (y1 - 
                    y2)^2 ≥  
            t &&  
(x1 - x3)^2  + (y1 - 
                    y3)^2 ≥  
            t &&  
(x1 - x4)^2  + (y1 - 
                    y4)^2 ≥  
            t &&  
(x2 - x3)^2  + (y2 - 
                    y3)^2 ≥  
            t &&  
(x2 - x4)^2  + (y2 - 
                    y4)^2 ≥  
            t &&  
(x3 - x4)^2  + (y3 - 
                    y4)^2 ≥  
            t;

Resolve[
      Exists[{x1, y1, x2, y2, x3, y3, x4, 
          y4},  (x1 | y1 | x2 | y2 | x3 | y3 | x4 | y4 | t)  ∈ 
          Reals, T]]