Loading PUZ031p1.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

