1 sort bitvec 4
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 sort bitvec 8
6 concat 5 2 3
7 concat 5 2 4
8 sort bitvec 1
9 ult 8 -6 -7
10 ult 8 -3 -4
11 neq 8 9 10
12 constraint 11