Loading ARI120=1.p ...
Warning: introducing partial function "nonLinMult" to encode multiplication
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading ARI496=1.p ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading ARI595=1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading ARI616=1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading ARI620=1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading GEG021=1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading PUZ001+1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading PUZ133=2.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading SYN050-1.p ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading SYO561_1.p ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading SYO563+1.p ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading SYO563+2.p ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

