1 sort bitvec 32
2 constd 1 97
3 input 1 @inp3
4 add 1 2 3
5 sort bitvec 1
6 eq 5 -3 -4
7 eq 5 -4 -3
8 or 5 6 7
9 constraint 8