1 sort bitvec 1 2 input 1 @inp2 3 input 1 @inp3 4 add 1 2 3 5 xor 1 2 3 6 eq 1 4 5 7 constraint -6