Без заголовка

Если вы формализовали критерии "по образу и подобию", то можете попробовать и такую сеть. Но смысла в ней нет. Вычислительные затраты на генерацию по аксиоматике практически ничтожны по сравнению с затратами на доказательство, а для каждой рассматриваемой теории заведомо потребуется либо одно, либо другое. Сеть здесь пригодна только для выбора стратегий, какие комбинации преобразований пробовать в первую очередь, etc. Если дана мотивация, разумеется.