>>379
証明器によると思う。よく知らない。
ただ、計算量は指数的に膨れ上がる事が知られており、自動証明可能なものであっても、
現実的な時間内には終わらないこともある。
そもそも、自動証明では記述できる命題が限られるため、証明支援器 (377の3.)を用いて、
部分的に自動化する方法が最も現実的である。