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