nnssdn 二重否定の利用

次の不等式を簡約します．

(%i90) f:x^3+y^3+z^3>=3*x*y*z;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.859 KB.
(%o90) z^3+y^3+x^3 >= 3*x*y*z

まずは，qepmax から．．．．

(%i91) qe([],f);
Evaluation took 0.0800 seconds (0.2700 elapsed) using 1.674 MB.
(%o91) (z+y+x >= 0) %or (z^2-y*z-x*z+y^2-x*y+x^2 = 0)

一方，nnss は．．．．いい感じです．

(%i92) nnss(f);
Evaluation took 1.4100 seconds (5.1900 elapsed) using 59.782 MB.
(%o92) ((y-x = 0) %and (z-x = 0)) %or (z+y+x >= 0)

では，次はどうでしょう．

(%i93) g:x^3+y^3+z^3>3*x*y*z;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.859 KB.
(%o93) z^3+y^3+x^3 > 3*x*y*z
(%i94) qe([],g);
Evaluation took 0.0700 seconds (0.2900 elapsed) using 1.510 MB.
(%o94) (z+y+x > 0) %and (z^2-y*z-x*z+y^2-x*y+x^2 > 0)
(%i95) nnss(g);
Evaluation took 1.6900 seconds (3.7200 elapsed) using 92.056 MB.
(%o95) (z+y+x > 0) %and (z^2-y*z-x*z+y^2-x*y+x^2 > 0)

共倒れです．．．．ということで，nnssdn の出番です．

(%i96) nnssdn(g);
Evaluation took 1.8000 seconds (5.7800 elapsed) using 78.075 MB.
(%o96) ((y-x # 0) %or (z-x # 0)) %and (z+y+x > 0)

勿論，万能ではありません．

(%i97) nnssdn(f);
Evaluation took 2.5600 seconds (4.8100 elapsed) using 147.524 MB.
(%o97) (z+y+x >= 0) %or (z^2-y*z-x*z+y^2-x*y+x^2 = 0)