[ Example 5.14 from Hong, Liska, Steinberg, 
  "Testing Stability by Quantifier Elimination" 
  Journal of Symbolic Computation, Vol. 24, No. 2, 
  August 1997. The "G" quatifier means "for all but 
  finitely many". ]
(a,b,c2)
0
(G a)(G b)(G c2)[
[ 0 <= a /\ a <= 1 /\ 0 <= b /\ b <= 1 ]
==>
[
  c2^4 (a - b + 1) ( a - b - 1) (a - b)^2 <= 0
  /\
  c2^4 b^2 (b^2 - 1) + 4 c2^3 a b^2 (b - 1)
  + 2 c2^2 a b (3 a b - 2 a - 2 b + 1)
  + 4 c2 a^2 b (a - 1) + a^2 (a^2 - 1) <= 0
  /\
  [
    c2^2 ( 8 a^2 b^2 - 12 a^2 b + 5 a^2 - 8 a b^3 + 8 a b^2 
    + 2 a b - 4 a + 4 b^4 - 4 b^3  - 3 b^2 + 4 b  ) 
    + 2 c2 ( 4 a^3 b  - 2 a^3 - 4 a^2 b^2 - 2 a^2 b + a^2 
    + 4 a b^3 - 2 a b^2 + 2 a b - 2 b^3 + b^2  )  
    + 4 a^4 - 8 a^3 b - 4 a^3 + 8 a^2 b^2 + 8 a^2 b - 3 a^2 
    - 12 a b^2 + 2 a b + 4 a + 5 b^2 - 4 b <= 0
   \/
    2 c2^4 b ( 3 a^2 b - 2 a^2 - 2 a b^2 + a + b^3 - b) 
    +  4 c2^3 a b ( a^2 - a + b^2 - b) 
    + 2 c2^2 a ( a^3 - 2 a^2b + 3 a b^2 - a - 2 b^2 + b ) <= 0
  ]
]
].