forked from ellisk42/ec
-
Notifications
You must be signed in to change notification settings - Fork 0
/
phone-4-long-repeat.sl
852 lines (421 loc) · 20.8 KB
/
phone-4-long-repeat.sl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
(set-logic SLIA)
(synth-fun f ((name String)) String
((Start String (ntString))
(ntString String (name " " "(" ")" "-" "."
(str.++ ntString ntString)
(str.replace ntString ntString ntString)
(str.at ntString ntInt)
(int.to.str ntInt)
(str.substr ntString ntInt ntInt)))
(ntInt Int (0 1 2 3 4 5
(+ ntInt ntInt)
(- ntInt ntInt)
(str.len ntString)
(str.to.int ntString)
(str.indexof ntString ntString ntInt)))
(ntBool Bool (true false
(str.prefixof ntString ntString)
(str.suffixof ntString ntString)
(str.contains ntString ntString)))))
(declare-var name String)
(constraint (= (f "938-242-504") "938.242.504"))
(constraint (= (f "938-242-504") "938.242.504"))
(constraint (= (f "938-242-504") "938.242.504"))
(constraint (= (f "308-916-545") "308.916.545"))
(constraint (= (f "308-916-545") "308.916.545"))
(constraint (= (f "308-916-545") "308.916.545"))
(constraint (= (f "623-599-749") "623.599.749"))
(constraint (= (f "623-599-749") "623.599.749"))
(constraint (= (f "623-599-749") "623.599.749"))
(constraint (= (f "981-424-843") "981.424.843"))
(constraint (= (f "981-424-843") "981.424.843"))
(constraint (= (f "981-424-843") "981.424.843"))
(constraint (= (f "118-980-214") "118.980.214"))
(constraint (= (f "118-980-214") "118.980.214"))
(constraint (= (f "118-980-214") "118.980.214"))
(constraint (= (f "244-655-094") "244.655.094"))
(constraint (= (f "244-655-094") "244.655.094"))
(constraint (= (f "244-655-094") "244.655.094"))
(constraint (= (f "830-941-991") "830.941.991"))
(constraint (= (f "830-941-991") "830.941.991"))
(constraint (= (f "830-941-991") "830.941.991"))
(constraint (= (f "911-186-562") "911.186.562"))
(constraint (= (f "911-186-562") "911.186.562"))
(constraint (= (f "911-186-562") "911.186.562"))
(constraint (= (f "002-500-200") "002.500.200"))
(constraint (= (f "002-500-200") "002.500.200"))
(constraint (= (f "002-500-200") "002.500.200"))
(constraint (= (f "113-860-034") "113.860.034"))
(constraint (= (f "113-860-034") "113.860.034"))
(constraint (= (f "113-860-034") "113.860.034"))
(constraint (= (f "457-622-959") "457.622.959"))
(constraint (= (f "457-622-959") "457.622.959"))
(constraint (= (f "457-622-959") "457.622.959"))
(constraint (= (f "986-722-311") "986.722.311"))
(constraint (= (f "986-722-311") "986.722.311"))
(constraint (= (f "986-722-311") "986.722.311"))
(constraint (= (f "110-170-771") "110.170.771"))
(constraint (= (f "110-170-771") "110.170.771"))
(constraint (= (f "110-170-771") "110.170.771"))
(constraint (= (f "469-610-118") "469.610.118"))
(constraint (= (f "469-610-118") "469.610.118"))
(constraint (= (f "469-610-118") "469.610.118"))
(constraint (= (f "817-925-247") "817.925.247"))
(constraint (= (f "817-925-247") "817.925.247"))
(constraint (= (f "817-925-247") "817.925.247"))
(constraint (= (f "256-899-439") "256.899.439"))
(constraint (= (f "256-899-439") "256.899.439"))
(constraint (= (f "256-899-439") "256.899.439"))
(constraint (= (f "886-911-726") "886.911.726"))
(constraint (= (f "886-911-726") "886.911.726"))
(constraint (= (f "886-911-726") "886.911.726"))
(constraint (= (f "562-950-358") "562.950.358"))
(constraint (= (f "562-950-358") "562.950.358"))
(constraint (= (f "562-950-358") "562.950.358"))
(constraint (= (f "693-049-588") "693.049.588"))
(constraint (= (f "693-049-588") "693.049.588"))
(constraint (= (f "693-049-588") "693.049.588"))
(constraint (= (f "840-503-234") "840.503.234"))
(constraint (= (f "840-503-234") "840.503.234"))
(constraint (= (f "840-503-234") "840.503.234"))
(constraint (= (f "698-815-340") "698.815.340"))
(constraint (= (f "698-815-340") "698.815.340"))
(constraint (= (f "698-815-340") "698.815.340"))
(constraint (= (f "498-808-434") "498.808.434"))
(constraint (= (f "498-808-434") "498.808.434"))
(constraint (= (f "498-808-434") "498.808.434"))
(constraint (= (f "329-545-000") "329.545.000"))
(constraint (= (f "329-545-000") "329.545.000"))
(constraint (= (f "329-545-000") "329.545.000"))
(constraint (= (f "380-281-597") "380.281.597"))
(constraint (= (f "380-281-597") "380.281.597"))
(constraint (= (f "380-281-597") "380.281.597"))
(constraint (= (f "332-395-493") "332.395.493"))
(constraint (= (f "332-395-493") "332.395.493"))
(constraint (= (f "332-395-493") "332.395.493"))
(constraint (= (f "251-903-028") "251.903.028"))
(constraint (= (f "251-903-028") "251.903.028"))
(constraint (= (f "251-903-028") "251.903.028"))
(constraint (= (f "176-090-894") "176.090.894"))
(constraint (= (f "176-090-894") "176.090.894"))
(constraint (= (f "176-090-894") "176.090.894"))
(constraint (= (f "336-611-100") "336.611.100"))
(constraint (= (f "336-611-100") "336.611.100"))
(constraint (= (f "336-611-100") "336.611.100"))
(constraint (= (f "416-390-647") "416.390.647"))
(constraint (= (f "416-390-647") "416.390.647"))
(constraint (= (f "416-390-647") "416.390.647"))
(constraint (= (f "019-430-596") "019.430.596"))
(constraint (= (f "019-430-596") "019.430.596"))
(constraint (= (f "019-430-596") "019.430.596"))
(constraint (= (f "960-659-771") "960.659.771"))
(constraint (= (f "960-659-771") "960.659.771"))
(constraint (= (f "960-659-771") "960.659.771"))
(constraint (= (f "475-505-007") "475.505.007"))
(constraint (= (f "475-505-007") "475.505.007"))
(constraint (= (f "475-505-007") "475.505.007"))
(constraint (= (f "424-069-886") "424.069.886"))
(constraint (= (f "424-069-886") "424.069.886"))
(constraint (= (f "424-069-886") "424.069.886"))
(constraint (= (f "941-102-117") "941.102.117"))
(constraint (= (f "941-102-117") "941.102.117"))
(constraint (= (f "941-102-117") "941.102.117"))
(constraint (= (f "331-728-008") "331.728.008"))
(constraint (= (f "331-728-008") "331.728.008"))
(constraint (= (f "331-728-008") "331.728.008"))
(constraint (= (f "487-726-198") "487.726.198"))
(constraint (= (f "487-726-198") "487.726.198"))
(constraint (= (f "487-726-198") "487.726.198"))
(constraint (= (f "612-419-942") "612.419.942"))
(constraint (= (f "612-419-942") "612.419.942"))
(constraint (= (f "612-419-942") "612.419.942"))
(constraint (= (f "594-741-346") "594.741.346"))
(constraint (= (f "594-741-346") "594.741.346"))
(constraint (= (f "594-741-346") "594.741.346"))
(constraint (= (f "320-984-742") "320.984.742"))
(constraint (= (f "320-984-742") "320.984.742"))
(constraint (= (f "320-984-742") "320.984.742"))
(constraint (= (f "060-919-361") "060.919.361"))
(constraint (= (f "060-919-361") "060.919.361"))
(constraint (= (f "060-919-361") "060.919.361"))
(constraint (= (f "275-536-998") "275.536.998"))
(constraint (= (f "275-536-998") "275.536.998"))
(constraint (= (f "275-536-998") "275.536.998"))
(constraint (= (f "548-835-065") "548.835.065"))
(constraint (= (f "548-835-065") "548.835.065"))
(constraint (= (f "548-835-065") "548.835.065"))
(constraint (= (f "197-485-507") "197.485.507"))
(constraint (= (f "197-485-507") "197.485.507"))
(constraint (= (f "197-485-507") "197.485.507"))
(constraint (= (f "455-776-949") "455.776.949"))
(constraint (= (f "455-776-949") "455.776.949"))
(constraint (= (f "455-776-949") "455.776.949"))
(constraint (= (f "085-421-340") "085.421.340"))
(constraint (= (f "085-421-340") "085.421.340"))
(constraint (= (f "085-421-340") "085.421.340"))
(constraint (= (f "785-713-099") "785.713.099"))
(constraint (= (f "785-713-099") "785.713.099"))
(constraint (= (f "785-713-099") "785.713.099"))
(constraint (= (f "426-712-861") "426.712.861"))
(constraint (= (f "426-712-861") "426.712.861"))
(constraint (= (f "426-712-861") "426.712.861"))
(constraint (= (f "386-994-906") "386.994.906"))
(constraint (= (f "386-994-906") "386.994.906"))
(constraint (= (f "386-994-906") "386.994.906"))
(constraint (= (f "918-304-840") "918.304.840"))
(constraint (= (f "918-304-840") "918.304.840"))
(constraint (= (f "918-304-840") "918.304.840"))
(constraint (= (f "247-153-598") "247.153.598"))
(constraint (= (f "247-153-598") "247.153.598"))
(constraint (= (f "247-153-598") "247.153.598"))
(constraint (= (f "075-497-069") "075.497.069"))
(constraint (= (f "075-497-069") "075.497.069"))
(constraint (= (f "075-497-069") "075.497.069"))
(constraint (= (f "140-726-583") "140.726.583"))
(constraint (= (f "140-726-583") "140.726.583"))
(constraint (= (f "140-726-583") "140.726.583"))
(constraint (= (f "049-413-248") "049.413.248"))
(constraint (= (f "049-413-248") "049.413.248"))
(constraint (= (f "049-413-248") "049.413.248"))
(constraint (= (f "977-386-462") "977.386.462"))
(constraint (= (f "977-386-462") "977.386.462"))
(constraint (= (f "977-386-462") "977.386.462"))
(constraint (= (f "058-272-455") "058.272.455"))
(constraint (= (f "058-272-455") "058.272.455"))
(constraint (= (f "058-272-455") "058.272.455"))
(constraint (= (f "428-629-927") "428.629.927"))
(constraint (= (f "428-629-927") "428.629.927"))
(constraint (= (f "428-629-927") "428.629.927"))
(constraint (= (f "449-122-191") "449.122.191"))
(constraint (= (f "449-122-191") "449.122.191"))
(constraint (= (f "449-122-191") "449.122.191"))
(constraint (= (f "568-759-670") "568.759.670"))
(constraint (= (f "568-759-670") "568.759.670"))
(constraint (= (f "568-759-670") "568.759.670"))
(constraint (= (f "312-846-053") "312.846.053"))
(constraint (= (f "312-846-053") "312.846.053"))
(constraint (= (f "312-846-053") "312.846.053"))
(constraint (= (f "943-037-297") "943.037.297"))
(constraint (= (f "943-037-297") "943.037.297"))
(constraint (= (f "943-037-297") "943.037.297"))
(constraint (= (f "014-270-177") "014.270.177"))
(constraint (= (f "014-270-177") "014.270.177"))
(constraint (= (f "014-270-177") "014.270.177"))
(constraint (= (f "658-877-878") "658.877.878"))
(constraint (= (f "658-877-878") "658.877.878"))
(constraint (= (f "658-877-878") "658.877.878"))
(constraint (= (f "888-594-038") "888.594.038"))
(constraint (= (f "888-594-038") "888.594.038"))
(constraint (= (f "888-594-038") "888.594.038"))
(constraint (= (f "232-253-254") "232.253.254"))
(constraint (= (f "232-253-254") "232.253.254"))
(constraint (= (f "232-253-254") "232.253.254"))
(constraint (= (f "308-722-292") "308.722.292"))
(constraint (= (f "308-722-292") "308.722.292"))
(constraint (= (f "308-722-292") "308.722.292"))
(constraint (= (f "342-145-742") "342.145.742"))
(constraint (= (f "342-145-742") "342.145.742"))
(constraint (= (f "342-145-742") "342.145.742"))
(constraint (= (f "568-181-515") "568.181.515"))
(constraint (= (f "568-181-515") "568.181.515"))
(constraint (= (f "568-181-515") "568.181.515"))
(constraint (= (f "300-140-756") "300.140.756"))
(constraint (= (f "300-140-756") "300.140.756"))
(constraint (= (f "300-140-756") "300.140.756"))
(constraint (= (f "099-684-216") "099.684.216"))
(constraint (= (f "099-684-216") "099.684.216"))
(constraint (= (f "099-684-216") "099.684.216"))
(constraint (= (f "575-296-621") "575.296.621"))
(constraint (= (f "575-296-621") "575.296.621"))
(constraint (= (f "575-296-621") "575.296.621"))
(constraint (= (f "994-443-794") "994.443.794"))
(constraint (= (f "994-443-794") "994.443.794"))
(constraint (= (f "994-443-794") "994.443.794"))
(constraint (= (f "400-334-692") "400.334.692"))
(constraint (= (f "400-334-692") "400.334.692"))
(constraint (= (f "400-334-692") "400.334.692"))
(constraint (= (f "684-711-883") "684.711.883"))
(constraint (= (f "684-711-883") "684.711.883"))
(constraint (= (f "684-711-883") "684.711.883"))
(constraint (= (f "539-636-358") "539.636.358"))
(constraint (= (f "539-636-358") "539.636.358"))
(constraint (= (f "539-636-358") "539.636.358"))
(constraint (= (f "009-878-919") "009.878.919"))
(constraint (= (f "009-878-919") "009.878.919"))
(constraint (= (f "009-878-919") "009.878.919"))
(constraint (= (f "919-545-701") "919.545.701"))
(constraint (= (f "919-545-701") "919.545.701"))
(constraint (= (f "919-545-701") "919.545.701"))
(constraint (= (f "546-399-239") "546.399.239"))
(constraint (= (f "546-399-239") "546.399.239"))
(constraint (= (f "546-399-239") "546.399.239"))
(constraint (= (f "993-608-757") "993.608.757"))
(constraint (= (f "993-608-757") "993.608.757"))
(constraint (= (f "993-608-757") "993.608.757"))
(constraint (= (f "107-652-845") "107.652.845"))
(constraint (= (f "107-652-845") "107.652.845"))
(constraint (= (f "107-652-845") "107.652.845"))
(constraint (= (f "206-805-793") "206.805.793"))
(constraint (= (f "206-805-793") "206.805.793"))
(constraint (= (f "206-805-793") "206.805.793"))
(constraint (= (f "198-857-684") "198.857.684"))
(constraint (= (f "198-857-684") "198.857.684"))
(constraint (= (f "198-857-684") "198.857.684"))
(constraint (= (f "912-827-430") "912.827.430"))
(constraint (= (f "912-827-430") "912.827.430"))
(constraint (= (f "912-827-430") "912.827.430"))
(constraint (= (f "560-951-766") "560.951.766"))
(constraint (= (f "560-951-766") "560.951.766"))
(constraint (= (f "560-951-766") "560.951.766"))
(constraint (= (f "142-178-290") "142.178.290"))
(constraint (= (f "142-178-290") "142.178.290"))
(constraint (= (f "142-178-290") "142.178.290"))
(constraint (= (f "732-196-946") "732.196.946"))
(constraint (= (f "732-196-946") "732.196.946"))
(constraint (= (f "732-196-946") "732.196.946"))
(constraint (= (f "963-875-745") "963.875.745"))
(constraint (= (f "963-875-745") "963.875.745"))
(constraint (= (f "963-875-745") "963.875.745"))
(constraint (= (f "881-865-867") "881.865.867"))
(constraint (= (f "881-865-867") "881.865.867"))
(constraint (= (f "881-865-867") "881.865.867"))
(constraint (= (f "234-686-715") "234.686.715"))
(constraint (= (f "234-686-715") "234.686.715"))
(constraint (= (f "234-686-715") "234.686.715"))
(constraint (= (f "720-330-583") "720.330.583"))
(constraint (= (f "720-330-583") "720.330.583"))
(constraint (= (f "720-330-583") "720.330.583"))
(constraint (= (f "593-065-126") "593.065.126"))
(constraint (= (f "593-065-126") "593.065.126"))
(constraint (= (f "593-065-126") "593.065.126"))
(constraint (= (f "671-778-064") "671.778.064"))
(constraint (= (f "671-778-064") "671.778.064"))
(constraint (= (f "671-778-064") "671.778.064"))
(constraint (= (f "252-029-036") "252.029.036"))
(constraint (= (f "252-029-036") "252.029.036"))
(constraint (= (f "252-029-036") "252.029.036"))
(constraint (= (f "700-322-036") "700.322.036"))
(constraint (= (f "700-322-036") "700.322.036"))
(constraint (= (f "700-322-036") "700.322.036"))
(constraint (= (f "882-587-473") "882.587.473"))
(constraint (= (f "882-587-473") "882.587.473"))
(constraint (= (f "882-587-473") "882.587.473"))
(constraint (= (f "964-134-953") "964.134.953"))
(constraint (= (f "964-134-953") "964.134.953"))
(constraint (= (f "964-134-953") "964.134.953"))
(constraint (= (f "038-300-876") "038.300.876"))
(constraint (= (f "038-300-876") "038.300.876"))
(constraint (= (f "038-300-876") "038.300.876"))
(constraint (= (f "158-894-947") "158.894.947"))
(constraint (= (f "158-894-947") "158.894.947"))
(constraint (= (f "158-894-947") "158.894.947"))
(constraint (= (f "757-454-374") "757.454.374"))
(constraint (= (f "757-454-374") "757.454.374"))
(constraint (= (f "757-454-374") "757.454.374"))
(constraint (= (f "872-513-190") "872.513.190"))
(constraint (= (f "872-513-190") "872.513.190"))
(constraint (= (f "872-513-190") "872.513.190"))
(constraint (= (f "566-086-726") "566.086.726"))
(constraint (= (f "566-086-726") "566.086.726"))
(constraint (= (f "566-086-726") "566.086.726"))
(constraint (= (f "938-242-504") "938.242.504"))
(constraint (= (f "308-916-545") "308.916.545"))
(constraint (= (f "623-599-749") "623.599.749"))
(constraint (= (f "981-424-843") "981.424.843"))
(constraint (= (f "118-980-214") "118.980.214"))
(constraint (= (f "244-655-094") "244.655.094"))
(constraint (= (f "830-941-991") "830.941.991"))
(constraint (= (f "911-186-562") "911.186.562"))
(constraint (= (f "002-500-200") "002.500.200"))
(constraint (= (f "113-860-034") "113.860.034"))
(constraint (= (f "457-622-959") "457.622.959"))
(constraint (= (f "986-722-311") "986.722.311"))
(constraint (= (f "110-170-771") "110.170.771"))
(constraint (= (f "469-610-118") "469.610.118"))
(constraint (= (f "817-925-247") "817.925.247"))
(constraint (= (f "256-899-439") "256.899.439"))
(constraint (= (f "886-911-726") "886.911.726"))
(constraint (= (f "562-950-358") "562.950.358"))
(constraint (= (f "693-049-588") "693.049.588"))
(constraint (= (f "840-503-234") "840.503.234"))
(constraint (= (f "698-815-340") "698.815.340"))
(constraint (= (f "498-808-434") "498.808.434"))
(constraint (= (f "329-545-000") "329.545.000"))
(constraint (= (f "380-281-597") "380.281.597"))
(constraint (= (f "332-395-493") "332.395.493"))
(constraint (= (f "251-903-028") "251.903.028"))
(constraint (= (f "176-090-894") "176.090.894"))
(constraint (= (f "336-611-100") "336.611.100"))
(constraint (= (f "416-390-647") "416.390.647"))
(constraint (= (f "019-430-596") "019.430.596"))
(constraint (= (f "960-659-771") "960.659.771"))
(constraint (= (f "475-505-007") "475.505.007"))
(constraint (= (f "424-069-886") "424.069.886"))
(constraint (= (f "941-102-117") "941.102.117"))
(constraint (= (f "331-728-008") "331.728.008"))
(constraint (= (f "487-726-198") "487.726.198"))
(constraint (= (f "612-419-942") "612.419.942"))
(constraint (= (f "594-741-346") "594.741.346"))
(constraint (= (f "320-984-742") "320.984.742"))
(constraint (= (f "060-919-361") "060.919.361"))
(constraint (= (f "275-536-998") "275.536.998"))
(constraint (= (f "548-835-065") "548.835.065"))
(constraint (= (f "197-485-507") "197.485.507"))
(constraint (= (f "455-776-949") "455.776.949"))
(constraint (= (f "085-421-340") "085.421.340"))
(constraint (= (f "785-713-099") "785.713.099"))
(constraint (= (f "426-712-861") "426.712.861"))
(constraint (= (f "386-994-906") "386.994.906"))
(constraint (= (f "918-304-840") "918.304.840"))
(constraint (= (f "247-153-598") "247.153.598"))
(constraint (= (f "075-497-069") "075.497.069"))
(constraint (= (f "140-726-583") "140.726.583"))
(constraint (= (f "049-413-248") "049.413.248"))
(constraint (= (f "977-386-462") "977.386.462"))
(constraint (= (f "058-272-455") "058.272.455"))
(constraint (= (f "428-629-927") "428.629.927"))
(constraint (= (f "449-122-191") "449.122.191"))
(constraint (= (f "568-759-670") "568.759.670"))
(constraint (= (f "312-846-053") "312.846.053"))
(constraint (= (f "943-037-297") "943.037.297"))
(constraint (= (f "014-270-177") "014.270.177"))
(constraint (= (f "658-877-878") "658.877.878"))
(constraint (= (f "888-594-038") "888.594.038"))
(constraint (= (f "232-253-254") "232.253.254"))
(constraint (= (f "308-722-292") "308.722.292"))
(constraint (= (f "342-145-742") "342.145.742"))
(constraint (= (f "568-181-515") "568.181.515"))
(constraint (= (f "300-140-756") "300.140.756"))
(constraint (= (f "099-684-216") "099.684.216"))
(constraint (= (f "575-296-621") "575.296.621"))
(constraint (= (f "994-443-794") "994.443.794"))
(constraint (= (f "400-334-692") "400.334.692"))
(constraint (= (f "684-711-883") "684.711.883"))
(constraint (= (f "539-636-358") "539.636.358"))
(constraint (= (f "009-878-919") "009.878.919"))
(constraint (= (f "919-545-701") "919.545.701"))
(constraint (= (f "546-399-239") "546.399.239"))
(constraint (= (f "993-608-757") "993.608.757"))
(constraint (= (f "107-652-845") "107.652.845"))
(constraint (= (f "206-805-793") "206.805.793"))
(constraint (= (f "198-857-684") "198.857.684"))
(constraint (= (f "912-827-430") "912.827.430"))
(constraint (= (f "560-951-766") "560.951.766"))
(constraint (= (f "142-178-290") "142.178.290"))
(constraint (= (f "732-196-946") "732.196.946"))
(constraint (= (f "963-875-745") "963.875.745"))
(constraint (= (f "881-865-867") "881.865.867"))
(constraint (= (f "234-686-715") "234.686.715"))
(constraint (= (f "720-330-583") "720.330.583"))
(constraint (= (f "593-065-126") "593.065.126"))
(constraint (= (f "671-778-064") "671.778.064"))
(constraint (= (f "252-029-036") "252.029.036"))
(constraint (= (f "700-322-036") "700.322.036"))
(constraint (= (f "882-587-473") "882.587.473"))
(constraint (= (f "964-134-953") "964.134.953"))
(constraint (= (f "038-300-876") "038.300.876"))
(constraint (= (f "158-894-947") "158.894.947"))
(constraint (= (f "757-454-374") "757.454.374"))
(constraint (= (f "872-513-190") "872.513.190"))
(constraint (= (f "566-086-726") "566.086.726"))
(check-synth)