Fix benchmark for SPLIT_TICKET

The protocol model for the SPLIT_TICKET instruction is linear in the max size of the two nat inputs. The benchmark model also has an (apparently unused) N_ISplit_ticket_cmp_coeff parameter. The benchmark should probably be simplified.