>>42
矛盾してるな。

２０万行を数千行に圧縮するには、
圧縮された証明の行間を埋められる
程度に賢い自動証明が不可欠。

述語論理の充足可能性の非決定性の壁を
突破しろなんて誰もいっちゃあいない。