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