1 sort bitvec 8 2 input 1 @inp2 3 input 1 @inp3 4 sort bitvec 1 5 ugte 4 2 3 6 ugte 4 3 2 7 and 4 5 6 8 eq 4 2 3 9 and 4 7 -8 10 constraint 9