1 sort bitvec 47 2 input 1 @inp2 3 input 1 @inp3 4 add 1 2 3 5 sort bitvec 1 6 eq 5 2 4 7 eq 5 4 2 8 zero 1 9 eq 5 3 8 10 eq 5 6 9 11 eq 5 7 9 12 or 5 -10 -11 13 constraint 12