1 sort bitvec 1
2 input 1 @inp2
3 sort bitvec 31
4 input 3 @inp4
5 sort bitvec 32
6 concat 5 2 4
7 constd 5 103
8 eq 1 6 7
9 slice 1 7 31 31
10 slice 3 7 30 0
11 eq 1 2 9
12 eq 1 4 10
13 and 1 11 12
14 eq 1 8 13
15 constraint -14