Контрпример вывода Z3

Когда формула в Z3 не задана и указано (get-proof), есть результат, о котором я не нахожу никакой информации. Где я могу найти какую-либо документацию по этому поводу?

Мне кажется совершенно нечитаемым, есть ли какой-нибудь инструмент, который принимает это в качестве входных данных?

Ура, Matt