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