Как преобразовать формулу в дизъюнктивную нормальную форму?

Скажем, учитывая формулу

(t1>=2 или t2>=3 )и (t3>=1)

Я хочу получить его дизъюнктивную нормальную форму (t1>=2 и t3>=1 )или (t2>=3 и t3>=1)

Как добиться этого в Z3?