CADによる量化子除去のすごく簡単なやつを実装してみて、ようやく実閉体の理論の完全性と決定可能性の実感がわいてきた。