1 sort bitvec 1 2 input 1 @inp2 3 input 1 @inp3 4 eq 1 2 3 5 constraint 4