機械判定にかけるってことは論理、言語、非論理公理をfixするってことだよね？　それ公開して欲しい
でもしないだろうな　延命目的だろうから