東ロボくんのこと（６）VS+GB+SNCAD

ニュースの画像をあらためて観たのですが，東ロボくんはSyNRACに実装されているSNCADを使っていました．それは．．．
http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CCoQFjAA&url=http%3A%2F%2Fgcoe-mi.jp%2Ftemp%2Fpublish%2F5013c35d964cdb4b1199a720b14e3662.pdf&ei=6-qeUsbLAuKdigKF3YH4Bw&usg=AFQjCNFjRocvjP3xhPM1W2kjTIh71wZwzw&sig2=RnIv0goBlVoSxBnw3v-hTQ&bvm=bv.57155469,d.cGE

CADについてはこのブログでもいろいろ書いています．
http://d.hatena.ne.jp/ehito/20110610/1307697873

ちなみに，現在公開されているSyNRACに，例えば

 qe(Ex([x, y], And(-a < 0, a-y <= 0, -2*a+y <= 0, x*y <> 0, g*x*y+x^2*y^2-x^2-y^2 = 0, -2*x <= -1, x <= 1)));

と尋ねても

error found. [SyNRAC:-qe] @ syn_lift_p
Error, (in SyNRAC:-qe) qe, cannot determine if this expression is true or false: %1, floor(ln(4294967299/4294967296)/ln(2)) < 0

と返します．