1 sort bitvec 8
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 input 1 @inp5
6 sort bitvec 16
7 concat 6 2 3
8 concat 6 4 5
9 sort bitvec 32
10 concat 9 7 8
11 concat 6 2 3
12 sort bitvec 24
13 concat 12 11 4
14 concat 9 13 5
15 sort bitvec 1
16 neq 15 10 14
17 constraint 16