Преобразование пропозициональных

Рисунок 16. 8. Преобразование пропозициональных формул в множество
дизъюнктов с записью их в базу данных при помощи assert.

?- транс( ~(( а=>b) & ( b=>c) => ( а=>с)) ), пуск.

Ответ программы "Обнаружено противоречие" будет означать, что исходная формула является теоремой.