次は，方程式 に正の解が存在すると述べている：

Resolveを使ってこの陳述が真になる実数パラメータの条件を求める：

Reduceは，解かれた形で条件を返す：

次は，方程式が真になる が存在すると述べている：

Resolveを使ってこの陳述が真であることを証明する：

次は，方程式が真となる実数 が存在すると述べている：

Resolveを使ってこの陳述が偽であることを証明する：

次は，不等式が真となるペアが存在すると述べている：

領域指定がないので，Resolveは不等式中の代数的変数が実数であるとみなす：

領域をComplexesとすると，不等式がTrueになる複素数値が使える：

次は，トートロジーの否定が満足できると述べている：

Resolveを使ってこれがFalseであることを証明する：

式が明示的に変数を含まない場合，Existsは自動的に簡約する：

TraditionalFormによる表示：

次は，二次方程式が負の値に達すると述べている：

次は，実数パラメータで明示的な条件を返す：

1つの領域が他の領域に含まれるかどうかテストする：

次は，R1は満足するがR2は満足しない点があると述べている：

この陳述は偽である．したがってR1で定義された範囲はR2で定義された範囲に含まれる：

この関係をプロットする：

幾何学的な推測をテストする：

次は，推測が真ではない三角形が存在すると述べている：

この陳述は真である．したがって推測は任意の三角形について真である訳ではない：

次は，推測が真ではない鋭角三角形が存在すると述べている：

この陳述は偽である．したがってこの推測はすべての鋭角三角形について真である：

この陳述がトートロジーであることを証明する：

次は，この陳述が真ではないの値は存在しないことを証明している：

これは，TautologyQを用いても証明できる：

Existsを否定するとForAllが返される：

ResolveまたはReduceを使って量限定子を除去することができる：

このように量限定子を除去する：

次では，量限定子を除去し，結果の方程式と不等式を解く：

次は，不等式系が解を持つことを示している：

FindInstanceを使って明示的な解の例を求める：

次は，方程式を満足する複素数 が存在すると述べている：

Resolveを使って，この陳述が真となる と の条件を求める：

次は，Eliminateを使って同じ問題を解いている：

次は，複素代数集合 の 軸に沿った投影を求める：

次は，実単位円の 軸に沿った投影を求める：