RedLogとQEPCADB

には互いに他を補う部分があります．例えば
x=a+b+c，y=ab+bc+ca，z=abc，a^3+b^3+c^3=1
を満たす実数a，b，cが存在する条件をRedLogに

rlqe(ex({a,b,c},and(x=a+b+c,y=a*b+b*c+c*a,z=a*b*c,a^3+b^3+c^3=1)));

と尋ねると，１０秒足らずで

5*x**6 - 24*x**4*y - 14*x**3 + 24*x**2*y**2 + 36*x*y + 12*y**3 + 9 = 0 and 4*x**3*z - x**2*y**2 - 18*x*y*z + 4*y**3 + 27*z**2 = 0 and x**3 - 3*x*y + 3*z - 1 = 0 and x**2 - 3*y >= 0 or 5*x**6 - 24*x**4*y - 14*x**3 + 24*x**2*y**2 + 36*x*y + 12*y**3 + 9 < 0 and 4*x**3*z - x**2*y**2 - 18*x*y*z + 4*y**3 + 27*z**2 < 0 and x**3 - 3*x*y + 3*z - 1 = 0 and x**2 - 3*y > 0

と答えますが，これを先述したRedLogの種々のsimplifierで処理してもそれ程簡約は進みません．

一方，QEPCADBに同じ条件を

(E a)(E b)(E c)[a^3 + b^3 + c^3 - 1 = 0 /\ a b c - z = 0 /\ a b + a c + b c - y = 0 /\ a + b + c - x = 0].

と尋ねても，一向に答える気配がないのですが，上のRedLogのやりっ放しの結果を

[ 5 x^6 - 24 x^4 y - 14 x^3 + 24 x^2 y^2 + 36 x y + 12 y^3 + 9 <= 0 /\ 4 x^3 z - x^2 y^2 - 18 x y z + 4 y^3 + 27 z^2 <= 0 /\ x^3 - 3 x y + 3 z - 1 = 0 /\ x^2 - 3 y >= 0 /\ [5 x^6 - 24 x^4 y - 14 x^3 + 24 x^2 y^2 + 36 x y + 12 y^3 + 9 = 0 \/ 4 x^3 z - x^2 y^2 - 18 x y z + 4 y^3 + 27 z^2 < 0] /\ [5 x^6 - 24 x^4 y - 14 x^3 + 24 x^2 y^2 + 36 x y + 12 y^3 + 9 = 0 \/ x^2 - 3 y > 0] /\ [5 x^6 - 24 x^4 y - 14 x^3 + 24 x^2 y^2 + 36 x y + 12 y^3 + 9 < 0 \/ 4 x^3 z - x^2 y^2 - 18 x y z + 4 y^3 + 27 z^2 = 0] /\ [4 x^3 z - x^2 y^2 - 18 x y z + 4 y^3 + 27 z^2 = 0 \/ x^2 - 3 y > 0] ].

と入力すると瞬時に

12 y^3 + 24 x^2 y^2 - 24 x^4 y + 36 x y + 5 x^6 - 14 x^3 + 9 <= 0 /\ 3 z - 3 x y + x^3 - 1 = 0

と返してくれるのです．