```
#
# Double xor encryption with 21 byte A and 19 byte key B is the same thing as encypring with one 399 byte key C.
#
# A01 .. A19 A01 A02 A03 ... A19 | A01
# B01 .. B19 B20 B21 B01 ... B21 | B01
# ------------------------------------
# C01 .. C399 | C01
#
# Step 1 - Recover 399 byte xor key C with histogram analysis, assuming 481 / (Space) as the most frequent character.
#
# Step 2 - Use z3 solver to recover original (A,B) keys from C.
#
# There are multiple solutions so we introduced additional constraints for keys:
# - ASCII printable,
# - must have '_' somewhere in it.
#

from z3 import *

from collections import defaultdict

f = open("encrypted.txt")

hist = {}
for i in range(399):
hist[i] = defaultdict(int)

idx = 0
while True:
line = f.readline().strip()
if len(line)==0:
break
n = int(line)
hist[idx%399][n] += 1
idx += 1

key = []
for i in range(399):
items = list(hist[i].items())
items.sort(key=lambda a: -a[1])
# print(items[0])
key.append(items[0][0] ^ 481)

print(key)

k1 = []
for i in range(21):
k1.append(BitVec('k1'+str(i), 8))
k2 = []
for i in range(19):
k2.append(BitVec('k2'+str(i), 8))

s = Solver()
for i in range(399):
s.add(k1[i%21] ^ k2[i%19] == key[i])

# Assume key values are in ASCII-printable range
for i in range(21):
s.add(k1[i] >= 32)
s.add(k1[i] < 127)

for i in range(19):
s.add(k2[i] >= 32)
s.add(k2[i] < 127)

# assume there is '_' somewhere in key1
# found this by manual brute-forcing
s.add(k1[6] == ord('_'))

print(s.check())
m = s.model()
# print(m)

print("\n\nKey1")
for i in range(21):
print(m.evaluate(k1[i]))

print("\n\nKey2")
for i in range(19):
print(m.evaluate(k2[i]))

# flag{h3r3'5_th3_f1r5t_h4lf_th3_53c0nd_15_th15}
```