RedLogはウソをつく

ことがあります．例えば，x^2+y^2=1を満たす任意の実数x，yがax^2+cxy+by^2=1を満たす条件

all({x,y},x^2+y^2=1 impl a*x^2+c*x*y+b*y^2=1)

をrlqeでQEして，rlgsnで簡約すると即座に

a - 1 > 0 and b - 1 = 0 and c = 0 or
a - 1 = 0 and b - 1 = 0 and c = 0 or
a - 1 < 0 and b - 1 = 0 and c = 0

と答えます．b=1，c=0はよいのですが，aが任意というのは戴けません．簡約以前の式をMathematicaのReduceコマンドで簡約してもc == 0 && b == 1なのでrlqeに問題があるようです．