1 sort bitvec 1
2 const 1 0
3 sort bitvec 6
4 const 3 000000
5 sort bitvec 5
6 const 5 00000
7 input 1 @inp7
8 input 5 @inp8
9 concat 3 8 -7
10 concat 3 6 -7
11 concat 3 8 2
12 and 3 10 11
13 and 3 9 -12
14 eq 1 4 13
15 constraint -14