1 sort bitvec 32
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 add 1 2 3
6 add 1 5 4
7 add 1 3 4
8 add 1 2 7
9 sort bitvec 1
10 input 9 @inp10
11 ite 1 10 6 -8
12 constraint 11