QEPCAD B は6変数くらいでも扱いきれなくなるのか。 もうちょっとはいくんじゃないかと思ってたけど、CADによる量化子除去って想像以上にスケールしないんだなぁ。 まあ、double exponential なので仕方ないけれど。 http://www.jssac.org/Editor/Suushiki/V10/No1/V10N1_103.pdf