1 sort bitvec 8
2 const 1 11111111
3 input 1 @inp3
4 add 1 -2 3
5 sort bitvec 1
6 eq 5 3 4
7 constraint 6