parker/example2.formula

   1 # This example Presburger formula has 16000 solutions.
   2
   3 {[In_1,In_2]: Exists(Ex_1,Ex_2: 2 <= Ex_1 <= 499 && 2 <= Ex_2 <= 499 && 16In_1 <= Ex_1-1 < 16In_1 + 16 && In_2=Ex_2)} union
   4 {[In_1,In_2]: Exists(Ex_1,Ex_2: 2 <= Ex_1 <= 499 && 2 <= Ex_2 <= 499 && 16In_1 <= Ex_1-2 < 16In_1 + 16 && In_2=Ex_2)} union
   5 {[In_1,In_2]: Exists(Ex_1,Ex_2: 2 <= Ex_1 <= 499 && 2 <= Ex_2 <= 499 && 16In_1 <= Ex_1 < 16In_1 + 16 && In_2=Ex_2)} union
   6 {[In_1,In_2]: Exists(Ex_1,Ex_2: 2 <= Ex_1 <= 499 && 2 <= Ex_2 <= 499 && 16In_1 <= Ex_1-1 < 16In_1 + 16 && In_2=Ex_2-1)} union
   7 {[In_1,In_2]: Exists(Ex_1,Ex_2: 2 <= Ex_1 <= 499 && 2 <= Ex_2 <= 499 && 16In_1 <= Ex_1-1 < 16In_1 + 16 && In_2=Ex_2+1)}