1 sort bitvec 8 2 constd 1 1 3 input 1 @inp3 4 mul 1 2 3 5 sort bitvec 1 6 eq 5 3 4 7 constraint 6