1 sort bitvec 8
2 const 1 01000101
3 const 1 10101010
4 zero 1
5 input 1 @inp5
6 and 1 2 5
7 and 1 6 3
8 and 1 4 5
9 sort bitvec 1
10 eq 9 7 8
11 and 1 2 5
12 and 1 3 6
13 eq 9 12 8
14 or 9 -10 -13
15 constraint 14