import z3
import struct
from more_itertools import chunked

# Create license

# license is 20 bytes
# we do not model the given - of XXXXX-XXXXX-XXXXX-XXXXX
# This will be consistent for all comments
license = [<TODO> for i in range(20)]

s = z3.Solver()

# General license format constraints:
#  Each character is either 0-9 or A-Z

## TODO


## bin1 constraints
# after performing sort on the license key
# it will be: 067889BBCKKMOPPUVWYY
# I.e. the license key is made up out of exactly these characters


## bin2 
# sums of numbers and capital chars
# For each set of 5 characters in the XXXXX-XXXXX-XXXXX-XXXXX license code,
# the numbers are summed together and compared
# same for the characters A-Z, where A represents 0, B represents 1, 
#  ... and Z represents 25
# The arrays below already have the correct sums
number_sums      = [  0,  7, 0xE, 0x11 ]
char_sums        = [ 61, 36,  44, 0x32 ]

## bin3
# bin3 will for each byte at license [i] in the license code
# get the index with strchr and then license[i+1] is allowed
# to only contain values that are in the 0x18 4-byte ints
# in the array starting at idx * 0x60 (note: 0x18*4 = 60)
# strchr of ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789
# Please keep in mind: this was a binary with a big-endian architecture
#  the given u32 will unpack a 4-byte big-endian value if given 4 bytes
allowed_chars = "ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"
bin3_allow_array = b'\x00\x00\x00H\x00\x00\x00O\x00\x00\x00W\x00\x00\x00F\x00\x00\x00M\x00\x00\x002\x00\x00\x00A\x00\x00\x001\x00\x00\x00T\x00\x00\x00E\x00\x00\x00S\x00\x00\x00X\x00\x00\x000\x00\x00\x00K\x00\x00\x00C\x00\x00\x00Q\x00\x00\x005\x00\x00\x00B\x00\x00\x00Y\x00\x00\x00D\x00\x00\x00J\x00\x00\x007\x00\x00\x00P\x00\x00\x008\x00\x00\x003\x00\x00\x00D\x00\x00\x00Z\x00\x00\x00J\x00\x00\x00H\x00\x00\x00B\x00\x00\x002\x00\x00\x00U\x00\x00\x00O\x00\x00\x00S\x00\x00\x009\x00\x00\x00M\x00\x00\x00T\x00\x00\x008\x00\x00\x00L\x00\x00\x00N\x00\x00\x00W\x00\x00\x00K\x00\x00\x00E\x00\x00\x00F\x00\x00\x00V\x00\x00\x006\x00\x00\x00I\x00\x00\x007\x00\x00\x00N\x00\x00\x00A\x00\x00\x00K\x00\x00\x001\x00\x00\x00L\x00\x00\x00Q\x00\x00\x00H\x00\x00\x00X\x00\x00\x00U\x00\x00\x00O\x00\x00\x00W\x00\x00\x00Z\x00\x00\x006\x00\x00\x00E\x00\x00\x00D\x00\x00\x009\x00\x00\x00R\x00\x00\x00S\x00\x00\x000\x00\x00\x00B\x00\x00\x00J\x00\x00\x007\x00\x00\x00T\x00\x00\x005\x00\x00\x00H\x00\x00\x009\x00\x00\x00O\x00\x00\x00J\x00\x00\x00V\x00\x00\x006\x00\x00\x00M\x00\x00\x001\x00\x00\x00S\x00\x00\x00A\x00\x00\x00P\x00\x00\x00C\x00\x00\x005\x00\x00\x00G\x00\x00\x00W\x00\x00\x000\x00\x00\x00U\x00\x00\x00E\x00\x00\x008\x00\x00\x00I\x00\x00\x00Z\x00\x00\x00Y\x00\x00\x00Q\x00\x00\x00N\x00\x00\x00W\x00\x00\x009\x00\x00\x00V\x00\x00\x00U\x00\x00\x004\x00\x00\x006\x00\x00\x00I\x00\x00\x00F\x00\x00\x00Y\x00\x00\x00P\x00\x00\x00N\x00\x00\x00J\x00\x00\x00X\x00\x00\x00O\x00\x00\x002\x00\x00\x00C\x00\x00\x00A\x00\x00\x001\x00\x00\x007\x00\x00\x00K\x00\x00\x00G\x00\x00\x000\x00\x00\x00D\x00\x00\x00M\x00\x00\x00H\x00\x00\x009\x00\x00\x00M\x00\x00\x00Q\x00\x00\x00F\x00\x00\x001\x00\x00\x00W\x00\x00\x00G\x00\x00\x00V\x00\x00\x000\x00\x00\x00C\x00\x00\x00N\x00\x00\x00I\x00\x00\x008\x00\x00\x00B\x00\x00\x00A\x00\x00\x00L\x00\x00\x00U\x00\x00\x00X\x00\x00\x00S\x00\x00\x00D\x00\x00\x00R\x00\x00\x00Z\x00\x00\x003\x00\x00\x007\x00\x00\x001\x00\x00\x003\x00\x00\x008\x00\x00\x00U\x00\x00\x00S\x00\x00\x005\x00\x00\x00D\x00\x00\x00J\x00\x00\x00M\x00\x00\x00N\x00\x00\x00L\x00\x00\x00X\x00\x00\x00I\x00\x00\x00G\x00\x00\x00T\x00\x00\x00Y\x00\x00\x006\x00\x00\x000\x00\x00\x00W\x00\x00\x00Z\x00\x00\x00P\x00\x00\x004\x00\x00\x009\x00\x00\x001\x00\x00\x004\x00\x00\x003\x00\x00\x006\x00\x00\x008\x00\x00\x00M\x00\x00\x00D\x00\x00\x00V\x00\x00\x00J\x00\x00\x00N\x00\x00\x00R\x00\x00\x00I\x00\x00\x005\x00\x00\x00O\x00\x00\x002\x00\x00\x00S\x00\x00\x00L\x00\x00\x00H\x00\x00\x00U\x00\x00\x00X\x00\x00\x00B\x00\x00\x00Z\x00\x00\x000\x00\x00\x00C\x00\x00\x00H\x00\x00\x001\x00\x00\x00I\x00\x00\x004\x00\x00\x00Y\x00\x00\x00L\x00\x00\x00Z\x00\x00\x00A\x00\x00\x002\x00\x00\x00U\x00\x00\x005\x00\x00\x00D\x00\x00\x009\x00\x00\x00C\x00\x00\x00G\x00\x00\x007\x00\x00\x00J\x00\x00\x00F\x00\x00\x00M\x00\x00\x00X\x00\x00\x00B\x00\x00\x00Q\x00\x00\x00S\x00\x00\x000\x00\x00\x009\x00\x00\x00H\x00\x00\x00G\x00\x00\x00Y\x00\x00\x00O\x00\x00\x006\x00\x00\x001\x00\x00\x007\x00\x00\x00Z\x00\x00\x000\x00\x00\x00F\x00\x00\x00U\x00\x00\x00L\x00\x00\x00V\x00\x00\x00E\x00\x00\x00P\x00\x00\x00S\x00\x00\x00J\x00\x00\x00A\x00\x00\x00X\x00\x00\x00R\x00\x00\x00B\x00\x00\x00W\x00\x00\x00Q\x00\x00\x005\x00\x00\x00T\x00\x00\x00W\x00\x00\x001\x00\x00\x00A\x00\x00\x00P\x00\x00\x008\x00\x00\x00M\x00\x00\x00F\x00\x00\x00D\x00\x00\x006\x00\x00\x00O\x00\x00\x00K\x00\x00\x00J\x00\x00\x00C\x00\x00\x000\x00\x00\x00Q\x00\x00\x00B\x00\x00\x00H\x00\x00\x00I\x00\x00\x002\x00\x00\x00E\x00\x00\x009\x00\x00\x004\x00\x00\x00J\x00\x00\x00D\x00\x00\x00Z\x00\x00\x00R\x00\x00\x006\x00\x00\x00O\x00\x00\x00A\x00\x00\x00W\x00\x00\x003\x00\x00\x001\x00\x00\x00B\x00\x00\x009\x00\x00\x00H\x00\x00\x00G\x00\x00\x002\x00\x00\x007\x00\x00\x00X\x00\x00\x00Y\x00\x00\x00V\x00\x00\x00N\x00\x00\x00E\x00\x00\x00U\x00\x00\x008\x00\x00\x00F\x00\x00\x000\x00\x00\x00E\x00\x00\x00V\x00\x00\x009\x00\x00\x00Y\x00\x00\x00D\x00\x00\x008\x00\x00\x00Q\x00\x00\x005\x00\x00\x00P\x00\x00\x00Z\x00\x00\x00N\x00\x00\x00B\x00\x00\x00G\x00\x00\x00U\x00\x00\x001\x00\x00\x00M\x00\x00\x00X\x00\x00\x00T\x00\x00\x003\x00\x00\x00I\x00\x00\x00A\x00\x00\x00C\x00\x00\x00W\x00\x00\x00G\x00\x00\x00H\x00\x00\x00V\x00\x00\x008\x00\x00\x00T\x00\x00\x00Y\x00\x00\x005\x00\x00\x00I\x00\x00\x00A\x00\x00\x00J\x00\x00\x00C\x00\x00\x00X\x00\x00\x00N\x00\x00\x00U\x00\x00\x00O\x00\x00\x003\x00\x00\x004\x00\x00\x001\x00\x00\x00R\x00\x00\x00P\x00\x00\x00K\x00\x00\x002\x00\x00\x00L\x00\x00\x00M\x00\x00\x00B\x00\x00\x00O\x00\x00\x00W\x00\x00\x00M\x00\x00\x007\x00\x00\x008\x00\x00\x004\x00\x00\x00K\x00\x00\x000\x00\x00\x00U\x00\x00\x00R\x00\x00\x002\x00\x00\x00L\x00\x00\x00J\x00\x00\x001\x00\x00\x00Y\x00\x00\x00P\x00\x00\x00E\x00\x00\x00I\x00\x00\x00V\x00\x00\x00A\x00\x00\x00S\x00\x00\x006\x00\x00\x009\x00\x00\x00F\x00\x00\x004\x00\x00\x000\x00\x00\x007\x00\x00\x008\x00\x00\x00G\x00\x00\x00N\x00\x00\x00B\x00\x00\x00Z\x00\x00\x00E\x00\x00\x00M\x00\x00\x005\x00\x00\x00C\x00\x00\x009\x00\x00\x00D\x00\x00\x00H\x00\x00\x001\x00\x00\x00P\x00\x00\x00U\x00\x00\x00L\x00\x00\x00I\x00\x00\x00T\x00\x00\x00A\x00\x00\x00V\x00\x00\x00T\x00\x00\x00I\x00\x00\x00X\x00\x00\x00P\x00\x00\x00V\x00\x00\x008\x00\x00\x00R\x00\x00\x001\x00\x00\x005\x00\x00\x007\x00\x00\x00N\x00\x00\x00J\x00\x00\x00L\x00\x00\x006\x00\x00\x00E\x00\x00\x00Y\x00\x00\x00B\x00\x00\x00D\x00\x00\x00U\x00\x00\x00F\x00\x00\x00O\x00\x00\x00W\x00\x00\x00M\x00\x00\x00G\x00\x00\x00B\x00\x00\x00H\x00\x00\x00S\x00\x00\x00O\x00\x00\x000\x00\x00\x00F\x00\x00\x00V\x00\x00\x00Z\x00\x00\x00E\x00\x00\x005\x00\x00\x004\x00\x00\x00Y\x00\x00\x006\x00\x00\x009\x00\x00\x00Q\x00\x00\x00R\x00\x00\x001\x00\x00\x00D\x00\x00\x00I\x00\x00\x003\x00\x00\x00M\x00\x00\x00P\x00\x00\x00G\x00\x00\x00U\x00\x00\x00Q\x00\x00\x008\x00\x00\x002\x00\x00\x00J\x00\x00\x00X\x00\x00\x00T\x00\x00\x00V\x00\x00\x000\x00\x00\x00W\x00\x00\x007\x00\x00\x004\x00\x00\x00A\x00\x00\x00S\x00\x00\x00Y\x00\x00\x003\x00\x00\x00U\x00\x00\x00R\x00\x00\x00O\x00\x00\x00G\x00\x00\x00Z\x00\x00\x00F\x00\x00\x00B\x00\x00\x005\x00\x00\x00E\x00\x00\x00O\x00\x00\x00E\x00\x00\x007\x00\x00\x00Z\x00\x00\x00K\x00\x00\x003\x00\x00\x00G\x00\x00\x00U\x00\x00\x00P\x00\x00\x00Y\x00\x00\x00T\x00\x00\x00W\x00\x00\x00A\x00\x00\x00F\x00\x00\x00J\x00\x00\x00X\x00\x00\x004\x00\x00\x00I\x00\x00\x002\x00\x00\x00R\x00\x00\x00Q\x00\x00\x00L\x00\x00\x00N\x00\x00\x009\x00\x00\x00N\x00\x00\x00E\x00\x00\x00J\x00\x00\x00H\x00\x00\x00C\x00\x00\x001\x00\x00\x00O\x00\x00\x00F\x00\x00\x00S\x00\x00\x00B\x00\x00\x00M\x00\x00\x00I\x00\x00\x00D\x00\x00\x00U\x00\x00\x003\x00\x00\x00P\x00\x00\x00V\x00\x00\x002\x00\x00\x007\x00\x00\x00Q\x00\x00\x009\x00\x00\x006\x00\x00\x00Y\x00\x00\x00W\x00\x00\x00T\x00\x00\x00M\x00\x00\x00B\x00\x00\x00J\x00\x00\x009\x00\x00\x005\x00\x00\x00Z\x00\x00\x00I\x00\x00\x00S\x00\x00\x00Q\x00\x00\x000\x00\x00\x00L\x00\x00\x004\x00\x00\x00Y\x00\x00\x00W\x00\x00\x00K\x00\x00\x00V\x00\x00\x00N\x00\x00\x007\x00\x00\x00U\x00\x00\x00C\x00\x00\x002\x00\x00\x00F\x00\x00\x006\x00\x00\x00S\x00\x00\x006\x00\x00\x00Z\x00\x00\x00H\x00\x00\x00Q\x00\x00\x004\x00\x00\x00C\x00\x00\x00Y\x00\x00\x00M\x00\x00\x00D\x00\x00\x003\x00\x00\x009\x00\x00\x000\x00\x00\x00E\x00\x00\x008\x00\x00\x00B\x00\x00\x00A\x00\x00\x00O\x00\x00\x00K\x00\x00\x00N\x00\x00\x00V\x00\x00\x00F\x00\x00\x007\x00\x00\x00J\x00\x00\x00X\x00\x00\x006\x00\x00\x005\x00\x00\x009\x00\x00\x00Z\x00\x00\x007\x00\x00\x003\x00\x00\x00M\x00\x00\x00C\x00\x00\x00D\x00\x00\x00I\x00\x00\x00N\x00\x00\x00O\x00\x00\x00K\x00\x00\x004\x00\x00\x00T\x00\x00\x00J\x00\x00\x00F\x00\x00\x001\x00\x00\x00G\x00\x00\x00S\x00\x00\x00W\x00\x00\x00H\x00\x00\x00E\x00\x00\x00L\x00\x00\x00G\x00\x00\x004\x00\x00\x00E\x00\x00\x002\x00\x00\x006\x00\x00\x005\x00\x00\x00F\x00\x00\x00X\x00\x00\x008\x00\x00\x00N\x00\x00\x00V\x00\x00\x00Z\x00\x00\x00I\x00\x00\x009\x00\x00\x00T\x00\x00\x00S\x00\x00\x00C\x00\x00\x003\x00\x00\x00K\x00\x00\x00P\x00\x00\x007\x00\x00\x00H\x00\x00\x00D\x00\x00\x004\x00\x00\x00R\x00\x00\x00D\x00\x00\x002\x00\x00\x00S\x00\x00\x00N\x00\x00\x00J\x00\x00\x00A\x00\x00\x008\x00\x00\x005\x00\x00\x00O\x00\x00\x00I\x00\x00\x006\x00\x00\x009\x00\x00\x00L\x00\x00\x00X\x00\x00\x00C\x00\x00\x00T\x00\x00\x00E\x00\x00\x00P\x00\x00\x007\x00\x00\x00W\x00\x00\x00M\x00\x00\x001\x00\x00\x00M\x00\x00\x00T\x00\x00\x00G\x00\x00\x00K\x00\x00\x000\x00\x00\x00Q\x00\x00\x003\x00\x00\x005\x00\x00\x00Z\x00\x00\x00W\x00\x00\x00R\x00\x00\x00A\x00\x00\x00E\x00\x00\x00P\x00\x00\x00V\x00\x00\x00F\x00\x00\x00J\x00\x00\x00H\x00\x00\x00Y\x00\x00\x002\x00\x00\x00S\x00\x00\x00X\x00\x00\x00L\x00\x00\x00D\x00\x00\x00D\x00\x00\x00Z\x00\x00\x00C\x00\x00\x00I\x00\x00\x00T\x00\x00\x007\x00\x00\x00W\x00\x00\x00M\x00\x00\x00K\x00\x00\x00N\x00\x00\x002\x00\x00\x00F\x00\x00\x000\x00\x00\x00R\x00\x00\x003\x00\x00\x00P\x00\x00\x00Y\x00\x00\x00Q\x00\x00\x00O\x00\x00\x00S\x00\x00\x00E\x00\x00\x001\x00\x00\x006\x00\x00\x009\x00\x00\x00U\x00\x00\x00T\x00\x00\x00C\x00\x00\x00O\x00\x00\x006\x00\x00\x00V\x00\x00\x00W\x00\x00\x00X\x00\x00\x00G\x00\x00\x00Y\x00\x00\x000\x00\x00\x008\x00\x00\x002\x00\x00\x00J\x00\x00\x00A\x00\x00\x00M\x00\x00\x00Z\x00\x00\x00K\x00\x00\x005\x00\x00\x001\x00\x00\x003\x00\x00\x00F\x00\x00\x00B\x00\x00\x00E\x00\x00\x000\x00\x00\x00A\x00\x00\x00G\x00\x00\x00E\x00\x00\x00D\x00\x00\x006\x00\x00\x00I\x00\x00\x00R\x00\x00\x00Z\x00\x00\x00H\x00\x00\x00O\x00\x00\x00V\x00\x00\x00T\x00\x00\x00W\x00\x00\x001\x00\x00\x00N\x00\x00\x00Q\x00\x00\x00J\x00\x00\x00S\x00\x00\x00M\x00\x00\x00P\x00\x00\x00X\x00\x00\x002\x00\x00\x00F\x00\x00\x00N\x00\x00\x00H\x00\x00\x00J\x00\x00\x009\x00\x00\x00G\x00\x00\x002\x00\x00\x00V\x00\x00\x007\x00\x00\x00L\x00\x00\x00K\x00\x00\x00Y\x00\x00\x00I\x00\x00\x003\x00\x00\x00D\x00\x00\x00M\x00\x00\x00R\x00\x00\x00P\x00\x00\x00C\x00\x00\x00T\x00\x00\x004\x00\x00\x00X\x00\x00\x008\x00\x00\x00A\x00\x00\x005\x00\x00\x005\x00\x00\x002\x00\x00\x00Q\x00\x00\x003\x00\x00\x00Y\x00\x00\x007\x00\x00\x00J\x00\x00\x00Z\x00\x00\x00P\x00\x00\x00X\x00\x00\x00D\x00\x00\x00L\x00\x00\x00F\x00\x00\x00B\x00\x00\x008\x00\x00\x009\x00\x00\x00U\x00\x00\x00K\x00\x00\x00G\x00\x00\x00E\x00\x00\x00O\x00\x00\x00V\x00\x00\x00H\x00\x00\x000\x00\x00\x007\x00\x00\x00S\x00\x00\x000\x00\x00\x00B\x00\x00\x00A\x00\x00\x00D\x00\x00\x00P\x00\x00\x00J\x00\x00\x003\x00\x00\x00U\x00\x00\x00F\x00\x00\x00I\x00\x00\x00X\x00\x00\x004\x00\x00\x00H\x00\x00\x009\x00\x00\x00T\x00\x00\x005\x00\x00\x00O\x00\x00\x00Y\x00\x00\x00E\x00\x00\x00G\x00\x00\x00K\x00\x00\x00R\x00\x00\x00V\x00\x00\x00R\x00\x00\x00L\x00\x00\x00F\x00\x00\x00U\x00\x00\x00H\x00\x00\x005\x00\x00\x00J\x00\x00\x00K\x00\x00\x00S\x00\x00\x00N\x00\x00\x00B\x00\x00\x00E\x00\x00\x00W\x00\x00\x006\x00\x00\x00I\x00\x00\x00X\x00\x00\x00C\x00\x00\x00A\x00\x00\x007\x00\x00\x00T\x00\x00\x004\x00\x00\x00Z\x00\x00\x00P\x00\x00\x00Y\x00\x00\x00Z\x00\x00\x00S\x00\x00\x004\x00\x00\x006\x00\x00\x00W\x00\x00\x00K\x00\x00\x00V\x00\x00\x003\x00\x00\x00O\x00\x00\x00U\x00\x00\x005\x00\x00\x00R\x00\x00\x008\x00\x00\x00T\x00\x00\x00I\x00\x00\x00H\x00\x00\x00C\x00\x00\x001\x00\x00\x00D\x00\x00\x00A\x00\x00\x002\x00\x00\x00L\x00\x00\x000\x00\x00\x00G\x00\x00\x009\x00\x00\x00X\x00\x00\x00Z\x00\x00\x00I\x00\x00\x005\x00\x00\x00T\x00\x00\x00E\x00\x00\x00D\x00\x00\x003\x00\x00\x00J\x00\x00\x00C\x00\x00\x00U\x00\x00\x00S\x00\x00\x001\x00\x00\x00F\x00\x00\x00A\x00\x00\x00M\x00\x00\x007\x00\x00\x00R\x00\x00\x00V\x00\x00\x00B\x00\x00\x006\x00\x00\x00P'
u32 = lambda x: struct.unpack(">I", x)[0]



## bin4
# Please keep in mind: this was a binary with a little-endian architecture
#  the given u32 will unpack a 4-byte little-endian value if given 4 bytes
u32 = lambda x: struct.unpack("<i", x)[0]

## bin4.1
# For each 4-byte integer in the bin4_known_vals array:
#  if the value is not -1, then license[i] == bin4_known_vals[i]
# Keep in mind: The above formula treats bin4_known_vals as an integer array
bin4_known_vals = b'\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x59\x00\x00\x00\xff\xff\xff\xff\x4d\x00\x00\x00\x38\x00\x00\x00\xff\xff\xff\xff'

## bin4.2
# imply_array contains a list of 200 elements of the following data type:
# struct s {
#   int padding;
#   int match_val;
#   int imply_idx;
#   int imply_val;
# };
#
# for each byte in the license there are 10 of these entries
# the program will check for each byte b and the corresponding entries, the following constraint:
#   b == s.match_val implies license[s.imply_idx] == s.imply_val
bin4_imply_array = b'\x00\x00\x00\x00\x49\x00\x00\x00\x12\x00\x00\x00\x35\x00\x00\x00\x00\x00\x00\x00\x59\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x00\x00\x00\x00\x56\x00\x00\x00\x0e\x00\x00\x00\x55\x00\x00\x00\x00\x00\x00\x00\x4c\x00\x00\x00\x06\x00\x00\x00\x49\x00\x00\x00\x00\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x5a\x00\x00\x00\x00\x00\x00\x00\x37\x00\x00\x00\x03\x00\x00\x00\x57\x00\x00\x00\x00\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x49\x00\x00\x00\x00\x00\x00\x00\x58\x00\x00\x00\x08\x00\x00\x00\x33\x00\x00\x00\x00\x00\x00\x00\x37\x00\x00\x00\x0c\x00\x00\x00\x4d\x00\x00\x00\x00\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x43\x00\x00\x00\x01\x00\x00\x00\x4a\x00\x00\x00\x03\x00\x00\x00\x54\x00\x00\x00\x01\x00\x00\x00\x55\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x4c\x00\x00\x00\x02\x00\x00\x00\x47\x00\x00\x00\x01\x00\x00\x00\x56\x00\x00\x00\x12\x00\x00\x00\x36\x00\x00\x00\x01\x00\x00\x00\x44\x00\x00\x00\x0f\x00\x00\x00\x35\x00\x00\x00\x01\x00\x00\x00\x4d\x00\x00\x00\x05\x00\x00\x00\x4f\x00\x00\x00\x01\x00\x00\x00\x4d\x00\x00\x00\x0d\x00\x00\x00\x54\x00\x00\x00\x01\x00\x00\x00\x38\x00\x00\x00\x07\x00\x00\x00\x55\x00\x00\x00\x01\x00\x00\x00\x58\x00\x00\x00\x11\x00\x00\x00\x50\x00\x00\x00\x02\x00\x00\x00\x58\x00\x00\x00\x05\x00\x00\x00\x44\x00\x00\x00\x02\x00\x00\x00\x59\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x00\x00\x02\x00\x00\x00\x4d\x00\x00\x00\x03\x00\x00\x00\x56\x00\x00\x00\x02\x00\x00\x00\x59\x00\x00\x00\x0d\x00\x00\x00\x5a\x00\x00\x00\x02\x00\x00\x00\x47\x00\x00\x00\x0c\x00\x00\x00\x4f\x00\x00\x00\x02\x00\x00\x00\x45\x00\x00\x00\x13\x00\x00\x00\x57\x00\x00\x00\x02\x00\x00\x00\x31\x00\x00\x00\x07\x00\x00\x00\x58\x00\x00\x00\x02\x00\x00\x00\x46\x00\x00\x00\x08\x00\x00\x00\x46\x00\x00\x00\x02\x00\x00\x00\x45\x00\x00\x00\x01\x00\x00\x00\x55\x00\x00\x00\x02\x00\x00\x00\x52\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x03\x00\x00\x00\x44\x00\x00\x00\x13\x00\x00\x00\x50\x00\x00\x00\x03\x00\x00\x00\x39\x00\x00\x00\x01\x00\x00\x00\x58\x00\x00\x00\x03\x00\x00\x00\x4e\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x03\x00\x00\x00\x4c\x00\x00\x00\x09\x00\x00\x00\x52\x00\x00\x00\x03\x00\x00\x00\x45\x00\x00\x00\x0c\x00\x00\x00\x48\x00\x00\x00\x03\x00\x00\x00\x59\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x03\x00\x00\x00\x4a\x00\x00\x00\x06\x00\x00\x00\x41\x00\x00\x00\x03\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x30\x00\x00\x00\x03\x00\x00\x00\x52\x00\x00\x00\x08\x00\x00\x00\x38\x00\x00\x00\x03\x00\x00\x00\x56\x00\x00\x00\x07\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x39\x00\x00\x00\x00\x00\x00\x00\x42\x00\x00\x00\x04\x00\x00\x00\x4a\x00\x00\x00\x10\x00\x00\x00\x45\x00\x00\x00\x04\x00\x00\x00\x37\x00\x00\x00\x06\x00\x00\x00\x32\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x04\x00\x00\x00\x4a\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x04\x00\x00\x00\x33\x00\x00\x00\x08\x00\x00\x00\x54\x00\x00\x00\x04\x00\x00\x00\x33\x00\x00\x00\x01\x00\x00\x00\x54\x00\x00\x00\x04\x00\x00\x00\x4c\x00\x00\x00\x03\x00\x00\x00\x42\x00\x00\x00\x04\x00\x00\x00\x52\x00\x00\x00\x0d\x00\x00\x00\x48\x00\x00\x00\x04\x00\x00\x00\x32\x00\x00\x00\x0b\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x42\x00\x00\x00\x0b\x00\x00\x00\x56\x00\x00\x00\x05\x00\x00\x00\x4a\x00\x00\x00\x13\x00\x00\x00\x30\x00\x00\x00\x05\x00\x00\x00\x31\x00\x00\x00\x12\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x36\x00\x00\x00\x06\x00\x00\x00\x4d\x00\x00\x00\x05\x00\x00\x00\x54\x00\x00\x00\x00\x00\x00\x00\x44\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x0e\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x42\x00\x00\x00\x0f\x00\x00\x00\x4a\x00\x00\x00\x05\x00\x00\x00\x45\x00\x00\x00\x10\x00\x00\x00\x44\x00\x00\x00\x05\x00\x00\x00\x55\x00\x00\x00\x11\x00\x00\x00\x4c\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x06\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x32\x00\x00\x00\x06\x00\x00\x00\x46\x00\x00\x00\x13\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x4f\x00\x00\x00\x0d\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x53\x00\x00\x00\x0b\x00\x00\x00\x56\x00\x00\x00\x06\x00\x00\x00\x30\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x06\x00\x00\x00\x32\x00\x00\x00\x09\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x33\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x06\x00\x00\x00\x56\x00\x00\x00\x00\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x5a\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x06\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x44\x00\x00\x00\x07\x00\x00\x00\x58\x00\x00\x00\x12\x00\x00\x00\x38\x00\x00\x00\x07\x00\x00\x00\x31\x00\x00\x00\x0f\x00\x00\x00\x57\x00\x00\x00\x07\x00\x00\x00\x33\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x07\x00\x00\x00\x4f\x00\x00\x00\x0a\x00\x00\x00\x41\x00\x00\x00\x07\x00\x00\x00\x34\x00\x00\x00\x08\x00\x00\x00\x4a\x00\x00\x00\x07\x00\x00\x00\x46\x00\x00\x00\x11\x00\x00\x00\x55\x00\x00\x00\x07\x00\x00\x00\x39\x00\x00\x00\x05\x00\x00\x00\x34\x00\x00\x00\x07\x00\x00\x00\x52\x00\x00\x00\x06\x00\x00\x00\x51\x00\x00\x00\x07\x00\x00\x00\x55\x00\x00\x00\x0e\x00\x00\x00\x4e\x00\x00\x00\x07\x00\x00\x00\x4f\x00\x00\x00\x10\x00\x00\x00\x48\x00\x00\x00\x08\x00\x00\x00\x4e\x00\x00\x00\x0f\x00\x00\x00\x4b\x00\x00\x00\x08\x00\x00\x00\x33\x00\x00\x00\x12\x00\x00\x00\x54\x00\x00\x00\x08\x00\x00\x00\x34\x00\x00\x00\x0a\x00\x00\x00\x4f\x00\x00\x00\x08\x00\x00\x00\x38\x00\x00\x00\x11\x00\x00\x00\x39\x00\x00\x00\x08\x00\x00\x00\x56\x00\x00\x00\x0b\x00\x00\x00\x54\x00\x00\x00\x08\x00\x00\x00\x4d\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x08\x00\x00\x00\x43\x00\x00\x00\x10\x00\x00\x00\x58\x00\x00\x00\x08\x00\x00\x00\x34\x00\x00\x00\x0c\x00\x00\x00\x37\x00\x00\x00\x08\x00\x00\x00\x52\x00\x00\x00\x06\x00\x00\x00\x46\x00\x00\x00\x08\x00\x00\x00\x4e\x00\x00\x00\x0d\x00\x00\x00\x50\x00\x00\x00\x09\x00\x00\x00\x52\x00\x00\x00\x05\x00\x00\x00\x52\x00\x00\x00\x09\x00\x00\x00\x33\x00\x00\x00\x07\x00\x00\x00\x41\x00\x00\x00\x09\x00\x00\x00\x49\x00\x00\x00\x03\x00\x00\x00\x47\x00\x00\x00\x09\x00\x00\x00\x59\x00\x00\x00\x11\x00\x00\x00\x58\x00\x00\x00\x09\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x41\x00\x00\x00\x09\x00\x00\x00\x32\x00\x00\x00\x10\x00\x00\x00\x33\x00\x00\x00\x09\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x52\x00\x00\x00\x09\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x33\x00\x00\x00\x09\x00\x00\x00\x51\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x09\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x0a\x00\x00\x00\x57\x00\x00\x00\x02\x00\x00\x00\x51\x00\x00\x00\x0a\x00\x00\x00\x30\x00\x00\x00\x09\x00\x00\x00\x4e\x00\x00\x00\x0a\x00\x00\x00\x4d\x00\x00\x00\x06\x00\x00\x00\x36\x00\x00\x00\x0a\x00\x00\x00\x33\x00\x00\x00\x0b\x00\x00\x00\x58\x00\x00\x00\x0a\x00\x00\x00\x49\x00\x00\x00\x0c\x00\x00\x00\x38\x00\x00\x00\x0a\x00\x00\x00\x52\x00\x00\x00\x0f\x00\x00\x00\x46\x00\x00\x00\x0a\x00\x00\x00\x57\x00\x00\x00\x0e\x00\x00\x00\x41\x00\x00\x00\x0a\x00\x00\x00\x45\x00\x00\x00\x05\x00\x00\x00\x34\x00\x00\x00\x0a\x00\x00\x00\x55\x00\x00\x00\x11\x00\x00\x00\x4b\x00\x00\x00\x0a\x00\x00\x00\x33\x00\x00\x00\x03\x00\x00\x00\x41\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x0b\x00\x00\x00\x4d\x00\x00\x00\x08\x00\x00\x00\x53\x00\x00\x00\x0b\x00\x00\x00\x4a\x00\x00\x00\x11\x00\x00\x00\x52\x00\x00\x00\x0b\x00\x00\x00\x5a\x00\x00\x00\x05\x00\x00\x00\x47\x00\x00\x00\x0b\x00\x00\x00\x52\x00\x00\x00\x0c\x00\x00\x00\x41\x00\x00\x00\x0b\x00\x00\x00\x39\x00\x00\x00\x0d\x00\x00\x00\x31\x00\x00\x00\x0b\x00\x00\x00\x32\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x0b\x00\x00\x00\x32\x00\x00\x00\x0e\x00\x00\x00\x48\x00\x00\x00\x0b\x00\x00\x00\x34\x00\x00\x00\x10\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0c\x00\x00\x00\x38\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0c\x00\x00\x00\x4f\x00\x00\x00\x01\x00\x00\x00\x43\x00\x00\x00\x0c\x00\x00\x00\x54\x00\x00\x00\x0b\x00\x00\x00\x31\x00\x00\x00\x0c\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x36\x00\x00\x00\x0c\x00\x00\x00\x37\x00\x00\x00\x06\x00\x00\x00\x54\x00\x00\x00\x0c\x00\x00\x00\x35\x00\x00\x00\x07\x00\x00\x00\x45\x00\x00\x00\x0c\x00\x00\x00\x50\x00\x00\x00\x13\x00\x00\x00\x53\x00\x00\x00\x0c\x00\x00\x00\x4d\x00\x00\x00\x0e\x00\x00\x00\x4a\x00\x00\x00\x0c\x00\x00\x00\x50\x00\x00\x00\x09\x00\x00\x00\x49\x00\x00\x00\x0c\x00\x00\x00\x57\x00\x00\x00\x10\x00\x00\x00\x41\x00\x00\x00\x0d\x00\x00\x00\x5a\x00\x00\x00\x02\x00\x00\x00\x37\x00\x00\x00\x0d\x00\x00\x00\x4e\x00\x00\x00\x00\x00\x00\x00\x38\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x08\x00\x00\x00\x37\x00\x00\x00\x0d\x00\x00\x00\x45\x00\x00\x00\x07\x00\x00\x00\x36\x00\x00\x00\x0d\x00\x00\x00\x55\x00\x00\x00\x12\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x0d\x00\x00\x00\x57\x00\x00\x00\x05\x00\x00\x00\x44\x00\x00\x00\x0d\x00\x00\x00\x56\x00\x00\x00\x01\x00\x00\x00\x50\x00\x00\x00\x0d\x00\x00\x00\x37\x00\x00\x00\x0f\x00\x00\x00\x36\x00\x00\x00\x0d\x00\x00\x00\x32\x00\x00\x00\x0a\x00\x00\x00\x51\x00\x00\x00\x0e\x00\x00\x00\x34\x00\x00\x00\x0d\x00\x00\x00\x4e\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x09\x00\x00\x00\x36\x00\x00\x00\x0e\x00\x00\x00\x37\x00\x00\x00\x12\x00\x00\x00\x32\x00\x00\x00\x0e\x00\x00\x00\x4b\x00\x00\x00\x0b\x00\x00\x00\x48\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x01\x00\x00\x00\x36\x00\x00\x00\x0e\x00\x00\x00\x57\x00\x00\x00\x04\x00\x00\x00\x4b\x00\x00\x00\x0e\x00\x00\x00\x41\x00\x00\x00\x02\x00\x00\x00\x46\x00\x00\x00\x0e\x00\x00\x00\x30\x00\x00\x00\x06\x00\x00\x00\x59\x00\x00\x00\x0e\x00\x00\x00\x48\x00\x00\x00\x10\x00\x00\x00\x42\x00\x00\x00\x0e\x00\x00\x00\x4e\x00\x00\x00\x0f\x00\x00\x00\x54\x00\x00\x00\x0f\x00\x00\x00\x42\x00\x00\x00\x09\x00\x00\x00\x35\x00\x00\x00\x0f\x00\x00\x00\x59\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x0f\x00\x00\x00\x48\x00\x00\x00\x0d\x00\x00\x00\x30\x00\x00\x00\x0f\x00\x00\x00\x42\x00\x00\x00\x0b\x00\x00\x00\x53\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x11\x00\x00\x00\x54\x00\x00\x00\x0f\x00\x00\x00\x50\x00\x00\x00\x03\x00\x00\x00\x57\x00\x00\x00\x0f\x00\x00\x00\x4c\x00\x00\x00\x01\x00\x00\x00\x32\x00\x00\x00\x0f\x00\x00\x00\x48\x00\x00\x00\x08\x00\x00\x00\x4f\x00\x00\x00\x0f\x00\x00\x00\x51\x00\x00\x00\x02\x00\x00\x00\x43\x00\x00\x00\x0f\x00\x00\x00\x4e\x00\x00\x00\x10\x00\x00\x00\x34\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x0a\x00\x00\x00\x36\x00\x00\x00\x10\x00\x00\x00\x4f\x00\x00\x00\x0b\x00\x00\x00\x51\x00\x00\x00\x10\x00\x00\x00\x42\x00\x00\x00\x06\x00\x00\x00\x4b\x00\x00\x00\x10\x00\x00\x00\x32\x00\x00\x00\x05\x00\x00\x00\x38\x00\x00\x00\x10\x00\x00\x00\x49\x00\x00\x00\x13\x00\x00\x00\x49\x00\x00\x00\x10\x00\x00\x00\x39\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x10\x00\x00\x00\x48\x00\x00\x00\x00\x00\x00\x00\x54\x00\x00\x00\x10\x00\x00\x00\x4a\x00\x00\x00\x01\x00\x00\x00\x32\x00\x00\x00\x10\x00\x00\x00\x57\x00\x00\x00\x0f\x00\x00\x00\x43\x00\x00\x00\x10\x00\x00\x00\x51\x00\x00\x00\x04\x00\x00\x00\x45\x00\x00\x00\x11\x00\x00\x00\x4c\x00\x00\x00\x0f\x00\x00\x00\x44\x00\x00\x00\x11\x00\x00\x00\x52\x00\x00\x00\x04\x00\x00\x00\x4f\x00\x00\x00\x11\x00\x00\x00\x48\x00\x00\x00\x06\x00\x00\x00\x43\x00\x00\x00\x11\x00\x00\x00\x38\x00\x00\x00\x08\x00\x00\x00\x32\x00\x00\x00\x11\x00\x00\x00\x4d\x00\x00\x00\x02\x00\x00\x00\x50\x00\x00\x00\x11\x00\x00\x00\x38\x00\x00\x00\x00\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x5a\x00\x00\x00\x0a\x00\x00\x00\x5a\x00\x00\x00\x11\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x31\x00\x00\x00\x11\x00\x00\x00\x33\x00\x00\x00\x12\x00\x00\x00\x33\x00\x00\x00\x11\x00\x00\x00\x4b\x00\x00\x00\x05\x00\x00\x00\x39\x00\x00\x00\x12\x00\x00\x00\x38\x00\x00\x00\x05\x00\x00\x00\x4b\x00\x00\x00\x12\x00\x00\x00\x46\x00\x00\x00\x0b\x00\x00\x00\x4f\x00\x00\x00\x12\x00\x00\x00\x4d\x00\x00\x00\x11\x00\x00\x00\x55\x00\x00\x00\x12\x00\x00\x00\x53\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x00\x00\x12\x00\x00\x00\x46\x00\x00\x00\x03\x00\x00\x00\x31\x00\x00\x00\x12\x00\x00\x00\x31\x00\x00\x00\x0d\x00\x00\x00\x47\x00\x00\x00\x12\x00\x00\x00\x36\x00\x00\x00\x04\x00\x00\x00\x36\x00\x00\x00\x12\x00\x00\x00\x31\x00\x00\x00\x06\x00\x00\x00\x54\x00\x00\x00\x12\x00\x00\x00\x45\x00\x00\x00\x13\x00\x00\x00\x37\x00\x00\x00\x12\x00\x00\x00\x42\x00\x00\x00\x08\x00\x00\x00\x52\x00\x00\x00\x13\x00\x00\x00\x32\x00\x00\x00\x08\x00\x00\x00\x56\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x0e\x00\x00\x00\x46\x00\x00\x00\x13\x00\x00\x00\x57\x00\x00\x00\x09\x00\x00\x00\x4d\x00\x00\x00\x13\x00\x00\x00\x43\x00\x00\x00\x0d\x00\x00\x00\x57\x00\x00\x00\x13\x00\x00\x00\x56\x00\x00\x00\x04\x00\x00\x00\x47\x00\x00\x00\x13\x00\x00\x00\x42\x00\x00\x00\x02\x00\x00\x00\x37\x00\x00\x00\x13\x00\x00\x00\x49\x00\x00\x00\x01\x00\x00\x00\x38\x00\x00\x00\x13\x00\x00\x00\x47\x00\x00\x00\x05\x00\x00\x00\x32\x00\x00\x00\x13\x00\x00\x00\x54\x00\x00\x00\x0c\x00\x00\x00\x44\x00\x00\x00\x13\x00\x00\x00\x45\x00\x00\x00\x0b\x00\x00\x00\x42\x00\x00\x00'



# Get and print the license key
s.check()
m = s.model()
key = [chr(m[f].as_long()) for f in license]

print("-".join("".join(kv) for kv in chunked(key, 5)))