1 sort bitvec 4 2 input 1 @inp2 3 input 1 @inp3 4 input 1 @inp4 5 mul 1 2 3 6 mul 1 2 4 7 sort bitvec 1 8 eq 7 5 6 9 eq 7 3 4 10 eq 7 8 9 11 constraint -10