>>36
通常、「自動証明」というのは人間にとっても意味のある定理を
証明することを目標にする

この場合は、人間にとって自明な命題を証明できればいい

厳密には区別できないが、そいうことだ