from z3 import *
import string
flag=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==target
def 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+"}")