```from z3 import *import stringflag=bytes.fromhex("07740277000105007572727106040400")first=flag[:8]second=flag[8:]def test(inp,target):    for i in range(8):        xorer=inp[i]        for j in range(8):            inp[j]^=xorer    assert inp==targetdef find(target):    flag=[BitVec(f"x{i}",8) for i in range(8)]    k=flag[:]    for i in range(8):        xorer=k[i]        for j in range(8):            k[j]^=xorer
    s=Solver()    ### only uppercase hex character    for i in range(len(flag)):        s.add(flag[i]<0x7f)        s.add(0x20<=flag[i])        for j in string.printable[:-6]:            if(j not in "0123456789ABCDEF"):                s.add(flag[i]!=ord(j))
    for i in range(len(target)):        s.add(k[i]==target[i])    print(s.check())    m=s.model()    l=[]    for i in flag:        l.append(m[i].as_long())    return bytearray(l).decode()
flag_first=find(first)flag_second=find(second)test(bytearray(flag_first.encode()),first)test(bytearray(flag_second.encode()),second)print("ENO{"+flag_first+flag_second+"}")```