SLFQ - ATPとCASのこと

今回はQEPCAD Bの応用プログラムである，SLFQ（http://www.usna.edu/cs/~qepcad/SLFQ/Home.html）についてお話しましょう．

SLFQは，Simplifying Large Formulas with QEPCAD Bという名の通り，QEPCAD Bを使って大きな論理式を簡約するもので，次からダウンロードできます．
http://www.usna.edu/cs/~qepcad/SLFQ/simplify-1.15.tar.gz

使い方は簡単で，QEPCAD BまたはRedLog形式のquantifier free formulaの書かれたファイル名を引数として起動するだけです．ただし，論理式には連言，選言以外の結合子や否定を含まないものとし，原子論理式の右辺は0とします．

次は前回同様，ファイルの代わりにecho出力をパイプ処理したものです．

knoppix@Microknoppix:~$ echo "x^2-1=0 and x+1<>0" | slfq
The input formula is: The AND of 2 things!
It contains 2 atomic formulas, nested to a depth of 1.
Variables are: x
Cutoff is 2
Simplifying conjunct number 1
Subformula 1:
[ x + 1 >= 0 /\ x - 1 <= 0 /\ [ x - 1 = 0 \/ x + 1 = 0 ] ]
Simplifying conjunct number 2
Subformula 2:
x + 1 /= 0

===================== The End =======================

-

0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
2490643 Cells in AVAIL, 2500000 Cells in SPACE.
System time: 83 milliseconds.
System time after the initialization: 24 milliseconds.

-

An equivalent formula is:
x - 1 = 0
There were 3 QEPCADB calls!

このSLFQは入力された式をDNF（選言標準形選言標準形 - Wikipedia）に直し，各連言項をQEPCAD Bで簡約するプログラムです．

その威力はvirtual substitutionで頑張れるだけ頑張り強大な論理式を出力するRedLogのrlqeなどとの組み合わせで最大限に発揮されます．

次の例は，QEPCAD B単独ではcellを確保し直さねばならなかったもので処理時間も分単位でしたが，rlqeでQEし，slfqで簡約すれば秒単位で片付きます．

knoppix@Microknoppix:~$ reduce -w
Reduce (Free CSL version), 19-Feb-11 ...
1: load qepcad;off nat;
Grow hash from 1 chunks
... to 1 chunks
Rehashing done

3: f:=rlqe ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1);
f := a**2 + b**2 - 1 >= 0 and b <> 0 and c <> 0 or a**2*b**2 - a**2*c**2 + b**4 + b**2*c**2 = 0 and a <> 0 and b + c <> 0 and b - c <> 0 and （b <> 0 or c <> 0） and （a**2*b**8 + 2*a**2*b**6*c**2 - 2*a**2*b**6 + a**2*b**4*c**4 + 4*a**2*b**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**4 - 2*a**2*b**2*c**2 - 4*a**2*c**6 + a**2*c**4 + b**10 + 3*b**8*c**2 - 2*b**8 + 3*b**6*c**4 - 2*b**6*c**2 + b**6 + b**4*c**6 + 2*b**4*c**4 - b**4*c**2 + 2*b**2*c**6 - b**2*c**4 + c**6 <= 0 or c = 0） and （b*c <= 0 and （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 <= 0 or c = 0） or （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 <= 0 or b**6*c + b**4*c - b**2*c**5 - 2*b**2*c**3 + c**5 <= 0 or c = 0） and （b*c > 0 or b**6*c + b**4*c - b**2*c**5 - 2*b**2*c**3 + c**5 <= 0 and （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 >= 0 or c = 0）） or b**6*c + b**4*c - b**2*c**5 - 2*b**2*c**3 + c**5 >= 0 and （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 >= 0 or c = 0） or b*c >= 0 and （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 <= 0 or c = 0） or （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 <= 0 or b**6*c + b**4*c - b**2*c**5 - 2*b**2*c**3 + c**5 <= 0 or c = 0） and （b*c < 0 or b**6*c + b**4*c - b**2*c**5 - 2*b**2*c**3 + c**5 <= 0 and （a**2*b**10 + 3*a**2*b**8*c**2 - 2*a**2*b**8 + 3*a**2*b**6*c**4 + 6*a**2*b**6*c**2 + a**2*b**6 + a**2*b**4*c**6 + 2*a**2*b**4*c**4 - a**2*b**4*c**2 - 6*a**2*b**2*c**6 - a**2*b**2*c**4 + a**2*c**6 + b**12 + 3*b**10*c**2 - 2*b**10 + 3*b**8*c**4 - 2*b**8*c**2 + b**8 + b**6*c**6 + 2*b**6*c**4 - b**6*c**2 + 2*b**4*c**6 - b**4*c**4 + b**2*c**6 >= 0 or c = 0））） or a <> 0 and b <> 0 and （a**2*b**2 + a**2*c**2 - b**2 - c**2 >= 0 or c = 0） and （a**2*b**2 + a**2*c**2 - b**2 - c**2 >= 0 or a + 1 = 0 or a - 1 = 0） or a**2*b**2 + a**2*c**2 - b**2 - c**2 >= 0 and a <> 0 and c <> 0 or b <> 0 and c = 0 and （a**2*b**2 - a**2*c**2 + b**4 + b**2*c**2 < 0 or a**2*b**2 - a**2*c**2 + b**4 + b**2*c**2 = 0 and （a*b**2 - a*c**2 > 0 or b**4 + b**2*c**2 - b**2 + c**2 >= 0 and （a = 0 or b + c = 0 or b - c = 0））） or （a <> 0 or b <> 0） and （a**2 + b**2 - 1 >= 0 or b = 0） and （（b <> 0 or c <> 0） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or c = 0 or a >= 0 and （a - 1 = 0 or a = 0 and b = 0）） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or a - 1 = 0 or b = 0 or c = 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b >= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 and a*b >= 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b <= 0） and （a*b < 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b <= 0）） or （b <> 0 or c <> 0） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or c = 0 or a <= 0 and （a + 1 = 0 or a = 0 and b = 0）） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or a + 1 = 0 or b = 0 or c = 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b >= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 and a*b <= 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b <= 0） and （a*b > 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b <= 0））） or a**2*b**2 - a**2*c**2 + b**4 + b**2*c**2 <> 0 and （a**2*b**4 - a**2*c**4 + b**6 + 2*b**4*c**2 - b**4 + b**2*c**4 + c**4 >= 0 or b = 0） and （（b <> 0 or c <> 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0）） and （b*c <= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 < 0 or a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 and a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0）） and （b*c > 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0 or c = 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 < 0 or （a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 > 0 or b = 0））） or （（a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 >= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0） or a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 >= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 > 0 or b = 0）） or b*c >= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 < 0 or a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 and a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0）） and （b*c < 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0 or c = 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 < 0 or （a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 > 0 or b = 0）））） or （b <> 0 or c <> 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） and （b*c <= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 > 0 or a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 and a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0）） and （b*c > 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0 or c = 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 > 0 or （a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 < 0 or b = 0））） or （（a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 >= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0） or a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 <= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 < 0 or b = 0）） or b*c >= 0 and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 <= 0 or b = 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 > 0 or a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 and a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0）） and （b*c < 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 >= 0 or a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0 or c = 0） and （a**3*b**2*c - a**3*c**3 + a*b**4*c + a*b**2*c**3 > 0 or （a**2*b**4*c - a**2*c**5 + b**6*c + 2*b**4*c**3 + b**2*c**5 <= 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 - b**6 - 2*b**4*c**2 - b**2*c**4 <= 0 or b = 0 or c = 0）） and （c = 0 or （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a + 1 = 0 or a - 1 = 0 or b = 0） and （a**4*b**4 - a**4*c**4 + a**2*b**6 + 2*a**2*b**4*c**2 - a**2*b**4 + a**2*b**2*c**4 + a**2*c**4 + b**6 + 2*b**4*c**2 + b**2*c**4 >= 0 or a*b**2 + a*c**2 < 0 or b = 0））））） or （b <> 0 or a <> 0 and c <> 0） and （a**2 + b**2 - 1 >= 0 or b = 0） and （（b <> 0 or c <> 0） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0 or a = 0 and b = 0）） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b**3 + b*c**2 <= 0） and （a*b < 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b**3 + b*c**2 <= 0） or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b**3 + b*c**2 >= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 and a*b >= 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） or （b <> 0 or c <> 0） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0 or a = 0 and b = 0）） and （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b**3 + b*c**2 <= 0） and （a*b > 0 or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b**3 + b*c**2 <= 0） or a**4 + a**2*b**2 - a**2 - b**2 <= 0 and b**3 + b*c**2 >= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 and a*b <= 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0））） or a**2*b**2 + a**2*c**2 + b**4 + 2*b**2*c**2 - b**2 + c**4 - c**2 >= 0 and （a <> 0 or b <> 0 or c <> 0） and （（b <> 0 or c <> 0） and （（a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or a**5 + a**3*b**2 + a**3*c**2 - a**3 + a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） and （b**3 + b*c**2 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or b = 0） or a*b >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b = 0））） and （（b**2*c + c**3 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0） or a*c >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 > 0）） or b*c >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0） and （a*c < 0 or a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 and b**2*c + c**3 <= 0）） and （b*c < 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0 or c = 0） and （a*c < 0 or b**2*c + c**3 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 > 0）））） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or a**5 + a**3*b**2 + a**3*c**2 - a**3 + a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**3 + b*c**2 <= 0 or b = 0） and （a*b < 0 or b**3 + b*c**2 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or b = 0））） and （（b**2*c + c**3 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0） or a*c >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 > 0）） or b*c <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0） and （a*c < 0 or a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 and b**2*c + c**3 <= 0）） and （b*c > 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0 or c = 0） and （a*c < 0 or b**2*c + c**3 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 > 0））））） or （b <> 0 or c <> 0） and （（a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or a**5 + a**3*b**2 + a**3*c**2 - a**3 + a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） and （b**3 + b*c**2 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or b = 0） or a*b <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b = 0））） and （（b**2*c + c**3 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0） or a*c <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 < 0）） or b*c >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0） and （a*c > 0 or a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 and b**2*c + c**3 <= 0）） and （b*c < 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0 or c = 0） and （a*c > 0 or b**2*c + c**3 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 < 0）））） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or c = 0 or a*b**2 + a*c**2 <= 0 and （a + 1 = 0 or a - 1 = 0） or a**5 + a**3*b**2 + a**3*c**2 - a**3 + a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**3 + b*c**2 <= 0 or b = 0） and （a*b > 0 or b**3 + b*c**2 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or b = 0））） and （（b**2*c + c**3 >= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0） or a*c <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 < 0）） or b*c <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0）） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 <= 0 or c = 0 or a*b**2 + a*c**2 >= 0 and （a + 1 = 0 or a - 1 = 0） or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0） and （a*c > 0 or a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 and b**2*c + c**3 <= 0）） and （b*c > 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 >= 0 or b**2*c + c**3 <= 0 or c = 0） and （a*c > 0 or b**2*c + c**3 <= 0 and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 - b**4 - 2*b**2*c**2 - c**4 <= 0 or c = 0）） and （c = 0 or （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a + 1 = 0 or a - 1 = 0） and （a**4*b**2 + a**4*c**2 + a**2*b**4 + 2*a**2*b**2*c**2 - a**2*b**2 + a**2*c**4 - a**2*c**2 + b**4 + 2*b**2*c**2 + c**4 >= 0 or a*b**2 + a*c**2 < 0）））））） or a**2 - 1 >= 0 and a <> 0 and c <> 0 and （a + 1 = 0 or a - 1 = 0 or b = 0） or 4*a**2 - b**4 - 2*b**2 - 1 >= 0 and a <> 0 and （a**2*b**4 - 6*a**2*b**2 + a**2 + b**6 + 2*b**4 + b**2 = 0 and a**2*b**3 - a**2*b - b**5 + b**3 <= 0 and （b**2*c - c >= 0 or b*c > 0） or a**2*b**4 - 6*a**2*b**2 + a**2 + b**6 + 2*b**4 + b**2 = 0 and a**2*b**3 - a**2*b - b**5 + b**3 <= 0 and （b**2*c - c <= 0 or b*c <= 0） or a**2*b**4 - 6*a**2*b**2 + a**2 + b**6 + 2*b**4 + b**2 = 0 and a**2*b**3 - a**2*b - b**5 + b**3 >= 0 and （b**2*c - c >= 0 or b*c < 0） or a**2*b**4 - 6*a**2*b**2 + a**2 + b**6 + 2*b**4 + b**2 = 0 and a**2*b**3 - a**2*b - b**5 + b**3 >= 0 and （b**2*c - c <= 0 or b*c >= 0）） and （a + b = 0 or a - b = 0） or a**2 - 1 >= 0 and a <> 0 and （a + 1 = 0 or a - 1 = 0 or b = 0） or （a <> 0 or b <> 0） and （a**2 + b**2 - 1 >= 0 or b = 0） and （（a**4 + a**2*b**2 - a**2 + b**2 >= 0 or a >= 0 and （a - 1 = 0 or a = 0 and b = 0）） and （（3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0） or a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0）） and （b*c > 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c <= 0） and （a*c < 0 or （b = 0 or c <= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0））） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0） or a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0）） and （b*c <= 0 or （b = 0 or c >= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0） or a*c >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c = 0）） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0） and （a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 < 0 or 3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0）） and （b*c < 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c <= 0） and （a*c < 0 or （b = 0 or c <= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0））） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0） and （a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 < 0 or 3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0）） and （b*c >= 0 or （b = 0 or c >= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0） or a*c >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c = 0））） or （a**4 + a**2*b**2 - a**2 + b**2 >= 0 or a <= 0 and （a + 1 = 0 or a = 0 and b = 0）） and （（3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0） or a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0）） and （b*c > 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c <= 0） and （a*c > 0 or （b = 0 or c <= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0））） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 >= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0） or a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0）） and （b*c <= 0 or （b = 0 or c >= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0） or a*c <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c = 0）） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0） and （a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 > 0 or 3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0）） and （b*c < 0 or （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c <= 0） and （a*c > 0 or （b = 0 or c <= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0））） or （3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 or a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0） and （a**5*b + a**3*b**3 - a**3*b + 3*a*b**3 > 0 or 3*a**4*b + 3*a**2*b**3 - 3*a**2*b + b**3 <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0）） and （b*c >= 0 or （b = 0 or c >= 0） and （a**4 + a**2*b**2 - a**2 - b**2 <= 0 or b = 0 or c = 0） or a*c <= 0 and （a**4 + a**2*b**2 - a**2 - b**2 >= 0 or b = 0 or c = 0）））） or a + b <> 0 and a - b <> 0 and （a**2 - b**2 - 1 <= 0 or b = 0） and （（a**4 - a**2*b**2 - a**2 - b**2 >= 0 or a - 1 = 0） and （（a**5 - a**3*b**2 - a**3 - a*b**2 <= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c > 0 or （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or a**2*c - b**2*c >= 0 or b = 0 or c = 0） and （a**3*c - a*b**2*c < 0 or （a**2*c - b**2*c >= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0））） or （a**5 - a**3*b**2 - a**3 - a*b**2 <= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c <= 0 or （a**2*c - b**2*c <= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0） or a**3*c - a*b**2*c >= 0 and （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or b = 0 or c = 0）） or （a**5 - a**3*b**2 - a**3 - a*b**2 <= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c < 0 or （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or a**2*c - b**2*c >= 0 or b = 0 or c = 0） and （a**3*c - a*b**2*c < 0 or （a**2*c - b**2*c >= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0））） or （a**5 - a**3*b**2 - a**3 - a*b**2 <= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c >= 0 or （a**2*c - b**2*c <= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0） or a**3*c - a*b**2*c >= 0 and （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or b = 0 or c = 0））） or （a**4 - a**2*b**2 - a**2 - b**2 >= 0 or a + 1 = 0） and （（a**5 - a**3*b**2 - a**3 - a*b**2 >= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c > 0 or （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or a**2*c - b**2*c >= 0 or b = 0 or c = 0） and （a**3*c - a*b**2*c > 0 or （a**2*c - b**2*c >= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0））） or （a**5 - a**3*b**2 - a**3 - a*b**2 >= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c <= 0 or （a**2*c - b**2*c <= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0） or a**3*c - a*b**2*c <= 0 and （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or b = 0 or c = 0）） or （a**5 - a**3*b**2 - a**3 - a*b**2 >= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c < 0 or （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or a**2*c - b**2*c >= 0 or b = 0 or c = 0） and （a**3*c - a*b**2*c > 0 or （a**2*c - b**2*c >= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0））） or （a**5 - a**3*b**2 - a**3 - a*b**2 >= 0 or b = 0） and （a + 1 = 0 or a - 1 = 0 or b = 0） and （b*c >= 0 or （a**2*c - b**2*c <= 0 or b = 0） and （a**4 - a**2*b**2 - a**2 + b**2 >= 0 or b = 0 or c = 0） or a**3*c - a*b**2*c <= 0 and （a**4 - a**2*b**2 - a**2 + b**2 <= 0 or b = 0 or c = 0）））） or a*b - b <= 0 and a - 1 = 0 and （a*c - c >= 0 or b*c > 0） or a*b - b <= 0 and a - 1 = 0 and （a*c - c <= 0 or b*c <= 0） or a*b - b >= 0 and a - 1 = 0 and （a*c - c >= 0 or b*c < 0） or a*b - b >= 0 and a - 1 = 0 and （a*c - c <= 0 or b*c >= 0） or a*b + b >= 0 and a + 1 = 0 and （a*c + c <= 0 or b*c > 0） or a*b + b >= 0 and a + 1 = 0 and （a*c + c >= 0 or b*c <= 0） or a*b + b <= 0 and a + 1 = 0 and （a*c + c <= 0 or b*c < 0） or a*b + b <= 0 and a + 1 = 0 and （a*c + c >= 0 or b*c >= 0）$
4: slfq f;
The input formula is: The OR of 22 things!
It contains 926 atomic formulas, nested to a depth of 13.
Variables are: b,c,a
Cutoff is 2
Simplifying disjunct number 1
4Subformula 1:
[ b /= 0 /\ c /= 0 /\ a^2 + b^2 - 1 >= 0 ]
Simplifying disjunct number 2
63Subformula 2:
[ c + b /= 0 /\ b^2 c^2 - c^2 + b^4 + b^2 = 0 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - b^4 = 0 ]
Simplifying disjunct number 3
76Subformula 3:
[ b /= 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
Simplifying disjunct number 4
81Subformula 4:
[ c /= 0 /\ [ a - 1 >= 0 \/ a + 1 <= 0 ] ]
Simplifying disjunct number 5
98Subformula 5:
FALSE
Simplifying disjunct number 6
185Subformula 6:
[ a^2 + b^2 - 1 >= 0 /\ [ b /= 0 \/ c /= 0 ] ]
Simplifying disjunct number 7
578Subformula 7:
[ b^2 c^2 - c^2 + b^4 + b^2 /= 0 /\ [ a - 1 = 0 \/ a + 1 = 0 \/ [ c > _root_-1 c^2 + b^2 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - c^2 - b^4 + b^2 > 0 ] \/ [ c < _root_-1 c^2 + b^2 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - c^2 - b^4 + b^2 > 0 ] \/ [ c = 0 /\ c^2 a^2 - b^2 a^2 - b^2 c^2 - c^2 - b^4 + b^2 <= 0 ] ] ]
Simplifying disjunct number 8
681Subformula 8:
[ a^2 + b^2 - 1 >= 0 /\ [ b /= 0 \/ c /= 0 ] ]
Simplifying disjunct number 9
1144Subformula 9:
[ c^2 + b^2 > 0 /\ a^2 + c^2 + b^2 - 1 >= 0 ]
Simplifying disjunct number 10
1155Subformula 10:
[ c /= 0 /\ [ a - 1 = 0 \/ a + 1 = 0 \/ [ b = 0 /\ a - 1 > 0 ] \/ [ b = 0 /\ a + 1 < 0 ] ] ]
Simplifying disjunct number 11
1194Subformula 11:
[ b - 1 <= 0 /\ b + 1 >= 0 /\ b^4 a^2 - 6 b^2 a^2 + a^2 + b^6 + 2 b^4 + b^2 = 0 /\ [ b - 1 = 0 \/ b + 1 = 0 ] ]
Simplifying disjunct number 12
1203Subformula 12:
[ a - 1 = 0 \/ a + 1 = 0 \/ [ b = 0 /\ a - 1 > 0 ] \/ [ b = 0 /\ a + 1 < 0 ] ]
Simplifying disjunct number 13
1492Subformula 13:
a^2 + b^2 - 1 >= 0
Simplifying disjunct number 14
1755Subformula 14:
[ b + 1 /= 0 /\ b - 1 /= 0 /\ [ a - 1 = 0 \/ a + 1 = 0 \/ [ b = 0 /\ a - 1 > 0 ] \/ [ b = 0 /\ a + 1 < 0 ] ] ]
Simplifying disjunct number 15
1762Subformula 15:
a - 1 = 0
Simplifying disjunct number 16
1769Subformula 16:
a - 1 = 0
Simplifying disjunct number 17
1776Subformula 17:
a - 1 = 0
Simplifying disjunct number 18
1783Subformula 18:
a - 1 = 0
Simplifying disjunct number 19
1790Subformula 19:
a + 1 = 0
Simplifying disjunct number 20
1797Subformula 20:
a + 1 = 0
Simplifying disjunct number 21
1804Subformula 21:
a + 1 = 0
Simplifying disjunct number 22
1811Subformula 22:
a + 1 = 0
1831
===================== The End =======================

-

32 Garbage collections, 75891976 Cells and 3 Arrays reclaimed, in 2105 milliseconds.
1560286 Cells in AVAIL, 2500000 Cells in SPACE.
System time: 27151 milliseconds.
System time after the initialization: 27142 milliseconds.

-

An equivalent formula is:
a^2 + c^2 + b^2 - 1 >= 0
There were 1832 QEPCADB calls!
There were 1832 QEPCADB calls!

a^2 + c^2 + b^2 - 1 >= 0

実行は見ての通りReduce上から，例によって自作の関数slfqによるものですが，ファイルに書き出すとしてもその働きを鑑みれば手間ではないと思います．

起動オプションなどは

slfq -h

で参照できます．

（書き忘れていましたが，QEPCAD Bのヘルプはソースファイルを見るか，対話モードのBefore Normalization以降のフェーズでhelpと入力するとコマンドの一覧が表示されます．）

なお作者のBrown教授はスイッチをお付けになるご予定の様ですが，現時点のSLFQの出力には前回述べた拡張タルスキー論理式が利用され，そのままではReduceに取り込むとエラーとなることがありますので，上記拙作slfq関数ではこの点も改良しています．