1988年東大前期理科第６問

これも「Vがその四面体の体積となる」という論理式を，mmaに

RS = Reduce[
   Exists[{a, b, c}, 
    And[0 <= a, 0 <= b, 0 <= c, 
     0 <= S == a*b*c/(4*R), (a/(2*R))^2 + ((b^2 + c^2 - a^2)/(2*b*c))^2 == 1]], Reals]
Reduce[Exists[{S, R, d, x, y, z}, 
  And[RS, x^2 + y^2 + z^2 == 1, V == S*Abs[d - z]/3, d^2 + R^2 == 4^2]], Reals]

とQEさせれば

0 <= V <= 9 Sqrt[3]

となります．