1 sort bitvec 1 2 zero 1 3 input 1 @inp3 4 eq 1 -2 3 5 input 1 @inp5 6 input 1 @inp6 7 eq 1 6 3 8 and 1 5 -7 9 and 1 4 -8 10 eq 1 6 2 11 and 1 9 10 12 eq 1 3 2 13 and 1 5 -12 14 and 1 11 -13 15 constraint 14