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

No countermodel exists, formula is valid

Loading vstte-problem-2-vc.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

