もっとも面倒くさい展開
・Corollary 3.12は集合論では決定不能
・のみならずそもそもABC予想自体が集合論では決定不能

一番目が成り立つとして、そこから二番目を導くには、
Corollary 3.12の否定からABC予想の否定を導く必要がある