from z3 import *

#A 행렬(38 * 38, 직접 구함)
value_str = "239	117	113	160	175	170	73	59	28	178	206	64	95	109	249	193	184	0	165	42	223	8	117	205	145	54	75	152	189	73	127	237	200	136	200	150	178	9 \
97	108	72	187	37	34	232	185	210	217	16	85	155	136	152	241	2	184	92	15	142	51	128	102	225	239	73	70	230	0	229	177	204	37	103	238	88	110	 \
74	80	83	141	35	126	180	99	241	64	127	144	24	122	132	36	107	2	12	176	210	158	34	36	141	82	138	126	197	125	3	201	75	225	186	152	92	106	 \
108	232	209	239	92	138	216	43	51	151	177	89	17	124	233	88	115	107	6	191	224	17	65	77	146	156	61	236	53	36	230	27	145	57	169	144	62	220	 \
214	186	140	232	21	38	103	88	229	86	121	136	236	6	39	27	127	115	217	34	5	62	95	118	90	182	206	246	111	18	37	137	244	152	23	18	179	68	 \
196	150	210	134	147	46	189	60	225	78	72	219	54	97	50	60	246	127	250	46	148	80	249	103	191	157	38	125	104	11	236	94	4	13	19	237	118	232	 \
194	60	201	9	173	106	210	129	6	61	111	92	233	41	65	126	243	246	6	169	100	25	195	15	164	51	102	211	137	17	35	12	31	172	201	160	73	11	 \
101	70	232	158	111	143	226	111	65	137	128	144	90	199	189	90	64	243	84	161	233	10	152	85	78	184	23	149	30	6	157	67	21	7	181	145	40	160	 \
210	184	133	28	29	208	6	19	0	202	163	197	117	133	189	150	6	64	64	43	21	22	93	173	57	97	57	30	90	144	139	87	63	199	3	178	31	85	 \
28	130	214	0	110	123	83	15	2	125	59	160	220	6	188	27	110	6	170	164	60	52	193	103	76	78	168	144	229	216	40	22	109	88	221	145	52	160	 \
196	2	77	39	240	128	51	42	204	74	135	240	111	140	118	173	14	110	53	77	226	114	26	8	15	64	145	190	102	157	132	71	117	23	183	104	217	50	 \
210	81	202	27	0	30	215	111	96	117	41	115	226	124	172	42	241	14	231	134	23	98	250	9	198	155	119	223	178	189	133	105	134	200	86	42	17	73	 \
11	82	129	190	108	50	81	129	134	45	89	237	202	199	212	214	229	241	33	140	111	173	221	15	155	81	118	208	190	229	123	247	90	174	185	12	242	123	 \
155	211	7	85	236	124	237	184	46	198	26	222	54	103	187	115	63	229	227	34	223	159	122	196	132	228	29	26	87	126	238	39	192	153	119	81	76	45	 \
96	106	198	73	16	212	220	208	183	201	101	203	120	77	121	207	216	63	250	100	35	151	110	34	146	148	55	167	82	183	238	113	247	223	110	24	236	246	 \
76	226	120	69	128	177	70	174	16	74	151	200	197	18	19	196	21	216	79	213	41	16	30	31	223	206	64	196	126	191	101	83	140	175	250	193	166	246	 \
234	115	180	6	211	101	34	6	16	159	59	5	148	66	101	167	90	21	20	93	120	211	55	182	163	241	231	31	8	234	66	180	66	18	158	49	85	169	 \
218	205	220	91	42	38	40	191	72	77	35	174	211	136	133	36	27	90	141	119	27	103	182	90	219	111	113	159	100	198	121	33	6	28	95	153	110	160	 \
216	59	45	9	72	210	119	243	198	242	3	51	135	50	10	244	82	27	194	26	112	29	195	45	189	107	67	151	18	181	167	243	83	40	78	7	72	175	 \
184	104	101	160	174	53	35	232	169	122	92	49	33	80	127	235	188	82	75	83	100	55	168	209	110	118	106	239	28	94	186	204	73	118	121	76	182	102	 \
47	55	121	34	173	244	24	15	214	198	133	15	221	196	153	236	45	188	209	48	101	59	177	90	62	147	16	80	243	250	102	195	183	129	97	168	105	230	 \
173	96	68	55	103	197	148	53	16	59	44	207	117	198	178	133	135	45	167	85	47	173	108	14	140	46	69	129	24	147	138	227	238	152	172	192	13	186	 \
186	231	137	246	234	198	68	85	172	145	56	65	46	141	64	57	162	135	56	220	217	81	231	38	191	244	51	213	242	146	122	204	73	63	249	182	70	114	 \
25	219	250	195	231	76	77	149	183	42	113	29	21	51	134	112	199	162	85	203	122	245	114	70	169	129	130	81	247	121	214	73	151	47	10	21	52	227	 \
130	247	73	161	231	58	15	234	215	244	169	228	235	9	118	69	223	199	31	184	137	105	216	149	107	117	1	58	150	186	8	181	150	113	124	5	82	127	 \
237	219	245	199	189	208	150	165	118	123	36	119	193	142	89	179	239	223	125	108	49	68	194	48	122	206	129	196	28	242	126	66	213	232	145	148	164	224	 \
244	202	138	77	78	136	169	201	236	157	233	19	82	66	119	175	36	239	238	106	37	141	33	167	84	241	190	120	236	240	71	216	107	20	22	113	187	142	 \
180	89	166	147	79	166	35	108	121	86	178	86	142	165	0	213	223	36	162	118	186	50	237	21	183	109	206	186	82	135	164	111	39	77	94	203	214	233	 \
216	4	155	24	227	85	142	105	171	145	173	71	237	199	35	246	125	223	219	131	55	204	125	8	159	179	215	46	172	58	107	7	59	94	25	55	227	46	 \
217	229	156	117	155	218	121	37	136	135	140	208	221	26	143	168	127	125	74	140	100	28	217	92	52	165	20	204	67	208	100	217	85	102	172	209	19	228	 \
162	133	135	54	178	78	24	143	107	79	148	49	69	117	21	249	126	127	161	179	70	120	195	102	78	187	227	149	49	124	149	65	215	174	100	45	152	167	 \
149	24	122	75	208	177	82	96	7	103	190	124	233	185	55	231	180	126	222	208	64	67	233	24	79	246	2	170	235	53	45	217	241	164	99	232	41	180	 \
234	46	94	230	99	9	220	103	140	215	104	183	94	225	146	179	54	180	206	37	164	220	215	89	216	128	77	205	216	27	145	23	101	132	48	12	189	91	 \
91	224	238	46	52	48	213	127	195	187	103	135	29	237	75	63	174	54	5	93	196	11	210	28	171	250	231	182	73	169	14	99	214	10	72	3	59	111	 \
137	241	105	205	206	64	0	102	2	243	110	140	186	143	228	65	138	174	169	194	218	232	161	3	53	163	211	162	154	25	113	202	246	73	157	245	51	225	 \
188	105	2	102	37	93	14	104	45	52	236	159	99	242	165	113	49	138	116	209	0	130	200	165	165	212	91	45	91	104	134	16	10	5	132	13	44	203	 \
102	248	208	39	166	92	124	70	54	14	222	50	79	245	138	161	143	49	184	41	8	165	190	67	175	212	96	214	84	122	182	159	125	54	114	151	233	10	 \
1	31	55	68	231	80	185	41	171	212	22	166	61	15	184	126	0	143	187	210	191	1	94	42	97	65	115	214	80	177	105	6	235	6	130	171	58	131".split(
    " "
)
value = list()
for i in range(38):
    value.append(value_str[i].split("\t"))

bytes_21BD60 = "141 19 175 235 67 221 136 245 242 163 220 204 13 60 76 235 82 200 153 127 132 244 84 57 77 201 232 24 122 148 224 158 80 162 197 193 170 177".split(
    " "
)


s = Solver()
arr = [BitVec("%d" % i, 8) for i in range(38)]
for i in range(38):
    s.add(32 <= arr[i], arr[i] <= 126)

for i in range(38):
    tmp = 0
    for j in range(38):
        tmp += int(value[i][j]) * arr[j]
        tmp %= 251
    s.add(tmp == bytes_21BD60[i])

s.check()
print(s.model())